Existence of almost-split sequences over a finite-dimensional algebra

Let A be a finite-dimensional algebra over a field k. This file proves the existence half of the Auslander–Reiten theorem: every finitely generated indecomposable non-projective A-module M ends an almost-split sequence

0 → τ M → E → M → 0,

whose left-hand end is the Auslander–Reiten translate τ M = ModuleCat.arTranslate k M and whose middle term is finitely generated (ModuleCat.exists_isAlmostSplit_arTranslate). Dually, every finitely generated indecomposable non-injective module starts an almost-split sequence with finitely generated middle term and right-hand end (ModuleCat.exists_isAlmostSplit_of_not_injective).

Both lifting properties hold in the category of all A-modules, not only the finitely generated ones, and the field is arbitrary. A finitely generated module therefore ends an almost-split sequence exactly when it is indecomposable and non-projective, and starts one exactly when it is indecomposable and non-injective.

By CategoryTheory.ShortComplex.IsAlmostSplit.nonempty_iso, the sequence ending at M is unique up to isomorphism among the almost-split sequences ending at M whose left-hand end has a local endomorphism ring, for instance a finitely generated one.

The sequence is obtained from a minimal projective presentation P₁ → P₀ → M → 0: the Auslander–Reiten translate of the presentation starts a short exact sequence ending at P₀ ⧸ im(P₁) whose first map is left almost split (LinearMap.exists_isLeftAlmostSplit_translate). Since M has a local endomorphism ring, a non-split sequence with left almost-split first map is almost split (CategoryTheory.ShortComplex.ShortExact.isAlmostSplit_iff_isLeftAlmostSplit).

References

• M. Auslander, I. Reiten, Representation theory of Artin algebras III: almost split sequences, Comm. Algebra 3 (1975), 239–294.
• M. Auslander, I. Reiten, S. O. Smalø, Representation Theory of Artin Algebras, Cambridge University Press (1995), Section V.1.

theorem ModuleCat.exists_isAlmostSplit_arTranslate (k : Type u) {A : Type v} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (M : ModuleCat A) [Module.Finite A ↑M] (hiM : CategoryTheory.Indecomposable M) (hpM : ¬CategoryTheory.Projective M) : ∃ (E : ModuleCat A) (i : arTranslate k M ⟶ E) (p : E ⟶ M) (h : CategoryTheory.CategoryStruct.comp i p = 0), Module.Finite A ↑E ∧ { X₁ := arTranslate k M, X₂ := E, X₃ := M, f := i, g := p, zero := h }.IsAlmostSplit

The Auslander–Reiten theorem, existence. Over a finite-dimensional algebra, a finitely generated indecomposable non-projective module M ends an almost-split sequence 0 → τ M → E → M → 0 of A-modules whose left-hand end is the translate τ M and whose middle term is finitely generated.

theorem ModuleCat.exists_isAlmostSplit_X₃_eq_iff (k : Type u) {A : Type v} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (M : ModuleCat A) [Module.Finite A ↑M] : (∃ (S : CategoryTheory.ShortComplex (ModuleCat A)), S.X₃ = M ∧ S.IsAlmostSplit) ↔ CategoryTheory.Indecomposable M ∧ ¬CategoryTheory.Projective M

Over a finite-dimensional algebra, a finitely generated module ends an almost-split sequence of A-modules exactly when it is indecomposable and non-projective.

theorem ModuleCat.exists_isAlmostSplit_of_not_injective (k : Type u) {A : Type v} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (N : ModuleCat A) [Module.Finite A ↑N] (hiN : CategoryTheory.Indecomposable N) (hinj : ¬CategoryTheory.Injective N) : ∃ (E : ModuleCat A) (M : ModuleCat A) (i : N ⟶ E) (p : E ⟶ M) (h : CategoryTheory.CategoryStruct.comp i p = 0), Module.Finite A ↑E ∧ Module.Finite A ↑M ∧ { X₁ := N, X₂ := E, X₃ := M, f := i, g := p, zero := h }.IsAlmostSplit

The Auslander–Reiten theorem, existence on the left. Over a finite-dimensional algebra, a finitely generated indecomposable non-injective module N starts an almost-split sequence 0 → N → E → M → 0 of A-modules with E and M finitely generated.

theorem ModuleCat.exists_isAlmostSplit_X₁_eq_iff (k : Type u) {A : Type v} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (N : ModuleCat A) [Module.Finite A ↑N] : (∃ (S : CategoryTheory.ShortComplex (ModuleCat A)), S.X₁ = N ∧ S.IsAlmostSplit) ↔ CategoryTheory.Indecomposable N ∧ ¬CategoryTheory.Injective N

Over a finite-dimensional algebra, a finitely generated module starts an almost-split sequence of A-modules exactly when it is indecomposable and non-injective.