The Matlis dual of a module over an algebra

Let R be a commutative ring, E an R-module and A an R-algebra. The Matlis dual D_R N = Hom_R(N, E) exchanges left and right A-modules. This file defines it with its contravariant action on morphisms, shows that for injective E it sends projective modules to injective modules, and proves that evaluation N → D_R (D_R N) is an isomorphism of A-modules for N of finite length over R, when E is an injective hull of R ⧸ J(R) and R ⧸ J(R) is semisimple.

Right A-modules are modules over Aᵐᵒᵖ.

Main definitions

• TauCeti.MatlisDual R E N: the module Hom_R(N, E), a right module when N is a left A-module and a left module when N is a right A-module, in both cases by precomposition. It is a type synonym, since the module of linear maps already carries the action on the codomain.
• TauCeti.MatlisDual.map and TauCeti.MatlisDual.mapOp: the contravariant action on morphisms of left and of right modules, with the isomorphisms TauCeti.MatlisDual.congr and TauCeti.MatlisDual.congrOp.
• TauCeti.IsInjectiveEnvelope.matlisDualEvalEquiv and TauCeti.IsInjectiveEnvelope.matlisDualEvalEquivOp: biduality for modules of finite length, as an isomorphism of left and of right A-modules.

Implementation notes

The actions of A and Aᵐᵒᵖ on MatlisDual R E N are instances of low priority, so that instance search prefers the R-module structure on the values whenever A is R itself. The action of R through A is equal to it by the IsScalarTower instances, not definitionally.

The suffix Op on a construction marks a right-module source: MatlisDual.map dualizes morphisms of left modules, MatlisDual.mapOp those of right modules, and matlisDualEvalEquivOp is biduality for right modules.

References

• M. Auslander, I. Reiten, S. O. Smalø, Representation Theory of Artin Algebras, Section II.3.

def TauCeti.MatlisDual (R : Type u) [CommRing R] (E : Type v) [AddCommGroup E] [Module R E] (N : Type w) [AddCommGroup N] [Module R N] : Type (max v w)

The Matlis dual D_R N = Hom_R(N, E) of an R-module N, with values in E. A left A-module N has a right A-module as dual, and a right A-module has a left A-module as dual. The synonym keeps these actions apart from the action on the codomain of a linear map.

@[instance_reducible]

instance TauCeti.MatlisDual.instAddCommGroup (R : Type u) [CommRing R] (E : Type v) [AddCommGroup E] [Module R E] (N : Type w) [AddCommGroup N] [Module R N] : AddCommGroup (MatlisDual R E N)

@[instance_reducible]

instance TauCeti.MatlisDual.instModule (R : Type u) [CommRing R] (E : Type v) [AddCommGroup E] [Module R E] (N : Type w) [AddCommGroup N] [Module R N] : Module R (MatlisDual R E N)

def TauCeti.MatlisDual.equivLinearMap (R : Type u) [CommRing R] (E : Type v) [AddCommGroup E] [Module R E] (N : Type w) [AddCommGroup N] [Module R N] : MatlisDual R E N ≃ₗ[R] N →ₗ[R] E

The underlying R-module of D_R N is the module of linear maps N → E.

theorem TauCeti.MatlisDual.ext {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] {N : Type w} [AddCommGroup N] [Module R N] {φ ψ : MatlisDual R E N} (h : ∀ (x : N), ((equivLinearMap R E N) φ) x = ((equivLinearMap R E N) ψ) x) : φ = ψ

theorem TauCeti.MatlisDual.ext_iff {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] {N : Type w} [AddCommGroup N] [Module R N] {φ ψ : MatlisDual R E N} : φ = ψ ↔ ∀ (x : N), ((equivLinearMap R E N) φ) x = ((equivLinearMap R E N) ψ) x

@[instance_reducible, instance 100]

instance TauCeti.MatlisDual.instModuleMulOpposite {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] : Module Aᵐᵒᵖ (MatlisDual R E N)

The dual of a left A-module is a right A-module: (φ · a) x = φ (a • x).

@[simp]

theorem TauCeti.MatlisDual.smul_op_apply {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] (a : Aᵐᵒᵖ) (φ : MatlisDual R E N) (x : N) : ((equivLinearMap R E N) (a • φ)) x = ((equivLinearMap R E N) φ) (MulOpposite.unop a • x)

The right action on the dual of a left module is precomposition with the left action.

instance TauCeti.MatlisDual.instIsScalarTowerMulOpposite {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] : IsScalarTower R Aᵐᵒᵖ (MatlisDual R E N)

def TauCeti.MatlisDual.map {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] {N' : Type u_1} [AddCommGroup N'] [Module R N'] [Module A N'] [IsScalarTower R A N'] (g : N →ₗ[A] N') : MatlisDual R E N' →ₗ[Aᵐᵒᵖ] MatlisDual R E N

A morphism of left modules dualizes to a morphism of right modules, by precomposition.

@[simp]

theorem TauCeti.MatlisDual.map_apply {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] {N' : Type u_1} [AddCommGroup N'] [Module R N'] [Module A N'] [IsScalarTower R A N'] (g : N →ₗ[A] N') (φ : MatlisDual R E N') (x : N) : ((equivLinearMap R E N) ((map g) φ)) x = ((equivLinearMap R E N') φ) (g x)

@[simp]

theorem TauCeti.MatlisDual.map_id {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] : map LinearMap.id = LinearMap.id

@[simp]

theorem TauCeti.MatlisDual.map_comp {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] {N' : Type u_1} [AddCommGroup N'] [Module R N'] [Module A N'] [IsScalarTower R A N'] {N'' : Type u_2} [AddCommGroup N''] [Module R N''] [Module A N''] [IsScalarTower R A N''] (g : N' →ₗ[A] N'') (h : N →ₗ[A] N') : map (g ∘ₗ h) = map h ∘ₗ map g

def TauCeti.MatlisDual.congr {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] {N' : Type u_1} [AddCommGroup N'] [Module R N'] [Module A N'] [IsScalarTower R A N'] (e : N ≃ₗ[A] N') : MatlisDual R E N' ≃ₗ[Aᵐᵒᵖ] MatlisDual R E N

An isomorphism of left modules dualizes to an isomorphism of right modules. The two modules may carry any R-module structures compatible with the A-action.

@[simp]

theorem TauCeti.MatlisDual.congr_apply {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] {N' : Type u_1} [AddCommGroup N'] [Module R N'] [Module A N'] [IsScalarTower R A N'] (e : N ≃ₗ[A] N') (φ : MatlisDual R E N') (x : N) : ((equivLinearMap R E N) ((congr e) φ)) x = ((equivLinearMap R E N') φ) (e x)

@[simp]

theorem TauCeti.MatlisDual.congr_symm {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] {N' : Type u_1} [AddCommGroup N'] [Module R N'] [Module A N'] [IsScalarTower R A N'] (e : N ≃ₗ[A] N') : (congr e).symm = congr e.symm

@[simp]

theorem TauCeti.MatlisDual.congr_refl {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] : congr (LinearEquiv.refl A N) = LinearEquiv.refl Aᵐᵒᵖ (MatlisDual R E N)

@[simp]

theorem TauCeti.MatlisDual.congr_trans {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] {N' : Type u_1} [AddCommGroup N'] [Module R N'] [Module A N'] [IsScalarTower R A N'] {N'' : Type u_2} [AddCommGroup N''] [Module R N''] [Module A N''] [IsScalarTower R A N''] (e : N ≃ₗ[A] N') (e' : N' ≃ₗ[A] N'') : congr (e ≪≫ₗ e') = congr e' ≪≫ₗ congr e

@[instance_reducible, instance 100]

instance TauCeti.MatlisDual.instModule_1 {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module Aᵐᵒᵖ N] [IsScalarTower R Aᵐᵒᵖ N] : Module A (MatlisDual R E N)

The dual of a right A-module is a left A-module: (a • φ) x = φ (x · a).

@[simp]

theorem TauCeti.MatlisDual.smul_apply {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module Aᵐᵒᵖ N] [IsScalarTower R Aᵐᵒᵖ N] (a : A) (φ : MatlisDual R E N) (x : N) : ((equivLinearMap R E N) (a • φ)) x = ((equivLinearMap R E N) φ) (MulOpposite.op a • x)

The left action on the dual of a right module is precomposition with the right action.

instance TauCeti.MatlisDual.instIsScalarTower {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module Aᵐᵒᵖ N] [IsScalarTower R Aᵐᵒᵖ N] : IsScalarTower R A (MatlisDual R E N)

def TauCeti.MatlisDual.mapOp {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module Aᵐᵒᵖ N] [IsScalarTower R Aᵐᵒᵖ N] {N' : Type u_1} [AddCommGroup N'] [Module R N'] [Module Aᵐᵒᵖ N'] [IsScalarTower R Aᵐᵒᵖ N'] (g : N →ₗ[Aᵐᵒᵖ] N') : MatlisDual R E N' →ₗ[A] MatlisDual R E N

A morphism of right modules dualizes to a morphism of left modules, by precomposition.

@[simp]

theorem TauCeti.MatlisDual.mapOp_apply {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module Aᵐᵒᵖ N] [IsScalarTower R Aᵐᵒᵖ N] {N' : Type u_1} [AddCommGroup N'] [Module R N'] [Module Aᵐᵒᵖ N'] [IsScalarTower R Aᵐᵒᵖ N'] (g : N →ₗ[Aᵐᵒᵖ] N') (φ : MatlisDual R E N') (x : N) : ((equivLinearMap R E N) ((mapOp g) φ)) x = ((equivLinearMap R E N') φ) (g x)

@[simp]

theorem TauCeti.MatlisDual.mapOp_id {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module Aᵐᵒᵖ N] [IsScalarTower R Aᵐᵒᵖ N] : mapOp LinearMap.id = LinearMap.id

@[simp]

theorem TauCeti.MatlisDual.mapOp_comp {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module Aᵐᵒᵖ N] [IsScalarTower R Aᵐᵒᵖ N] {N' : Type u_1} [AddCommGroup N'] [Module R N'] [Module Aᵐᵒᵖ N'] [IsScalarTower R Aᵐᵒᵖ N'] {N'' : Type u_2} [AddCommGroup N''] [Module R N''] [Module Aᵐᵒᵖ N''] [IsScalarTower R Aᵐᵒᵖ N''] (g : N' →ₗ[Aᵐᵒᵖ] N'') (h : N →ₗ[Aᵐᵒᵖ] N') : mapOp (g ∘ₗ h) = mapOp h ∘ₗ mapOp g

def TauCeti.MatlisDual.congrOp {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module Aᵐᵒᵖ N] [IsScalarTower R Aᵐᵒᵖ N] {N' : Type u_1} [AddCommGroup N'] [Module R N'] [Module Aᵐᵒᵖ N'] [IsScalarTower R Aᵐᵒᵖ N'] (e : N ≃ₗ[Aᵐᵒᵖ] N') : MatlisDual R E N' ≃ₗ[A] MatlisDual R E N

An isomorphism of right modules dualizes to an isomorphism of left modules. The two modules may carry any R-module structures compatible with the A-action.

@[simp]

theorem TauCeti.MatlisDual.congrOp_apply {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module Aᵐᵒᵖ N] [IsScalarTower R Aᵐᵒᵖ N] {N' : Type u_1} [AddCommGroup N'] [Module R N'] [Module Aᵐᵒᵖ N'] [IsScalarTower R Aᵐᵒᵖ N'] (e : N ≃ₗ[Aᵐᵒᵖ] N') (φ : MatlisDual R E N') (x : N) : ((equivLinearMap R E N) ((congrOp e) φ)) x = ((equivLinearMap R E N') φ) (e x)

@[simp]

theorem TauCeti.MatlisDual.congrOp_symm {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module Aᵐᵒᵖ N] [IsScalarTower R Aᵐᵒᵖ N] {N' : Type u_1} [AddCommGroup N'] [Module R N'] [Module Aᵐᵒᵖ N'] [IsScalarTower R Aᵐᵒᵖ N'] (e : N ≃ₗ[Aᵐᵒᵖ] N') : (congrOp e).symm = congrOp e.symm

@[simp]

theorem TauCeti.MatlisDual.congrOp_refl {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module Aᵐᵒᵖ N] [IsScalarTower R Aᵐᵒᵖ N] : congrOp (LinearEquiv.refl Aᵐᵒᵖ N) = LinearEquiv.refl A (MatlisDual R E N)

@[simp]

theorem TauCeti.MatlisDual.congrOp_trans {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module Aᵐᵒᵖ N] [IsScalarTower R Aᵐᵒᵖ N] {N' : Type u_1} [AddCommGroup N'] [Module R N'] [Module Aᵐᵒᵖ N'] [IsScalarTower R Aᵐᵒᵖ N'] {N'' : Type u_2} [AddCommGroup N''] [Module R N''] [Module Aᵐᵒᵖ N''] [IsScalarTower R Aᵐᵒᵖ N''] (e : N ≃ₗ[Aᵐᵒᵖ] N') (e' : N' ≃ₗ[Aᵐᵒᵖ] N'') : congrOp (e ≪≫ₗ e') = congrOp e' ≪≫ₗ congrOp e

instance TauCeti.instInjectiveMatlisDualOfProjectiveMulOpposite {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] [Small.{v, u} R] [Module.Injective R E] {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module Aᵐᵒᵖ N] [IsScalarTower R Aᵐᵒᵖ N] [Module.Projective Aᵐᵒᵖ N] : Module.Injective A (MatlisDual R E N)

The dual of a projective right module is an injective left module.

instance TauCeti.instInjectiveMulOppositeMatlisDualOfProjective {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] [Small.{v, u} R] [Module.Injective R E] {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] [Module.Projective A N] : Module.Injective Aᵐᵒᵖ (MatlisDual R E N)

The dual of a projective left module is an injective right module.

instance TauCeti.instInjectiveMatlisDual {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] [Small.{v, u} R] [Module.Injective R E] {A : Type t} [Ring A] [Algebra R A] : Module.Injective A (MatlisDual R E A)

D_R A, the dual of the right regular module with action (a • φ) x = φ (x * a), is an injective left A-module.

def TauCeti.MatlisDual.evalₗ (R : Type u) [CommRing R] (E : Type v) [AddCommGroup E] [Module R E] (N : Type w) [AddCommGroup N] [Module R N] : N →ₗ[R] MatlisDual R E (MatlisDual R E N)

Evaluation N → D_R (D_R N), as a map of R-modules.

@[simp]

theorem TauCeti.MatlisDual.evalₗ_apply {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] (N : Type w) [AddCommGroup N] [Module R N] (x : N) (φ : MatlisDual R E N) : ((equivLinearMap R E (MatlisDual R E N)) ((evalₗ R E N) x)) φ = ((equivLinearMap R E N) φ) x

theorem TauCeti.IsInjectiveEnvelope.bijective_evalₗ {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] [IsSemisimpleRing (R ⧸ Ring.jacobson R)] [Small.{v, u} R] {f : R ⧸ Ring.jacobson R →ₗ[R] E} {N : Type w} [AddCommGroup N] [Module R N] (hf : IsInjectiveEnvelope f) (hN : IsFiniteLength R N) : Function.Bijective ⇑(MatlisDual.evalₗ R E N)

Matlis biduality. Evaluation N → D_R (D_R N) is bijective for every R-module N of finite length.

noncomputable def TauCeti.IsInjectiveEnvelope.matlisDualEvalEquiv {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] [IsSemisimpleRing (R ⧸ Ring.jacobson R)] [Small.{v, u} R] {f : R ⧸ Ring.jacobson R →ₗ[R] E} {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] (hf : IsInjectiveEnvelope f) (hN : IsFiniteLength R N) : N ≃ₗ[A] MatlisDual R E (MatlisDual R E N)

Matlis biduality for left modules. Evaluation N → D_R (D_R N) is an isomorphism of left A-modules for every left A-module N of finite length over R.

@[simp]

theorem TauCeti.IsInjectiveEnvelope.matlisDualEvalEquiv_apply {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] [IsSemisimpleRing (R ⧸ Ring.jacobson R)] [Small.{v, u} R] {f : R ⧸ Ring.jacobson R →ₗ[R] E} {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module A N] [IsScalarTower R A N] (hf : IsInjectiveEnvelope f) (hN : IsFiniteLength R N) (x : N) (φ : MatlisDual R E N) : ((MatlisDual.equivLinearMap R E (MatlisDual R E N)) ((hf.matlisDualEvalEquiv hN) x)) φ = ((MatlisDual.equivLinearMap R E N) φ) x

noncomputable def TauCeti.IsInjectiveEnvelope.matlisDualEvalEquivOp {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] [IsSemisimpleRing (R ⧸ Ring.jacobson R)] [Small.{v, u} R] {f : R ⧸ Ring.jacobson R →ₗ[R] E} {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module Aᵐᵒᵖ N] [IsScalarTower R Aᵐᵒᵖ N] (hf : IsInjectiveEnvelope f) (hN : IsFiniteLength R N) : N ≃ₗ[Aᵐᵒᵖ] MatlisDual R E (MatlisDual R E N)

Matlis biduality for right modules. Evaluation N → D_R (D_R N) is an isomorphism of right A-modules for every right A-module N of finite length over R.

@[simp]

theorem TauCeti.IsInjectiveEnvelope.matlisDualEvalEquivOp_apply {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] [IsSemisimpleRing (R ⧸ Ring.jacobson R)] [Small.{v, u} R] {f : R ⧸ Ring.jacobson R →ₗ[R] E} {A : Type t} [Ring A] [Algebra R A] {N : Type w} [AddCommGroup N] [Module R N] [Module Aᵐᵒᵖ N] [IsScalarTower R Aᵐᵒᵖ N] (hf : IsInjectiveEnvelope f) (hN : IsFiniteLength R N) (x : N) (φ : MatlisDual R E N) : ((MatlisDual.equivLinearMap R E (MatlisDual R E N)) ((hf.matlisDualEvalEquivOp hN) x)) φ = ((MatlisDual.equivLinearMap R E N) φ) x