Documentation

TauCeti.Algebra.Category.ModuleCat.AuslanderReiten.LeftAlmostSplit

Left almost-split sequences from Auslander–Reiten duality #

If the translate T = D Tr(f) of a finite projective presentation over a finite-dimensional algebra is noninjective and has local endomorphism ring, there is a nonsplit short exact sequence 0 → T → E → coker f → 0 whose first map is left almost split. Its middle term is finitely generated. The factorization property holds against all modules, not just finitely generated ones.

The extension class supplied by LinearMap.exists_auslanderReitenExt_ne_zero is realized by pushing out the image presentation of f. Vanishing of its pushforwards gives the left almost-split property. The result does not assert that the first map is left minimal or that the second map is right almost split.

References #

theorem LinearMap.exists_isLeftAlmostSplit_translate {k : Type u} {A : Type v} [Field k] [Ring A] [Algebra k A] [Module.Finite k A] {P₀ P₁ : Type (max u v w)} [AddCommGroup P₀] [Module A P₀] [Module.Finite A P₀] [Module.Projective A P₀] [AddCommGroup P₁] [Module A P₁] [Module.Finite A P₁] [Module.Projective A P₁] (f : P₁ →ₗ[A] P₀) [IsLocalRing (CategoryTheory.End ↧(TauCeti.AuslanderReitenTranslate k f))] (hi : ¬CategoryTheory.Injective ↧(TauCeti.AuslanderReitenTranslate k f)) :
∃ (E : ModuleCat A) (i : ↧(TauCeti.AuslanderReitenTranslate k f) ⟶ E) (p : E ⟶ ↧(P₀ ⧸ f.range)) (h : CategoryTheory.CategoryStruct.comp i p = 0), { X₁ := ↧(TauCeti.AuslanderReitenTranslate k f), X₂ := E, X₃ := ↧(P₀ ⧸ f.range), f := i, g := p, zero := h }.ShortExact ∧ Module.Finite A ↑E ∧ TauCeti.IsLeftAlmostSplit i

A noninjective Auslander–Reiten translate with local endomorphism ring starts a short exact sequence with finitely generated middle term and a left almost-split first map. The presentation need not be minimal, and the field need not be algebraically closed.