Documentation

TauCeti.Algebra.Category.ModuleCat.AuslanderReiten.Translate

The Auslander–Reiten translate of a module #

For a finitely generated module M over a finite-dimensional algebra A over a field k, ModuleCat.arTranslate k M is D Tr of a chosen finite minimal projective presentation of M, as an object of ModuleCat A. It is finitely generated, independent of the minimal presentation up to isomorphism (ModuleCat.nonempty_iso_arTranslate), and zero exactly when M is projective. For indecomposable M, it is indecomposable exactly when M is non-projective, and it is injective exactly when M is projective. On non-projective indecomposables it detects isomorphism classes (ModuleCat.nonempty_iso_arTranslate_iff), and every non-injective indecomposable is a translate (ModuleCat.exists_nonempty_iso_arTranslate).

The presentation-level construction TauCeti.AuslanderReitenTranslate and its properties are in TauCeti/Algebra/Module/AuslanderReiten/; this file chooses the presentation, so that the translate becomes a function of the module.

The field is arbitrary and the algebra may be noncommutative. The module lives in a universe containing those of the field and the algebra, as do its transpose and their linear duals.

References #

source
noncomputable def ModuleCat.arTranslate (k : Type u) {A : Type v} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (M : ModuleCat A) [Module.Finite A ↑M] :
ModuleCat A

The Auslander–Reiten translate τ M = D Tr M of a finitely generated module, formed from a chosen finite minimal projective presentation.

Instances For
    source
    theorem ModuleCat.nonempty_iso_arTranslate (k : Type u) {A : Type v} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (M : ModuleCat A) [Module.Finite A ↑M] (P : TauCeti.FiniteProjectivePresentation M) (hP : TauCeti.IsMinimalProjectivePresentation P.p P.π) :
    Nonempty (arTranslate k M ≅ ↧(TauCeti.AuslanderReitenTranslate k P.p))

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

    source
    theorem ModuleCat.nonempty_iso_arTranslate_of_iso (k : Type u) {A : Type v} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] {M N : ModuleCat A} [Module.Finite A ↑M] [Module.Finite A ↑N] (e : M ≅ N) :
    Nonempty (arTranslate k M ≅ arTranslate k N)

    Isomorphic modules have isomorphic Auslander–Reiten translates.

    source
    instance ModuleCat.instFiniteCarrierArTranslate (k : Type u) {A : Type v} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (M : ModuleCat A) [Module.Finite A ↑M] :
    Module.Finite A ↑(arTranslate k M)
    source
    @[simp]
    theorem ModuleCat.isZero_arTranslate_iff (k : Type u) {A : Type v} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (M : ModuleCat A) [Module.Finite A ↑M] :
    CategoryTheory.Limits.IsZero (arTranslate k M) ↔ CategoryTheory.Projective M

    The translate vanishes precisely on the projective modules.

    source
    @[simp]
    theorem ModuleCat.indecomposable_arTranslate_iff (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) :
    CategoryTheory.Indecomposable (arTranslate k M) ↔ ¬CategoryTheory.Projective M

    The translate of a finitely generated indecomposable module is indecomposable exactly when the module is not projective.

    source
    @[simp]
    theorem ModuleCat.injective_arTranslate_iff (k : Type u) {A : Type v} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (M : ModuleCat A) [Module.Finite A ↑M] :
    CategoryTheory.Injective (arTranslate k M) ↔ CategoryTheory.Projective M

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

    source
    theorem ModuleCat.nonempty_iso_arTranslate_iff (k : Type u) {A : Type v} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] {M N : ModuleCat A} [Module.Finite A ↑M] [Module.Finite A ↑N] (hiM : CategoryTheory.Indecomposable M) (hiN : CategoryTheory.Indecomposable N) (hpM : ¬CategoryTheory.Projective M) :
    Nonempty (arTranslate k M ≅ arTranslate k N) ↔ Nonempty (M ≅ N)

    On finitely generated indecomposables, with a non-projective source, isomorphism of Auslander–Reiten translates is equivalent to isomorphism of the modules.

    source
    theorem ModuleCat.exists_nonempty_iso_arTranslate (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) :
    ∃ (M : ModuleCat A) (x : Module.Finite A ↑M), CategoryTheory.Indecomposable M ∧ ¬CategoryTheory.Projective M ∧ Nonempty (arTranslate k M ≅ N)

    Every finitely generated non-injective indecomposable module is, up to isomorphism, the translate of a finitely generated non-projective indecomposable module.