Extension classes and left almost-split maps

The first map of a short exact sequence is left almost split exactly when its extension class is nonzero and is killed by pushforward along every map out of the first term that is not a split monomorphism. This converts an extension class constructed by Auslander–Reiten duality into the factorization property of an actual sequence.

The factorization test uses the kernel of TauCeti.homBoundary, computed from Mathlib's contravariant long exact Ext sequence. No finiteness or linearity assumption is needed.

When the right-hand end has a local endomorphism ring, the same condition characterizes almost-split sequences (CategoryTheory.ShortComplex.ShortExact.isAlmostSplit_iff_extClass).

References

• M. Auslander, I. Reiten, S. O. Smalø, Representation Theory of Artin Algebras, Cambridge University Press (1995), Section V.1.

theorem CategoryTheory.ShortComplex.ShortExact.isLeftAlmostSplit_f_iff_extClass {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {S : ShortComplex C} (hS : S.ShortExact) : TauCeti.IsLeftAlmostSplit S.f ↔ hS.extClass ≠ 0 ∧ ∀ (N : C) (g : S.X₁ ⟶ N), ¬IsSplitMono g → hS.extClass.comp (Abelian.Ext.mk₀ g) ⋯ = 0

A short exact sequence starts with a left almost-split map exactly when its class is nonzero and every pushforward along a map that is not a split monomorphism vanishes.

theorem CategoryTheory.ShortComplex.ShortExact.isAlmostSplit_iff_extClass {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {S : ShortComplex C} (hS : S.ShortExact) [IsLocalRing (End S.X₃)] : S.IsAlmostSplit ↔ hS.extClass ≠ 0 ∧ ∀ (N : C) (g : S.X₁ ⟶ N), ¬IsSplitMono g → hS.extClass.comp (Abelian.Ext.mk₀ g) ⋯ = 0

The extension-class criterion in an abelian category: a short exact sequence with local right-hand endomorphism ring is almost split exactly when its class is nonzero and is killed by pushforward along every map out of the first term that is not a split monomorphism.