Documentation

TauCeti.Algebra.Module.Nakayama.Hom

Hom duality for the Nakayama construction #

For a finite projective left module P over a possibly noncommutative algebra A, the Nakayama module ν(P) = D Hom_A(P,A) represents the scalar dual of Hom_A(P,-):

D Hom_A(P,N) ≃ Hom_A(N,ν(P)).

The equivalence is linear over any commutative ground ring and natural in both modules. Neither the algebra nor the coefficient module needs to be finite-dimensional. Evaluation on the elementary map x ↦ ψ(x) • n characterizes both directions of the equivalence.

Applied to the terms of a projective presentation, naturality identifies the dual Hom complex with the Hom complex into the Nakayama terms. Together with the kernel description of D Tr, this is the termwise comparison used in Auslander–Reiten duality.

The construction uses balancedDualTensorHomEquiv for finite projective modules and the universal property of BalancedTensorProduct to curry its scalar dual. The Nakayama action is the domain action on functionals, rather than codomain scaling.

References #

source
noncomputable def TauCeti.nakayamaHomEquiv (k : Type u_1) (A : Type u_2) (P : Type u_3) (N : Type u_4) [CommRing k] [Ring A] [Algebra k A] [AddCommMonoid P] [Module A P] [AddCommGroup N] [Module A N] [Module k N] [IsScalarTower k A N] [Module.Finite A P] [Module.Projective A P] :
Module.Dual k (P →ₗ[A] N) ≃ₗ[k] N →ₗ[A] NakayamaModule k A P

Scalar duality of Hom from a finite projective module is represented by its Nakayama module: D Hom_A(P,N) ≃ Hom_A(N,ν(P)).

Instances For
    source
    @[simp]
    theorem TauCeti.nakayamaHomEquiv_apply (k : Type u_1) (A : Type u_2) (P : Type u_3) (N : Type u_4) [CommRing k] [Ring A] [Algebra k A] [AddCommMonoid P] [Module A P] [AddCommGroup N] [Module A N] [Module k N] [IsScalarTower k A N] [Module.Finite A P] [Module.Projective A P] (χ : Module.Dual k (P →ₗ[A] N)) (n : N) (ψ : Module.Dual A P) :
    ((NakayamaModule.equivDual k A P) (((nakayamaHomEquiv k A P N) χ) n)) ψ = χ ((balancedDualTensorHom k A P N) (BalancedTensorProduct.tmul k A ψ n))

    The functional corresponding to χ evaluates on ψ at n by applying χ to the elementary map x ↦ ψ(x) • n.

    source
    @[simp]
    theorem TauCeti.nakayamaHomEquiv_symm_apply (k : Type u_1) (A : Type u_2) (P : Type u_3) (N : Type u_4) [CommRing k] [Ring A] [Algebra k A] [AddCommMonoid P] [Module A P] [AddCommGroup N] [Module A N] [Module k N] [IsScalarTower k A N] [Module.Finite A P] [Module.Projective A P] (F : N →ₗ[A] NakayamaModule k A P) (ψ : Module.Dual A P) (n : N) :
    ((nakayamaHomEquiv k A P N).symm F) ((balancedDualTensorHom k A P N) (BalancedTensorProduct.tmul k A ψ n)) = ((NakayamaModule.equivDual k A P) (F n)) ψ

    Inverse Hom duality evaluates on a elementary map by the associated Nakayama functional.

    source
    @[simp]
    theorem TauCeti.nakayamaHomEquiv_dualMap_lcomp (k : Type u_1) (A : Type u_2) {P : Type u_3} {N : Type u_4} [CommRing k] [Ring A] [Algebra k A] [AddCommMonoid P] [Module A P] [AddCommGroup N] [Module A N] [Module k N] [IsScalarTower k A N] [Module.Finite A P] [Module.Projective A P] {Q : Type u_5} [AddCommMonoid Q] [Module A Q] [Module.Finite A Q] [Module.Projective A Q] (f : P →ₗ[A] Q) (χ : Module.Dual k (P →ₗ[A] N)) :
    (nakayamaHomEquiv k A Q N) ((LinearMap.lcomp k N f).dualMap χ) = f.nakayamaMap ∘ₗ (nakayamaHomEquiv k A P N) χ

    Nakayama Hom duality is covariantly natural in the projective module: dualizing precomposition by f corresponds to postcomposition by ν(f).

    source
    @[simp]
    theorem TauCeti.nakayamaHomEquiv_dualMap_compRight (k : Type u_1) (A : Type u_2) {P : Type u_3} {N : Type u_4} [CommRing k] [Ring A] [Algebra k A] [AddCommMonoid P] [Module A P] [AddCommGroup N] [Module A N] [Module k N] [IsScalarTower k A N] [Module.Finite A P] [Module.Projective A P] {N' : Type u_6} [AddCommGroup N'] [Module A N'] [Module k N'] [IsScalarTower k A N'] (g : N' →ₗ[A] N) (χ : Module.Dual k (P →ₗ[A] N)) :
    (nakayamaHomEquiv k A P N') ((LinearMap.compRight k g).dualMap χ) = (nakayamaHomEquiv k A P N) χ ∘ₗ g

    Nakayama Hom duality is contravariantly natural in the coefficient module: dualizing postcomposition by g corresponds to precomposition by g.