The finite-kernel lemma from Ext vanishing on subobjects

theorem MagnitudeConjecture.FiniteKernel.finrank_hom_le_one_of_ext_vanishing {k : Type u} [Field k] [Infinite k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] [CategoryTheory.Limits.HasFiniteBiproducts C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] {ι : Type} [Fintype ι] (F : ι → C) (hF : ∀ (i : ι), ¬CategoryTheory.Limits.IsZero (F i)) (hdec : ∀ (X : C), ∃ (n : ℕ) (label : Fin n → ι), Nonempty (X ≅ ⨁ fun (j : Fin n) => F (label j))) (Z I : C) [CategoryTheory.Injective I] (hZ : ∀ (a : Z ⟶ Z), ∃ (c : k), a = c • CategoryTheory.CategoryStruct.id Z) (hI : ∀ (a : I ⟶ I), ∃ (c : k), a = c • CategoryTheory.CategoryStruct.id I) (hext : ∀ (U : C) (j : U ⟶ I), CategoryTheory.Mono j → ∀ (xi : CategoryTheory.Abelian.Ext U Z 1), xi = 0) : Module.finrank k (Z ⟶ I) ≤ 1

In a Hom-finite category with a finite additive classification, the frozen finite-kernel hypotheses imply that Hom(Z,I) has dimension at most one.