Irreducible short exact sequences are almost split

We formalize the comparison argument of Auslander--Reiten--Smalø, Proposition V.5.9, in the direction needed for the Butler--Ringel canonical string sequences. A short exact sequence whose two differentials are irreducible is compared with an existing almost-split sequence at the same right endpoint. Irreducibility makes the comparison maps split monic; the local endomorphism ring of the comparison kernel upgrades the left comparison to an isomorphism, and the short five lemma upgrades the middle comparison.

theorem MagnitudeConjecture.CategoryTheory.isIrreducibleMorphism_ne_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X Y : C} {f : X ⟶ Y} (hf : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f) : f ≠ 0

An irreducible morphism in an abelian category is nonzero.

theorem MagnitudeConjecture.CategoryTheory.ShortComplex.shortExact_of_exact_of_irreducible {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex C} (hexact : S.Exact) (hf : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism S.f) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism S.g) : S.ShortExact

Exactness plus irreducibility of both differentials already forces a short complex in an abelian category to be short exact.

theorem MagnitudeConjecture.CategoryTheory.ShortComplex.ShortExact.isRightAlmostSplit_of_irreducible {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {S T : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (hT : T.ShortExact) (hf : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism S.f) (hg : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism S.g) (hTf : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit T.f) (hTg : QuotientSubmoduleEquidistribution.IsRightAlmostSplit T.g) [IsLocalRing (CategoryTheory.End T.X₁)] (e₃ : S.X₃ ≅ T.X₃) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit S.g

Auslander--Reiten--Smalø V.5.9, comparison form. If S is short exact and both its maps are irreducible, then its terminal map is right almost split as soon as an almost-split short exact sequence T with the same right endpoint is available.