Isomorphic kernels force proportional maps under an extension hypothesis

theorem MagnitudeConjecture.FiniteKernel.exists_end_factor_of_kernel_comp_zero {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Abelian C] {Z I : C} [CategoryTheory.Injective I] (f g : Z ⟶ I) (hg : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) g = 0) : ∃ (a : I ⟶ I), CategoryTheory.CategoryStruct.comp f a = g

A map annihilating the kernel of f factors through f when its target is injective. The coimage realizes the required intermediate quotient.

theorem MagnitudeConjecture.FiniteKernel.exists_scalar_of_kernel_comp_zero {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] {Z I : C} [CategoryTheory.Injective I] (hI : ∀ (a : I ⟶ I), ∃ (c : k), a = c • CategoryTheory.CategoryStruct.id I) (f g : Z ⟶ I) (hg : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) g = 0) : ∃ (c : k), c • f = g

Scalar endomorphisms of an injective target turn kernel containment into proportionality of the maps.

theorem MagnitudeConjecture.FiniteKernel.exists_scalar_of_kernel_iso {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear k C] {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) (f g : Z ⟶ I) (e : CategoryTheory.Limits.kernel f ≅ CategoryTheory.Limits.kernel g) (hext : ∀ (h : CategoryTheory.Limits.kernel f ⟶ Z), ∃ (a : Z ⟶ Z), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) a = h) : ∃ (c : k), c • f = g

If maps from ker f to Z extend over Z, scalar endomorphisms of Z and of an injective target imply that isomorphic kernels give proportional maps.