Ext vanishing extends maps out of kernels

theorem MagnitudeConjecture.FiniteKernel.kernel_extension_of_ext_vanishing {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {Z I : C} (f : Z ⟶ I) (hext : ∀ (U : C) (j : U ⟶ I), CategoryTheory.Mono j → ∀ (xi : CategoryTheory.Abelian.Ext U Z 1), xi = 0) (h : CategoryTheory.Limits.kernel f ⟶ Z) : ∃ (a : Z ⟶ Z), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) a = h

If Ext¹(U,Z) vanishes for every subobject U of I, every map ker f to Z extends to an endomorphism of Z, for every f from Z to I.