Nakayama modules

The Nakayama construction sends a left A-module P to ν(P) = Hom_k(Hom_A(P, A), k). Both dualizations reverse arrows, so ν is covariant. The left action is (a • φ)(ψ) = φ(ψ · a), where the inner dual is a right A-module. Finite projective modules go to injective modules when k is a field.

These modules are the injective terms obtained by dualizing a projective presentation when computing the Auslander–Reiten translate. The type synonym keeps the domain action separate from Mathlib's codomain action on linear maps. NakayamaModule.equivDual identifies the underlying scalar module with the double dual, and LinearMap.nakayamaMap computes its maps.

References

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

The action uses TauCeti.linearMapRightAction; injectivity uses the opposite dual of a finite projective module and LinearEquiv.moduleInjective_of_dual_projective.

def TauCeti.NakayamaModule (k : Type u) (A : Type v) (P : Type w) [CommSemiring k] [Semiring A] [Algebra k A] [AddCommMonoid P] [Module A P] : Type (max (max w v) u)

The Nakayama module ν(P) = D Hom_A(P, A), with the left action dual to the right action on Hom_A(P, A).

@[instance_reducible]

instance TauCeti.NakayamaModule.instAddCommMonoid (k : Type u) (A : Type v) (P : Type w) [CommSemiring k] [Semiring A] [Algebra k A] [AddCommMonoid P] [Module A P] : AddCommMonoid (NakayamaModule k A P)

@[instance_reducible]

instance TauCeti.NakayamaModule.instModule (k : Type u) (A : Type v) (P : Type w) [CommSemiring k] [Semiring A] [Algebra k A] [AddCommMonoid P] [Module A P] : Module k (NakayamaModule k A P)

@[instance_reducible]

instance TauCeti.NakayamaModule.instModule_1 (k : Type u) (A : Type v) (P : Type w) [CommSemiring k] [Semiring A] [Algebra k A] [AddCommMonoid P] [Module A P] : Module A (NakayamaModule k A P)

def TauCeti.NakayamaModule.equivDual (k : Type u) (A : Type v) (P : Type w) [CommSemiring k] [Semiring A] [Algebra k A] [AddCommMonoid P] [Module A P] : NakayamaModule k A P ≃ₗ[k] Module.Dual k (Module.Dual A P)

The underlying scalar module of ν(P) is the scalar dual of its algebra-valued dual.

theorem TauCeti.NakayamaModule.ext (k : Type u) (A : Type v) (P : Type w) [CommSemiring k] [Semiring A] [Algebra k A] [AddCommMonoid P] [Module A P] {φ χ : NakayamaModule k A P} (h : ∀ (ψ : Module.Dual A P), ((equivDual k A P) φ) ψ = ((equivDual k A P) χ) ψ) : φ = χ

Nakayama functionals are determined by evaluation on algebra-valued functionals.

theorem TauCeti.NakayamaModule.ext_iff {k : Type u} {A : Type v} {P : Type w} [CommSemiring k] [Semiring A] [Algebra k A] [AddCommMonoid P] [Module A P] {φ χ : NakayamaModule k A P} : φ = χ ↔ ∀ (ψ : Module.Dual A P), ((equivDual k A P) φ) ψ = ((equivDual k A P) χ) ψ

@[simp]

theorem TauCeti.NakayamaModule.smul_apply (k : Type u) (A : Type v) (P : Type w) [CommSemiring k] [Semiring A] [Algebra k A] [AddCommMonoid P] [Module A P] (a : A) (φ : NakayamaModule k A P) (ψ : Module.Dual A P) : ((equivDual k A P) (a • φ)) ψ = ((equivDual k A P) φ) (MulOpposite.op a • ψ)

The left action is dual to right multiplication on the values of an inner functional.

instance TauCeti.NakayamaModule.instIsScalarTower (k : Type u) (A : Type v) (P : Type w) [CommSemiring k] [Semiring A] [Algebra k A] [AddCommMonoid P] [Module A P] : IsScalarTower k A (NakayamaModule k A P)

@[instance_reducible]

instance TauCeti.NakayamaModule.instAddCommGroup (k : Type u) (A : Type v) (P : Type w) [CommRing k] [Semiring A] [Algebra k A] [AddCommMonoid P] [Module A P] : AddCommGroup (NakayamaModule k A P)

instance TauCeti.NakayamaModule.instInjectiveOfFiniteOfProjective (k : Type u) (A : Type v) (P : Type w) [Field k] [Ring A] [Algebra k A] [AddCommMonoid P] [Module A P] [Module.Finite A P] [Module.Projective A P] : Module.Injective A (NakayamaModule k A P)

The Nakayama module of a finite projective module is injective over an algebra over a field. The algebra need not be finite-dimensional.

def LinearMap.nakayamaMap {k : Type u} {A : Type v} [CommSemiring k] [Semiring A] [Algebra k A] {P : Type w} {Q : Type z} [AddCommMonoid P] [Module A P] [AddCommMonoid Q] [Module A Q] (f : P →ₗ[A] Q) : TauCeti.NakayamaModule k A P →ₗ[A] TauCeti.NakayamaModule k A Q

The covariant Nakayama map, obtained by applying the algebra dual and then the scalar dual.

@[simp]

theorem LinearMap.nakayamaMap_apply {k : Type u} {A : Type v} [CommSemiring k] [Semiring A] [Algebra k A] {P : Type w} {Q : Type z} [AddCommMonoid P] [Module A P] [AddCommMonoid Q] [Module A Q] (f : P →ₗ[A] Q) (φ : TauCeti.NakayamaModule k A P) (ψ : Module.Dual A Q) : ((TauCeti.NakayamaModule.equivDual k A Q) (f.nakayamaMap φ)) ψ = ((TauCeti.NakayamaModule.equivDual k A P) φ) (ψ ∘ₗ f)

A Nakayama map evaluates by precomposing the inner functional with the original map.

@[simp]

theorem LinearMap.nakayamaMap_id {k : Type u} {A : Type v} [CommSemiring k] [Semiring A] [Algebra k A] {P : Type w} [AddCommMonoid P] [Module A P] : id.nakayamaMap = id

The Nakayama construction preserves identity maps.

@[simp]

theorem LinearMap.nakayamaMap_comp {k : Type u} {A : Type v} [CommSemiring k] [Semiring A] [Algebra k A] {P : Type w} {Q : Type z} {N : Type t} [AddCommMonoid P] [Module A P] [AddCommMonoid Q] [Module A Q] [AddCommMonoid N] [Module A N] (g : Q →ₗ[A] N) (f : P →ₗ[A] Q) : (g ∘ₗ f).nakayamaMap = g.nakayamaMap ∘ₗ f.nakayamaMap

The Nakayama construction preserves composition in its original order.

@[simp]

theorem LinearMap.nakayamaMap_zero {k : Type u} {A : Type v} [CommSemiring k] [Semiring A] [Algebra k A] {P : Type w} {Q : Type z} [AddCommMonoid P] [Module A P] [AddCommMonoid Q] [Module A Q] : nakayamaMap 0 = 0

The Nakayama construction sends the zero map to zero.

@[simp]

theorem LinearMap.nakayamaMap_add {k : Type u} {A : Type v} [CommSemiring k] [Semiring A] [Algebra k A] {P : Type w} {Q : Type z} [AddCommMonoid P] [Module A P] [AddCommMonoid Q] [Module A Q] (f g : P →ₗ[A] Q) : (f + g).nakayamaMap = f.nakayamaMap + g.nakayamaMap

The Nakayama construction preserves addition of maps.