The Auslander–Reiten translate as a kernel

For an arrow f : P₁ → P₀, dualizing the quotient defining its transpose gives the exact sequence 0 → D Tr(f) → ν(P₁) → ν(P₀), where ν(P) = D Hom_A(P, A) is the Nakayama module. LinearMap.auslanderReitenTranslateEquivKerNakayama identifies the translate with this kernel, with forward and inverse evaluation formulas.

When the arrow belongs to a finite projective presentation over an algebra over a field, both Nakayama modules are injective. Thus this sequence gives an injective copresentation of the translate, used to compute morphisms into it and to establish Auslander–Reiten duality. No minimality, exactness, or projectivity is needed for the kernel identification itself.

References

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

The exactness proof uses Mathlib's LinearMap.range_dualMap_eq_dualAnnihilator_ker_of_surjective and LinearMap.ker_dualMap_eq_dualAnnihilator_range, applied to the transpose quotient.

def LinearMap.auslanderReitenTranslateToNakayama {k : Type u} {A : Type v} [CommRing k] [Ring A] [Algebra k A] {P₀ : Type w} {P₁ : Type z} [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] (f : P₁ →ₗ[A] P₀) : TauCeti.AuslanderReitenTranslate k f →ₗ[A] TauCeti.NakayamaModule k A P₁

The canonical embedding of D Tr(f) into ν(P₁), obtained by dualizing the quotient onto the transpose.

@[simp]

theorem LinearMap.auslanderReitenTranslateToNakayama_apply {k : Type u} {A : Type v} [CommRing k] [Ring A] [Algebra k A] {P₀ : Type w} {P₁ : Type z} [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] (f : P₁ →ₗ[A] P₀) (φ : TauCeti.AuslanderReitenTranslate k f) (ψ : Module.Dual A P₁) : ((TauCeti.NakayamaModule.equivDual k A P₁) (f.auslanderReitenTranslateToNakayama φ)) ψ = φ ((TauCeti.AuslanderReitenTranspose.mk f) ψ)

The embedding evaluates a translate functional on the class of the inner functional.

theorem LinearMap.auslanderReitenTranslateToNakayama_injective {k : Type u} {A : Type v} [CommRing k] [Ring A] [Algebra k A] {P₀ : Type w} {P₁ : Type z} [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] (f : P₁ →ₗ[A] P₀) : Function.Injective ⇑f.auslanderReitenTranslateToNakayama

Dualizing the transpose quotient is injective.

theorem LinearMap.exact_auslanderReitenTranslateToNakayama_nakayamaMap {k : Type u} {A : Type v} [CommRing k] [Ring A] [Algebra k A] {P₀ : Type w} {P₁ : Type z} [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] (f : P₁ →ₗ[A] P₀) : Function.Exact ⇑f.auslanderReitenTranslateToNakayama ⇑f.nakayamaMap

The image of the translate in ν(P₁) is exactly the kernel of ν(f).

noncomputable def LinearMap.auslanderReitenTranslateEquivKerNakayama {k : Type u} {A : Type v} [CommRing k] [Ring A] [Algebra k A] {P₀ : Type w} {P₁ : Type z} [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] (f : P₁ →ₗ[A] P₀) : TauCeti.AuslanderReitenTranslate k f ≃ₗ[A] ↥f.nakayamaMap.ker

The canonical algebra-linear identification of D Tr(f) with the kernel of ν(f).

@[simp]

theorem LinearMap.auslanderReitenTranslateEquivKerNakayama_apply {k : Type u} {A : Type v} [CommRing k] [Ring A] [Algebra k A] {P₀ : Type w} {P₁ : Type z} [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] (f : P₁ →ₗ[A] P₀) (φ : TauCeti.AuslanderReitenTranslate k f) (ψ : Module.Dual A P₁) : ((TauCeti.NakayamaModule.equivDual k A P₁) ↑(f.auslanderReitenTranslateEquivKerNakayama φ)) ψ = φ ((TauCeti.AuslanderReitenTranspose.mk f) ψ)

Forward kernel transport evaluates on transpose classes.

@[simp]

theorem LinearMap.auslanderReitenTranslateEquivKerNakayama_symm_apply_mk {k : Type u} {A : Type v} [CommRing k] [Ring A] [Algebra k A] {P₀ : Type w} {P₁ : Type z} [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] (f : P₁ →ₗ[A] P₀) (φ : ↥f.nakayamaMap.ker) (ψ : Module.Dual A P₁) : (f.auslanderReitenTranslateEquivKerNakayama.symm φ) ((TauCeti.AuslanderReitenTranspose.mk f) ψ) = ((TauCeti.NakayamaModule.equivDual k A P₁) ↑φ) ψ

Inverse kernel transport descends a Nakayama functional to the transpose quotient.