Comparing short exact sequences with an almost-split sequence

This file isolates the final diagram argument in Gabriel's preservation proof. Given a comparison to a right almost-split short exact sequence, it is enough to identify the left terms and to know that every noninvertible endomorphism of the source left term factors through its injection. The comparison on the middle terms is then invertible by exactness.

theorem MagnitudeConjecture.CategoryTheory.ShortComplex.ShortExact.isSplitMono_f_of_isSplitEpi_g {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Balanced C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) [CategoryTheory.IsSplitEpi S.g] : CategoryTheory.IsSplitMono S.f

In a short exact sequence, a splitting of the terminal epimorphism also splits the initial monomorphism.

theorem MagnitudeConjecture.CategoryTheory.ShortComplex.ShortExact.not_isSplitEpi_g_of_not_isSplitMono_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Balanced C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (hf : ¬CategoryTheory.IsSplitMono S.f) : ¬CategoryTheory.IsSplitEpi S.g

Contrapositive splitting lemma for a short exact sequence.

theorem MagnitudeConjecture.CategoryTheory.ShortComplex.ShortExact.isRightAlmostSplit_of_leftEndomorphismFactorization {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {S T : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (hT : T.ShortExact) (hTg : QuotientSubmoduleEquidistribution.IsRightAlmostSplit T.g) (hSg : ¬CategoryTheory.IsSplitEpi S.g) (e₁ : T.X₁ ≅ S.X₁) (e₃ : S.X₃ ≅ T.X₃) (hfac : ∀ (q : S.X₁ ⟶ S.X₁), ¬CategoryTheory.IsIso q → ∃ (c : S.X₂ ⟶ S.X₁), CategoryTheory.CategoryStruct.comp S.f c = q) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit S.g

A short exact sequence is right almost split when its endpoint is identified with that of a right almost-split short exact sequence, its left term is identified with the comparison kernel, and every noninvertible endomorphism of its left term factors through its injection.

The proof first constructs the comparison of short exact sequences. If its left component were noninvertible, the factorization hypothesis and the cokernel property would split the right almost-split terminal map. Thus the left component is invertible, and the short five lemma makes the middle component invertible as well.