Minimalizing almost-split maps of finite modules

Any right almost-split map between finite-support pointwise finite-dimensional modules can be replaced by a right-minimal one. The proof minimizes total pointwise dimension of the source. A noninvertible endomorphism fixing a minimal candidate would make its categorical image a strictly smaller right almost-split source.

The exact dual construction minimizes the target of a left almost-split morphism.

theorem MagnitudeConjecture.CoveringHom.finiteDimensionalModule_exists_rightMinimal_rightAlmostSplit {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {M E : FiniteDimensionalModuleCategory k} (f : E ⟶ M) (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f) : ∃ (E' : FiniteDimensionalModuleCategory k) (f' : E' ⟶ M), QuotientSubmoduleEquidistribution.IsRightAlmostSplit f' ∧ QuotientSubmoduleEquidistribution.IsRightMinimal f'

A right almost-split morphism with finite-dimensional source can be replaced by a right-minimal right almost-split morphism to the same target.

theorem MagnitudeConjecture.CoveringHom.finiteDimensionalModule_exists_leftMinimal_leftAlmostSplit {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {M E : FiniteDimensionalModuleCategory k} (f : M ⟶ E) (hf : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f) : ∃ (E' : FiniteDimensionalModuleCategory k) (f' : M ⟶ E'), QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f' ∧ QuotientSubmoduleEquidistribution.IsLeftMinimal f'

A left almost-split morphism with finite-dimensional target can be replaced by a left-minimal left almost-split morphism from the same source.