Uniqueness of the almost-split sequence at a given end

An almost-split sequence 0 ⟶ A ⟶ B ⟶ C ⟶ 0 whose left-hand end has local endomorphism ring is determined by its right-hand end C: two such almost-split sequences with isomorphic right-hand ends are isomorphic as short complexes, so in particular their left-hand ends and their middle terms are isomorphic. This file proves that, the uniqueness half of the Auslander-Reiten theorem, and proves it in the sharper form that every morphism between two such almost-split sequences that is invertible at the right-hand end is invertible. Concretely, every uniqueness statement below carries [IsLocalRing (End S.X₁)] together with [IsLocalRing (End S'.X₁)] for the second sequence, in a preadditive and balanced ambient category; none of these conclusions is claimed for an arbitrary almost-split sequence in an arbitrary preadditive category. Only the comparison morphism CategoryTheory.ShortComplex.IsAlmostSplit.exists_hom_τ₃_eq, which produces a morphism and asserts nothing about its invertibility, is free of the locality hypotheses.

Two inputs beyond the definition are therefore needed, and both are hypotheses rather than ambient assumptions. The category is asked to be preadditive and balanced, which is what makes the left-hand end of a short exact sequence a kernel of its second map (ShortComplex.Exact.lift' is stated only for a balanced category) and lets a morphism that is both monic and epic be inverted. And the endomorphism ring of each left-hand end is asked to be local, the Krull-Schmidt input. An almost-split sequence does have an indecomposable left-hand end (TauCeti.IsLeftAlmostSplit.indecomposable), but indecomposability in a general preadditive category does not give locality. What it gives, once idempotents split — over an idempotent-complete category with binary biproducts, for instance any abelian one — is that the object is nonzero and has no idempotent endomorphism other than 0 and the identity (TauCeti.indecomposable_iff_idempotent_eq_zero_or_id), and that is strictly weaker: a ring whose only idempotents are 0 and 1 need not be local. Indecomposability becomes equivalent to locality of the endomorphism ring for a module of finite length — in particular for a finite-dimensional module over a finite-dimensional algebra — which is Fitting's lemma, available here for objects of ModuleCat A as TauCeti.indecomposable_iff_isLocalRing_end; that is how a use site over such an algebra discharges the hypothesis.

The three lemmas the argument runs on need only one half of the almost-split condition — exactness, monicity of the first map, and TauCeti.IsLeftAlmostSplit or TauCeti.IsRightAlmostSplit — so they are stated in those namespaces; the results about an almost-split sequence are their corollaries. Only TauCeti.IsLeftAlmostSplit.isIso_of_τ₃_eq_id, whose five-lemma step needs the second map to be an epimorphism, asks for full short exactness.

Main results

• TauCeti.IsLeftAlmostSplit.isIso_τ₁_of_τ₃_eq_id: an endomorphism of an exact short complex with monic, left almost split first map that is the identity on the right-hand end is an isomorphism on the left-hand end, and TauCeti.IsLeftAlmostSplit.isIso_of_τ₃_eq_id: it is then an isomorphism of short complexes. This is the engine of the file.
• TauCeti.IsRightAlmostSplit.exists_hom_τ₃_eq_of_not_isSplitEpi: the comparison morphism. A map into the right-hand end of an exact short complex with monic first map and right almost split second map, whose composite with the first sequence's g is not a split epimorphism, is the third component of a morphism of short complexes; CategoryTheory.ShortComplex.IsAlmostSplit.exists_hom_τ₃_eq is the case of an isomorphism between the right-hand ends of two almost-split sequences.
• CategoryTheory.ShortComplex.IsAlmostSplit.isIso_of_isIso_τ₃: a morphism between two almost-split sequences with local left-hand endomorphism rings that is invertible at the right-hand end is invertible, the sharp form of uniqueness.
• CategoryTheory.ShortComplex.IsAlmostSplit.exists_iso_τ₃_eq: uniqueness. An isomorphism between the right-hand ends of two almost-split sequences with local left-hand endomorphism rings is realized by an isomorphism of the sequences, so such a sequence is unique under its right-hand end; the plainer statement is CategoryTheory.ShortComplex.IsAlmostSplit.nonempty_iso, with CategoryTheory.ShortComplex.IsAlmostSplit.nonempty_iso_X₁ and .nonempty_iso_X₂ the statements about the left-hand ends and the middle terms that the Auslander-Reiten theorem is usually quoted in.

References

• M. Auslander, I. Reiten, S. Smalø, Representation Theory of Artin Algebras, CUP (1995), V.1.
• I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, LMS Student Texts 65, CUP (2006), IV.1.13.

Endomorphisms fixing the right-hand end

theorem TauCeti.IsLeftAlmostSplit.isIso_τ₁_of_τ₃_eq_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Balanced C] {S : CategoryTheory.ShortComplex C} (hf : IsLeftAlmostSplit S.f) (hS : S.Exact) [CategoryTheory.Mono S.f] [IsLocalRing (CategoryTheory.End S.X₁)] (φ : S ⟶ S) (hφ : φ.τ₃ = CategoryTheory.CategoryStruct.id S.X₃) : CategoryTheory.IsIso φ.τ₁

An endomorphism of an exact short complex with monic, left almost split first map acting as the identity on the right-hand end is an isomorphism on the left-hand end. This is the engine of the uniqueness statements below.

theorem TauCeti.IsLeftAlmostSplit.isIso_of_τ₃_eq_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Balanced C] {S : CategoryTheory.ShortComplex C} (hf : IsLeftAlmostSplit S.f) (hS : S.ShortExact) [IsLocalRing (CategoryTheory.End S.X₁)] (φ : S ⟶ S) (hφ : φ.τ₃ = CategoryTheory.CategoryStruct.id S.X₃) : CategoryTheory.IsIso φ

An endomorphism of a short exact sequence with left almost split first map acting as the identity on the right-hand end is an isomorphism.

The comparison morphism

theorem TauCeti.IsRightAlmostSplit.exists_hom_τ₃_eq_of_not_isSplitEpi {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Balanced C] {S S' : CategoryTheory.ShortComplex C} (hg : IsRightAlmostSplit S'.g) (hS' : S'.Exact) [CategoryTheory.Mono S'.f] (e : S.X₃ ⟶ S'.X₃) (he : ¬CategoryTheory.IsSplitEpi (CategoryTheory.CategoryStruct.comp S.g e)) : ∃ (φ : S ⟶ S'), φ.τ₃ = e

A map e into the right-hand end of an exact short complex S' with monic first map and right almost split second map extends to a morphism of short complexes S ⟶ S', as soon as S.g ≫ e is not a split epimorphism. No hypothesis on S beyond its being a short complex is needed.

Uniqueness

theorem CategoryTheory.ShortComplex.IsAlmostSplit.exists_hom_τ₃_eq {C : Type u} [Category.{v, u} C] [Preadditive C] [Balanced C] {S S' : ShortComplex C} (hS : S.IsAlmostSplit) (hS' : S'.IsAlmostSplit) (e : S.X₃ ≅ S'.X₃) : ∃ (φ : S ⟶ S'), φ.τ₃ = e.hom

An isomorphism between the right-hand ends of two almost-split sequences is the third component of a morphism of short complexes between them.

theorem CategoryTheory.ShortComplex.IsAlmostSplit.isIso_of_isIso_τ₃ {C : Type u} [Category.{v, u} C] [Preadditive C] [Balanced C] {S S' : ShortComplex C} (hS : S.IsAlmostSplit) (hS' : S'.IsAlmostSplit) [IsLocalRing (End S.X₁)] [IsLocalRing (End S'.X₁)] (φ : S ⟶ S') [IsIso φ.τ₃] : IsIso φ

A morphism of almost-split sequences that is invertible at the right-hand end is invertible, the sharp form of uniqueness.

theorem CategoryTheory.ShortComplex.IsAlmostSplit.exists_iso_τ₃_eq {C : Type u} [Category.{v, u} C] [Preadditive C] [Balanced C] {S S' : ShortComplex C} (hS : S.IsAlmostSplit) (hS' : S'.IsAlmostSplit) [IsLocalRing (End S.X₁)] [IsLocalRing (End S'.X₁)] (e : S.X₃ ≅ S'.X₃) : ∃ (f : S ≅ S'), f.hom.τ₃ = e.hom

Uniqueness of the almost-split sequence at a given right-hand end, in its sharp form: an isomorphism between the right-hand ends of two almost-split sequences is realized by an isomorphism of the sequences themselves. The sequence ending at an object is therefore determined up to isomorphism under that object, not merely up to abstract isomorphism.

theorem CategoryTheory.ShortComplex.IsAlmostSplit.nonempty_iso {C : Type u} [Category.{v, u} C] [Preadditive C] [Balanced C] {S S' : ShortComplex C} (hS : S.IsAlmostSplit) (hS' : S'.IsAlmostSplit) [IsLocalRing (End S.X₁)] [IsLocalRing (End S'.X₁)] (e : S.X₃ ≅ S'.X₃) : Nonempty (S ≅ S')

Uniqueness of the almost-split sequence at a given right-hand end: two almost-split sequences whose right-hand ends are isomorphic are isomorphic as short complexes.

theorem CategoryTheory.ShortComplex.IsAlmostSplit.nonempty_iso_X₁ {C : Type u} [Category.{v, u} C] [Preadditive C] [Balanced C] {S S' : ShortComplex C} (hS : S.IsAlmostSplit) (hS' : S'.IsAlmostSplit) [IsLocalRing (End S.X₁)] [IsLocalRing (End S'.X₁)] (e : S.X₃ ≅ S'.X₃) : Nonempty (S.X₁ ≅ S'.X₁)

The left-hand ends of two almost-split sequences with isomorphic right-hand ends are isomorphic: the object τ M of the Auslander-Reiten theorem is determined by M up to isomorphism.

theorem CategoryTheory.ShortComplex.IsAlmostSplit.nonempty_iso_X₂ {C : Type u} [Category.{v, u} C] [Preadditive C] [Balanced C] {S S' : ShortComplex C} (hS : S.IsAlmostSplit) (hS' : S'.IsAlmostSplit) [IsLocalRing (End S.X₁)] [IsLocalRing (End S'.X₁)] (e : S.X₃ ≅ S'.X₃) : Nonempty (S.X₂ ≅ S'.X₂)

The middle terms of two almost-split sequences with isomorphic right-hand ends are isomorphic: the middle term of the Auslander-Reiten sequence ending at M, which carries the irreducible morphisms into M, is determined by M up to isomorphism.