The Auslander–Reiten translate of a quiver representation

For a quiver with finitely many paths, arTranslate k Q M hM is the representation corresponding to the translate ModuleCat.arTranslate of the path-algebra module of M, that is, to D Tr of a chosen finite minimal projective presentation of that module. It is pointwise finite-dimensional, independent of the minimal presentation up to isomorphism, and zero exactly when M is projective. For indecomposable M, it is indecomposable exactly when M is non-projective, and every nonzero value is non-injective. These properties allow the translate to act on isomorphism classes of indecomposables and provide the endpoints of almost-split sequences. On non-projective indecomposables, it detects isomorphism classes. AR duality and the inverse correspondence are separate results.

The field is arbitrary. Vertex and arrow universes are independent of the field universe. The vertex spaces lie in a universe containing the field and the path algebra, as do the transpose and its linear dual.

References

• M. Auslander, I. Reiten, S. O. Smalø, Representation Theory of Artin Algebras, Cambridge University Press (1995), Section IV.1.

noncomputable def TauCeti.arTranslate (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite (Quiver.TotalPath Q)] (M : QuiverRep k Q) (hM : IsFinDim k Q M) : QuiverRep k Q

The Auslander–Reiten translate τ M = D Tr M of a pointwise finite-dimensional representation: the translate of its path-algebra module, read back as a representation.

theorem TauCeti.arTranslate_eq_quiverRepFunctor_obj (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite (Quiver.TotalPath Q)] (M : QuiverRep k Q) (hM : IsFinDim k Q M) : have this := ⋯; arTranslate k Q M hM = (quiverRepFunctor k Q).obj (ModuleCat.arTranslate k ((quiverRepEquivalence k Q).functor.obj M))

The quiver translate is the module translate transported through the path-algebra equivalence.

theorem TauCeti.nonempty_iso_arTranslate (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite (Quiver.TotalPath Q)] (M : QuiverRep k Q) (hM : IsFinDim k Q M) (P : FiniteProjectivePresentation ((quiverRepEquivalence k Q).functor.obj M)) (hP : IsMinimalProjectivePresentation P.p P.π) : Nonempty (arTranslate k Q M hM ≅ (quiverRepFunctor k Q).obj ↧(AuslanderReitenTranslate k P.p))

Any finite minimal projective presentation computes the same translate up to isomorphism. This characterizes arTranslate without referring to its chosen presentation.

theorem TauCeti.nonempty_iso_arTranslate_of_iso (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite (Quiver.TotalPath Q)] {M N : QuiverRep k Q} (hM : IsFinDim k Q M) (hN : IsFinDim k Q N) (e : M ≅ N) : Nonempty (arTranslate k Q M hM ≅ arTranslate k Q N hN)

Isomorphic representations have isomorphic Auslander–Reiten translates.

theorem TauCeti.isFinDim_arTranslate (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite (Quiver.TotalPath Q)] (M : QuiverRep k Q) (hM : IsFinDim k Q M) : IsFinDim k Q (arTranslate k Q M hM)

The Auslander–Reiten translate stays within the pointwise finite-dimensional representations.

@[simp]

theorem TauCeti.isZero_arTranslate_iff (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite (Quiver.TotalPath Q)] (M : QuiverRep k Q) (hM : IsFinDim k Q M) : CategoryTheory.Limits.IsZero (arTranslate k Q M hM) ↔ CategoryTheory.Projective M

The translate vanishes precisely on the projective representations.

@[simp]

theorem TauCeti.indecomposable_arTranslate_iff (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite (Quiver.TotalPath Q)] (M : QuiverRep k Q) (hM : IsFinDim k Q M) (hiM : CategoryTheory.Indecomposable M) : CategoryTheory.Indecomposable (arTranslate k Q M hM) ↔ ¬CategoryTheory.Projective M

The translate of a finite-dimensional indecomposable representation is indecomposable exactly when the representation is not projective.

@[simp]

theorem TauCeti.injective_arTranslate_iff (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite (Quiver.TotalPath Q)] (M : QuiverRep k Q) (hM : IsFinDim k Q M) : CategoryTheory.Injective (arTranslate k Q M hM) ↔ CategoryTheory.Projective M

The translate is injective exactly when the original representation is projective. Consequently every nonzero translate is non-injective.

theorem TauCeti.nonempty_iso_arTranslate_iff (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite (Quiver.TotalPath Q)] {M N : QuiverRep k Q} (hM : IsFinDim k Q M) (hN : IsFinDim k Q N) (hiM : CategoryTheory.Indecomposable M) (hiN : CategoryTheory.Indecomposable N) (hpM : ¬CategoryTheory.Projective M) : Nonempty (arTranslate k Q M hM ≅ arTranslate k Q N hN) ↔ Nonempty (M ≅ N)

On finite-dimensional indecomposables, with a non-projective source, isomorphism of Auslander–Reiten translates is equivalent to isomorphism of the representations.

theorem TauCeti.exists_nonempty_iso_arTranslate (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite (Quiver.TotalPath Q)] (N : QuiverRep k Q) (hN : IsFinDim k Q N) (hiN : CategoryTheory.Indecomposable N) (hinj : ¬CategoryTheory.Injective N) : ∃ (M : QuiverRep k Q) (hM : IsFinDim k Q M), CategoryTheory.Indecomposable M ∧ ¬CategoryTheory.Projective M ∧ Nonempty (arTranslate k Q M hM ≅ N)

Every finite-dimensional non-injective indecomposable representation is the translate of a finite-dimensional non-projective indecomposable representation.