Minimal morphisms and almost-split sequences

In an abelian category, a short exact sequence whose final map is right almost split and right minimal is almost split. Dually, left almost splitness and left minimality of the initial map suffice. These criteria let a construction of an almost-split sequence supply only one of its two lifting properties.

Minimality is stated explicitly: an endomorphism fixing the specified map is invertible. This agrees with the convention in TauCeti.CategoryTheory.AlmostSplit.Irreducible. No finite-length or locality hypothesis is needed when minimality is supplied. If the opposite end has a local endomorphism ring, non-splitness already implies minimality, so a single almost-split lifting property suffices. Conversely, the maps of an almost-split sequence are minimal when the opposite end has a local endomorphism ring.

The pushout argument uses TauCeti.shortExact_cobaseChange.

References

• M. Auslander, I. Reiten, S. Smalø, Representation Theory of Artin Algebras, V.1.

theorem TauCeti.IsRightAlmostSplit.isLeftAlmostSplit_of_minimal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex C} (hg : IsRightAlmostSplit S.g) (hS : S.ShortExact) (hmin : ∀ (b : S.X₂ ⟶ S.X₂), CategoryTheory.CategoryStruct.comp b S.g = S.g → CategoryTheory.IsIso b) : IsLeftAlmostSplit S.f

In a short exact sequence, right almost splitness and right minimality of the final map imply left almost splitness of the initial map.

theorem TauCeti.IsLeftAlmostSplit.isRightAlmostSplit_of_minimal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex C} (hf : IsLeftAlmostSplit S.f) (hS : S.ShortExact) (hmin : ∀ (b : S.X₂ ⟶ S.X₂), CategoryTheory.CategoryStruct.comp S.f b = S.f → CategoryTheory.IsIso b) : IsRightAlmostSplit S.g

In a short exact sequence, left almost splitness and left minimality of the initial map imply right almost splitness of the final map.

theorem CategoryTheory.ShortComplex.IsAlmostSplit.isIso_of_comp_g_eq {C : Type u} [Category.{v, u} C] [Preadditive C] [Balanced C] {S : ShortComplex C} (hS : S.IsAlmostSplit) [IsLocalRing (End S.X₁)] (b : S.X₂ ⟶ S.X₂) (hb : CategoryStruct.comp b S.g = S.g) : IsIso b

The final map of an almost-split sequence is right minimal when the left-hand end has a local endomorphism ring.

theorem CategoryTheory.ShortComplex.IsAlmostSplit.isIso_of_f_comp_eq {C : Type u} [Category.{v, u} C] [Preadditive C] [Balanced C] {S : ShortComplex C} (hS : S.IsAlmostSplit) [IsLocalRing (End S.X₃)] (b : S.X₂ ⟶ S.X₂) (hb : CategoryStruct.comp S.f b = S.f) : IsIso b

The initial map of an almost-split sequence is left minimal when the right-hand end has a local endomorphism ring.

theorem CategoryTheory.ShortComplex.ShortExact.isAlmostSplit_of_isRightAlmostSplit {C : Type u} [Category.{v, u} C] [Abelian C] {S : ShortComplex C} (hS : S.ShortExact) (hg : TauCeti.IsRightAlmostSplit S.g) (hmin : ∀ (b : S.X₂ ⟶ S.X₂), CategoryStruct.comp b S.g = S.g → IsIso b) : S.IsAlmostSplit

A short exact sequence with a right minimal right almost split final map is almost split.

theorem CategoryTheory.ShortComplex.ShortExact.isAlmostSplit_of_isLeftAlmostSplit {C : Type u} [Category.{v, u} C] [Abelian C] {S : ShortComplex C} (hS : S.ShortExact) (hf : TauCeti.IsLeftAlmostSplit S.f) (hmin : ∀ (b : S.X₂ ⟶ S.X₂), CategoryStruct.comp S.f b = S.f → IsIso b) : S.IsAlmostSplit

A short exact sequence with a left minimal left almost split initial map is almost split.

theorem CategoryTheory.ShortComplex.ShortExact.isAlmostSplit_iff_isRightAlmostSplit {C : Type u} [Category.{v, u} C] [Abelian C] {S : ShortComplex C} (hS : S.ShortExact) [IsLocalRing (End S.X₁)] : S.IsAlmostSplit ↔ TauCeti.IsRightAlmostSplit S.g

A short exact sequence with local left-hand endomorphism ring is almost split exactly when its final map is right almost split. No separate minimality assumption is needed.

theorem CategoryTheory.ShortComplex.ShortExact.isAlmostSplit_iff_isLeftAlmostSplit {C : Type u} [Category.{v, u} C] [Abelian C] {S : ShortComplex C} (hS : S.ShortExact) [IsLocalRing (End S.X₃)] : S.IsAlmostSplit ↔ TauCeti.IsLeftAlmostSplit S.f

A short exact sequence with local right-hand endomorphism ring is almost split exactly when its initial map is left almost split. No separate minimality assumption is needed.

theorem TauCeti.IsRightAlmostSplit.exists_iso_of_minimal {C : Type u} [CategoryTheory.Category.{v, u} C] {X X' Y : C} {f : X ⟶ Y} {g : X' ⟶ Y} (hf : IsRightAlmostSplit f) (hg : IsRightAlmostSplit g) (hminf : ∀ (b : X ⟶ X), CategoryTheory.CategoryStruct.comp b f = f → CategoryTheory.IsIso b) (hming : ∀ (b : X' ⟶ X'), CategoryTheory.CategoryStruct.comp b g = g → CategoryTheory.IsIso b) : ∃ (e : X ≅ X'), CategoryTheory.CategoryStruct.comp e.hom g = f

Two right minimal right almost-split morphisms f : X ⟶ Y and g : X' ⟶ Y have an isomorphism e : X ≅ X' satisfying e.hom ≫ g = f.