Irreducible maps in almost-split sequences

A left minimal left almost-split map that is not split epic is irreducible; dually, a right minimal right almost-split map that is not split monic is irreducible. These criteria identify irreducible maps in almost-split sequences from minimality and the complementary non-splitting condition.

These are standard criteria for irreducible maps; see Auslander, Reiten and Smalø, Representation Theory of Artin Algebras, V.5.

theorem TauCeti.IsLeftAlmostSplit.isIrreducibleMorphism_of_minimal {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (hf : IsLeftAlmostSplit f) (hnot : ¬CategoryTheory.IsSplitEpi f) (hmin : ∀ (u : Y ⟶ Y), CategoryTheory.CategoryStruct.comp f u = f → CategoryTheory.IsIso u) : IsIrreducibleMorphism f

A left minimal left almost-split map that is not split epic is irreducible. Left minimality says that every endomorphism of the target fixing the map is invertible.

theorem TauCeti.IsRightAlmostSplit.isIrreducibleMorphism_of_minimal {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} (hf : IsRightAlmostSplit f) (hnot : ¬CategoryTheory.IsSplitMono f) (hmin : ∀ (u : X ⟶ X), CategoryTheory.CategoryStruct.comp u f = f → CategoryTheory.IsIso u) : IsIrreducibleMorphism f

A right minimal right almost-split map that is not split monic is irreducible. Right minimality says that every endomorphism of the source fixing the map is invertible.