Removing an injective kernel from a right almost-split map

An injective kernel splits off the source of a right almost-split morphism. The induced morphism on the complementary summand is monic, right almost split, and therefore right minimal.

theorem MagnitudeConjecture.CategoryTheory.exists_mono_rightAlmostSplit_complement_of_injective_kernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E Y : C} (f : E ⟶ Y) (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f) [CategoryTheory.Injective (CategoryTheory.Limits.kernel f)] : ∃ (E' : C) (g : E' ⟶ Y), CategoryTheory.Mono g ∧ QuotientSubmoduleEquidistribution.IsRightAlmostSplit g ∧ QuotientSubmoduleEquidistribution.IsRightMinimal g ∧ Nonempty (E ≅ CategoryTheory.Limits.kernel f ⊞ E')

A right almost-split morphism with injective kernel is the direct sum of that kernel, mapped to zero, and a monic minimal right almost-split map.