The Auslander--Reiten translate

For an algebra A over a commutative semiring k, the duality D = Hom_k(-, k) turns a right A-module into a left A-module, by TauCeti.dualRightAction. This file applies that duality to the Auslander--Reiten transpose to define the Auslander--Reiten translate

τ M = D (Tr M)

of a module M presented by a minimal projective presentation P₁ → P₀ → M → 0, the k-dual of the Auslander--Reiten transpose TauCeti.AuslanderReitenTranspose of that presentation. The transpose is a right A-module, so the translate is a left A-module again, as M was.

The translate is attached to a presentation, not directly to M: like the transpose it is well defined only because a minimal projective presentation is unique up to isomorphism of the whole diagram. TauCeti.IsMinimalProjectivePresentation.nonempty_linearEquiv_auslanderReitenTranslate is that statement, and it is what licenses the notation τ M.

Main definitions

• TauCeti.AuslanderReitenTranslate: the k-dual D (Tr) of the Auslander--Reiten transpose of a linear map p₁ : P₁ → P₀, carrying the resulting A-module structure. It is the Auslander--Reiten translate of M when p₁ is the first map of a minimal projective presentation of M.
• TauCeti.AuslanderReitenTranslate.linearEquiv: the transport of the translate along an isomorphism of transposes, contravariant by TauCeti.AuslanderReitenTranslate.linearEquiv_trans.

Main results

• TauCeti.IsMinimalProjectivePresentation.nonempty_linearEquiv_auslanderReitenTranslate: the translate is independent, up to A-linear equivalence, of the chosen minimal projective presentation.
• TauCeti.IsMinimalProjectivePresentation.subsingleton_auslanderReitenTranslate_of_projective: the translate of a projective module vanishes.
• TauCeti.IsMinimalProjectivePresentation.subsingleton_auslanderReitenTranslate_iff_projective: for a finitely generated left-hand source and a transpose projective over the base, the converse holds too — the translate vanishes exactly on the projective modules — so that τ assigns a nonzero module to every non-projective one.
• TauCeti.AuslanderReitenTranslate.isIndecomposableModule_iff: when the transpose is reflexive over a commutative base ring, the translate is indecomposable exactly when the transpose is.

Implementation notes

TauCeti.dualRightAction is a plain ring homomorphism rather than a Module instance on every dual, for the reasons recorded in TauCeti/LinearAlgebra/Dual/RightAction.lean; the single Module instance built from it is the one on the translate, whose underlying transpose pins the right-module structure being dualized.

The translate is a reducible abbreviation of the dual rather than a fresh type, so that its elements are literally k-linear functionals on the transpose and the whole Module.Dual API applies to it unchanged: extensionality, the dimension count Subspace.dual_finrank_eq and the finite-dimensionality of a dual are inherited verbatim and are not restated here. Only the A-action is new, and it is described by the single lemma TauCeti.AuslanderReitenTranslate.smul_apply.

The name arTranslate is deliberately left free: the roadmap pins it for the object-level translate arTranslate k Q M of a representation, which this presentation-level construction will supply once the stable category is available.

References

This is the arTranslate M = D (Tr M) construction of sublayer 6D, "the AR translate τ = D Tr and AR duality", of Layer 6 of the quiver-representations roadmap, which names it as the composite of the transpose of sublayer 6C with the duality D = Hom_k(-, k), "well-defined only up to projectives, through minimal presentations and duality on finite-dimensional modules".

AR duality itself, and the bijection it yields from non-projective indecomposables to non-injective indecomposables with inverse Tr D, is not proved here: it needs the finite-dimensional hypotheses and the stable morphism spaces that sublayer 6C supplies.

• M. Auslander, I. Reiten, S. O. Smalø, Representation Theory of Artin Algebras, Cambridge University Press (1995), Section IV.1.
• I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, Cambridge University Press (2006), Section IV.2.

@[reducible, inline]

abbrev TauCeti.AuslanderReitenTranslate {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] (k : Type x) [CommSemiring k] [Algebra k A] (p₁ : P₁ →ₗ[A] P₀) : Type (max (max w u) x)

The Auslander--Reiten translate τ = D Tr attached to a linear map p₁ : P₁ → P₀: the k-dual of its Auslander--Reiten transpose. The transpose is a right A-module, so TauCeti.dualRightAction makes the translate a left A-module.

When p₁ is the first map of a minimal projective presentation P₁ → P₀ → M → 0, this is the Auslander--Reiten translate of M: no exactness or projectivity is needed to form it, and minimality enters only through TauCeti.IsMinimalProjectivePresentation.nonempty_linearEquiv_auslanderReitenTranslate, which shows that the result is then independent, up to equivalence, of the chosen presentation.

Equations

• TauCeti.AuslanderReitenTranslate k p₁ = Module.Dual k (TauCeti.AuslanderReitenTranspose p₁)

@[instance_reducible]

instance TauCeti.AuslanderReitenTranslate.instModule {A : Type u} [Ring A] {k : Type x} [CommSemiring k] [Algebra k A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] {p₁ : P₁ →ₗ[A] P₀} : Module A (AuslanderReitenTranslate k p₁)

Equations

• TauCeti.AuslanderReitenTranslate.instModule = Module.compHom (Module.Dual k (TauCeti.AuslanderReitenTranspose p₁)) (TauCeti.dualRightAction k (TauCeti.AuslanderReitenTranspose p₁))

@[simp]

theorem TauCeti.AuslanderReitenTranslate.smul_apply {A : Type u} [Ring A] {k : Type x} [CommSemiring k] [Algebra k A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] {p₁ : P₁ →ₗ[A] P₀} (a : A) (φ : AuslanderReitenTranslate k p₁) (x : AuslanderReitenTranspose p₁) : (a • φ) x = φ (MulOpposite.op a • x)

The A-action on the translate is precomposition with the right action on the transpose.

instance TauCeti.AuslanderReitenTranslate.instIsScalarTower {A : Type u} [Ring A] {k : Type x} [CommSemiring k] [Algebra k A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] {p₁ : P₁ →ₗ[A] P₀} : IsScalarTower k A (AuslanderReitenTranslate k p₁)

Scalars from k act on the translate through A, so the two actions on it are the layered ones: the k-action is the restriction of the A-action along the algebra map.

def TauCeti.AuslanderReitenTranslate.linearEquiv {A : Type u} [Ring A] {k : Type x} [CommSemiring k] [Algebra k A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] {p₁ : P₁ →ₗ[A] P₀} {Q₀ : Type v'} {Q₁ : Type w'} [AddCommMonoid Q₀] [Module A Q₀] [AddCommMonoid Q₁] [Module A Q₁] {q₁ : Q₁ →ₗ[A] Q₀} (e : AuslanderReitenTranspose q₁ ≃ₗ[Aᵐᵒᵖ] AuslanderReitenTranspose p₁) : AuslanderReitenTranslate k p₁ ≃ₗ[A] AuslanderReitenTranslate k q₁

An equivalence of transposes dualizes to an equivalence of translates, contravariantly: an Aᵐᵒᵖ-linear equivalence Tr q₁ ≃ Tr p₁ sends a functional on Tr p₁ to its composite with that equivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.AuslanderReitenTranslate.linearEquiv_apply {A : Type u} [Ring A] {k : Type x} [CommSemiring k] [Algebra k A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] {p₁ : P₁ →ₗ[A] P₀} {Q₀ : Type v'} {Q₁ : Type w'} [AddCommMonoid Q₀] [Module A Q₀] [AddCommMonoid Q₁] [Module A Q₁] {q₁ : Q₁ →ₗ[A] Q₀} (e : AuslanderReitenTranspose q₁ ≃ₗ[Aᵐᵒᵖ] AuslanderReitenTranspose p₁) (φ : AuslanderReitenTranslate k p₁) (x : AuslanderReitenTranspose q₁) : ((linearEquiv e) φ) x = φ (e x)

@[simp]

theorem TauCeti.AuslanderReitenTranslate.linearEquiv_symm {A : Type u} [Ring A] {k : Type x} [CommSemiring k] [Algebra k A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] {p₁ : P₁ →ₗ[A] P₀} {Q₀ : Type v'} {Q₁ : Type w'} [AddCommMonoid Q₀] [Module A Q₀] [AddCommMonoid Q₁] [Module A Q₁] {q₁ : Q₁ →ₗ[A] Q₀} (e : AuslanderReitenTranspose q₁ ≃ₗ[Aᵐᵒᵖ] AuslanderReitenTranspose p₁) : (linearEquiv e).symm = linearEquiv e.symm

@[simp]

theorem TauCeti.AuslanderReitenTranslate.linearEquiv_refl {A : Type u} [Ring A] {k : Type x} [CommSemiring k] [Algebra k A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] {p₁ : P₁ →ₗ[A] P₀} : linearEquiv (LinearEquiv.refl Aᵐᵒᵖ (AuslanderReitenTranspose p₁)) = LinearEquiv.refl A (AuslanderReitenTranslate k p₁)

Transport along the identity equivalence of transposes is the identity.

@[simp]

theorem TauCeti.AuslanderReitenTranslate.linearEquiv_trans {A : Type u} [Ring A] {k : Type x} [CommSemiring k] [Algebra k A] {P₀ : Type v} {P₁ : Type w} [AddCommMonoid P₀] [Module A P₀] [AddCommMonoid P₁] [Module A P₁] {p₁ : P₁ →ₗ[A] P₀} {Q₀ : Type v'} {Q₁ : Type w'} [AddCommMonoid Q₀] [Module A Q₀] [AddCommMonoid Q₁] [Module A Q₁] {q₁ : Q₁ →ₗ[A] Q₀} {R₀ : Type u_1} {R₁ : Type u_2} [AddCommMonoid R₀] [Module A R₀] [AddCommMonoid R₁] [Module A R₁] {r₁ : R₁ →ₗ[A] R₀} (f : AuslanderReitenTranspose r₁ ≃ₗ[Aᵐᵒᵖ] AuslanderReitenTranspose q₁) (e : AuslanderReitenTranspose q₁ ≃ₗ[Aᵐᵒᵖ] AuslanderReitenTranspose p₁) : linearEquiv (f ≪≫ₗ e) = linearEquiv e ≪≫ₗ linearEquiv f

Dualizing is contravariant: transporting along a composite of equivalences of transposes is the composite of the transports in the reverse order.

theorem TauCeti.IsMinimalProjectivePresentation.subsingleton_auslanderReitenTranslate_of_projective {A : Type u} [Ring A] {k : Type x} [CommSemiring k] [Algebra k A] {M : Type u_1} [AddCommGroup M] [Module A M] {P₀ : Type v} [AddCommGroup P₀] [Module A P₀] {P₁ : Type w} [AddCommMonoid P₁] [Module A P₁] {p₁ : P₁ →ₗ[A] P₀} {p₀ : P₀ →ₗ[A] M} [Module.Projective A M] (h : IsMinimalProjectivePresentation p₁ p₀) : Subsingleton (AuslanderReitenTranslate k p₁)

The Auslander--Reiten translate of a projective module vanishes: its transpose already does, and the dual of a subsingleton is a subsingleton.

theorem TauCeti.IsMinimalProjectivePresentation.subsingleton_auslanderReitenTranslate_iff_projective {A : Type u} [Ring A] {M : Type u_1} [AddCommGroup M] [Module A M] {P₀ : Type v} [AddCommGroup P₀] [Module A P₀] {P₁ : Type w} [AddCommGroup P₁] [Module A P₁] {p₁ : P₁ →ₗ[A] P₀} {p₀ : P₀ →ₗ[A] M} (K : Type u_2) [CommSemiring K] [Algebra K A] [Module.Projective K (AuslanderReitenTranspose p₁)] [Module.Finite A P₁] (h : IsMinimalProjectivePresentation p₁ p₀) : Subsingleton (AuslanderReitenTranslate K p₁) ↔ Module.Projective A M

The Auslander--Reiten translate vanishes exactly on the projective modules, for a minimal projective presentation with finitely generated left-hand source and a transpose that is projective over the base. This is what makes τ a construction on the non-projective modules: it assigns a nonzero module to every module that is not projective.

The projectivity of the transpose over K is what lets a vanishing translate imply projectivity of M, through Module.subsingleton_dual_iff; it is automatic when K is a field. The implication the other way — a projective M has vanishing translate — is TauCeti.IsMinimalProjectivePresentation.subsingleton_auslanderReitenTranslate_of_projective, and needs neither hypothesis.

theorem TauCeti.IsMinimalProjectivePresentation.nonempty_linearEquiv_auslanderReitenTranslate {A : Type u} [Ring A] {k : Type x} [CommSemiring k] [Algebra k A] {M : Type u_1} [AddCommGroup M] [Module A M] {P₀ : Type v} [AddCommGroup P₀] [Module A P₀] {P₁ : Type w} [AddCommGroup P₁] [Module A P₁] {p₁ : P₁ →ₗ[A] P₀} {p₀ : P₀ →ₗ[A] M} {Q₀ : Type v'} {Q₁ : Type w'} [AddCommGroup Q₀] [Module A Q₀] [AddCommGroup Q₁] [Module A Q₁] {q₁ : Q₁ →ₗ[A] Q₀} {q₀ : Q₀ →ₗ[A] M} (h : IsMinimalProjectivePresentation p₁ p₀) (h' : IsMinimalProjectivePresentation q₁ q₀) : Nonempty (AuslanderReitenTranslate k p₁ ≃ₗ[A] AuslanderReitenTranslate k q₁)

The Auslander--Reiten translate is well defined: it is independent, up to A-linear equivalence, of the chosen minimal projective presentation of a module. This is the statement that licenses writing τ M for a module M.

@[simp]

theorem TauCeti.AuslanderReitenTranslate.isIndecomposableModule_iff {A : Type u} [Ring A] {P₀ : Type v} {P₁ : Type w} [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] (p₁ : P₁ →ₗ[A] P₀) (K : Type u_1) [CommRing K] [Algebra K A] [Module.IsReflexive K (AuslanderReitenTranspose p₁)] : IsIndecomposableModule A (AuslanderReitenTranslate K p₁) ↔ IsIndecomposableModule Aᵐᵒᵖ (AuslanderReitenTranspose p₁)

For a transpose reflexive over the base, the translate is indecomposable exactly when the transpose is. In particular this applies to finite-dimensional transposes over a field.