Irreducible short exact sequences in a finite module category

A complete finite indecomposable skeleton supplies a chosen minimal right almost-split map at every indecomposable endpoint. Consequently the abstract irreducible-short-exact comparison theorem can be applied without making the comparison sequence an extra input.

theorem MagnitudeConjecture.CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton.isRightAlmostSplit_of_shortExact_of_irreducible {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (V : FiniteDimensionalModuleIndecomposableSkeleton) [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] {S : CategoryTheory.ShortComplex (FiniteDimensionalModuleCategory k)} (hS : S.ShortExact) (hf : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism S.f) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism S.g) (y : Fin V.n) (e₃ : S.X₃ ≅ V.obj y) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit S.g

A short exact complex with two irreducible differentials and an endpoint in a complete finite indecomposable skeleton is right almost split.