The finite-kernel bound for representation-finite right modules

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finrank_hom_le_one_of_ext_vanishing {k A : Type u} [Field k] [Infinite k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [CategoryTheory.HasExt (FGModuleCat Aᵐᵒᵖ)] (S : FiniteIndecomposableSkeleton k A) (Z I : FinitelyGeneratedCategory A) [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 : FinitelyGeneratedCategory A) (j : U ⟶ I), CategoryTheory.Mono j → ∀ (xi : CategoryTheory.Abelian.Ext U Z 1), xi = 0) : Module.finrank k (Z ⟶ I) ≤ 1

Scalar endpoint endomorphisms and Ext vanishing on submodules of an injective target bound the Hom dimension by one.