The Matlis dual on bundled modules over an algebra

Let R be a commutative ring and A an R-algebra. This file packages the Matlis dual D_R = Hom_R(-, E) of TauCeti/RingTheory/MatlisDuality/Basic.lean as contravariant additive functors between ModuleCat A and ModuleCat Aᵐᵒᵖ, and evaluation as a natural isomorphism on modules of finite length over R, when E is an injective hull of R ⧸ J(R) and R ⧸ J(R) is semisimple.

Main definitions

• ModuleCat.matlisDual and ModuleCat.matlisDualOp: D_R as a contravariant additive functor from left to right modules and from right to left modules.
• TauCeti.IsInjectiveEnvelope.moduleCatEvalIso and TauCeti.IsInjectiveEnvelope.moduleCatEvalIsoOp: biduality for bundled modules of finite length.

Implementation notes

A module over an R-algebra A is bundled in ModuleCat A, which remembers only the action of A, so its R-action is recovered through the algebra map, by ModuleCat.moduleOfAlgebra. On the dual of a module this equals the R-action on the values only propositionally, not definitionally. The bundled duals ModuleCat.matlisDualObj and ModuleCat.matlisDualOpObj are therefore not reducible to MatlisDual, and are compared with it by ModuleCat.matlisDualObjEquiv and ModuleCat.matlisDualOpObjEquiv.

References

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

def ModuleCat.matlisDualObj (R : Type u) [CommRing R] {A : Type t} [Ring A] [Algebra R A] (E : Type v) [AddCommGroup E] [Module R E] (M : ModuleCat A) : ModuleCat Aᵐᵒᵖ

The Matlis dual of a left A-module, as a bundled right A-module.

noncomputable def ModuleCat.matlisDualObjEquiv (R : Type u) [CommRing R] {A : Type t} [Ring A] [Algebra R A] (E : Type v) [AddCommGroup E] [Module R E] (M : ModuleCat A) : ↑(matlisDualObj R E M) ≃ₗ[Aᵐᵒᵖ] TauCeti.MatlisDual R E ↑M

The underlying module of the bundled dual of a left module is its Matlis dual.

noncomputable def ModuleCat.matlisDualObjLinearEquiv (R : Type u) [CommRing R] {A : Type t} [Ring A] [Algebra R A] (E : Type v) [AddCommGroup E] [Module R E] (M : ModuleCat A) : ↑(matlisDualObj R E M) ≃ₗ[R] ↑M →ₗ[R] E

The underlying R-module of the bundled dual of a left module is the module of linear maps.

theorem ModuleCat.matlisDualObjLinearEquiv_apply (R : Type u) [CommRing R] {A : Type t} [Ring A] [Algebra R A] (E : Type v) [AddCommGroup E] [Module R E] (M : ModuleCat A) (φ : ↑(matlisDualObj R E M)) : (matlisDualObjLinearEquiv R E M) φ = (TauCeti.MatlisDual.equivLinearMap R E ↑M) ((matlisDualObjEquiv R E M) φ)

@[simp]

theorem ModuleCat.matlisDualObjLinearEquiv_smul (R : Type u) [CommRing R] {A : Type t} [Ring A] [Algebra R A] (E : Type v) [AddCommGroup E] [Module R E] (M : ModuleCat A) (a : Aᵐᵒᵖ) (φ : ↑(matlisDualObj R E M)) (x : ↑M) : ((matlisDualObjLinearEquiv R E M) (a • φ)) x = ((matlisDualObjLinearEquiv R E M) φ) (MulOpposite.unop a • x)

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

noncomputable def ModuleCat.matlisDualMap (R : Type u) [CommRing R] {A : Type t} [Ring A] [Algebra R A] (E : Type v) [AddCommGroup E] [Module R E] {M M' : ModuleCat A} (g : M ⟶ M') : matlisDualObj R E M' ⟶ matlisDualObj R E M

The dual of a morphism of left modules.

@[simp]

theorem ModuleCat.matlisDualObjEquiv_map_apply (R : Type u) [CommRing R] {A : Type t} [Ring A] [Algebra R A] (E : Type v) [AddCommGroup E] [Module R E] {M M' : ModuleCat A} (g : M ⟶ M') (φ : ↑(matlisDualObj R E M')) (x : ↑M) : ((TauCeti.MatlisDual.equivLinearMap R E ↑M) ((matlisDualObjEquiv R E M) ((CategoryTheory.ConcreteCategory.hom (matlisDualMap R E g)) φ))) x = ((TauCeti.MatlisDual.equivLinearMap R E ↑M') ((matlisDualObjEquiv R E M') φ)) ((CategoryTheory.ConcreteCategory.hom g) x)

noncomputable def ModuleCat.matlisDual (R : Type u) [CommRing R] {A : Type t} [Ring A] [Algebra R A] (E : Type v) [AddCommGroup E] [Module R E] : CategoryTheory.Functor (ModuleCat A)ᵒᵖ (ModuleCat Aᵐᵒᵖ)

The Matlis dual D_R = Hom_R(-, E), from left to right A-modules.

@[simp]

theorem ModuleCat.matlisDual_obj (R : Type u) [CommRing R] {A : Type t} [Ring A] [Algebra R A] (E : Type v) [AddCommGroup E] [Module R E] (M : (ModuleCat A)ᵒᵖ) : (matlisDual R E).obj M = matlisDualObj R E (Opposite.unop M)

@[simp]

theorem ModuleCat.matlisDual_map (R : Type u) [CommRing R] {A : Type t} [Ring A] [Algebra R A] (E : Type v) [AddCommGroup E] [Module R E] {X✝ Y✝ : (ModuleCat A)ᵒᵖ} (g : X✝ ⟶ Y✝) : (matlisDual R E).map g = matlisDualMap R E g.unop

theorem ModuleCat.matlisDualMap_add (R : Type u) [CommRing R] {A : Type t} [Ring A] [Algebra R A] (E : Type v) [AddCommGroup E] [Module R E] {M M' : ModuleCat A} (g h : M ⟶ M') : matlisDualMap R E (g + h) = matlisDualMap R E g + matlisDualMap R E h

instance ModuleCat.instAdditiveOppositeMulOppositeMatlisDual (R : Type u) [CommRing R] {A : Type t} [Ring A] [Algebra R A] (E : Type v) [AddCommGroup E] [Module R E] : (matlisDual R E).Additive

def ModuleCat.matlisDualOpObj (R : Type u) [CommRing R] {A : Type t} [Ring A] [Algebra R A] (E : Type v) [AddCommGroup E] [Module R E] (N : ModuleCat Aᵐᵒᵖ) : ModuleCat A

The Matlis dual of a right A-module, as a bundled left A-module.

noncomputable def ModuleCat.matlisDualOpObjEquiv (R : Type u) [CommRing R] {A : Type t} [Ring A] [Algebra R A] (E : Type v) [AddCommGroup E] [Module R E] (N : ModuleCat Aᵐᵒᵖ) : ↑(matlisDualOpObj R E N) ≃ₗ[A] TauCeti.MatlisDual R E ↑N

The underlying module of the bundled dual of a right module is its Matlis dual.

noncomputable def ModuleCat.matlisDualOpMap (R : Type u) [CommRing R] {A : Type t} [Ring A] [Algebra R A] (E : Type v) [AddCommGroup E] [Module R E] {N N' : ModuleCat Aᵐᵒᵖ} (g : N ⟶ N') : matlisDualOpObj R E N' ⟶ matlisDualOpObj R E N

The dual of a morphism of right modules.

@[simp]

theorem ModuleCat.matlisDualOpObjEquiv_map_apply (R : Type u) [CommRing R] {A : Type t} [Ring A] [Algebra R A] (E : Type v) [AddCommGroup E] [Module R E] {N N' : ModuleCat Aᵐᵒᵖ} (g : N ⟶ N') (φ : ↑(matlisDualOpObj R E N')) (x : ↑N) : ((TauCeti.MatlisDual.equivLinearMap R E ↑N) ((matlisDualOpObjEquiv R E N) ((CategoryTheory.ConcreteCategory.hom (matlisDualOpMap R E g)) φ))) x = ((TauCeti.MatlisDual.equivLinearMap R E ↑N') ((matlisDualOpObjEquiv R E N') φ)) ((CategoryTheory.ConcreteCategory.hom g) x)

noncomputable def ModuleCat.matlisDualOp (R : Type u) [CommRing R] {A : Type t} [Ring A] [Algebra R A] (E : Type v) [AddCommGroup E] [Module R E] : CategoryTheory.Functor (ModuleCat Aᵐᵒᵖ)ᵒᵖ (ModuleCat A)

The Matlis dual D_R = Hom_R(-, E), from right to left A-modules.

@[simp]

theorem ModuleCat.matlisDualOp_map (R : Type u) [CommRing R] {A : Type t} [Ring A] [Algebra R A] (E : Type v) [AddCommGroup E] [Module R E] {X✝ Y✝ : (ModuleCat Aᵐᵒᵖ)ᵒᵖ} (g : X✝ ⟶ Y✝) : (matlisDualOp R E).map g = matlisDualOpMap R E g.unop

@[simp]

theorem ModuleCat.matlisDualOp_obj (R : Type u) [CommRing R] {A : Type t} [Ring A] [Algebra R A] (E : Type v) [AddCommGroup E] [Module R E] (N : (ModuleCat Aᵐᵒᵖ)ᵒᵖ) : (matlisDualOp R E).obj N = matlisDualOpObj R E (Opposite.unop N)

theorem ModuleCat.matlisDualOpMap_add (R : Type u) [CommRing R] {A : Type t} [Ring A] [Algebra R A] (E : Type v) [AddCommGroup E] [Module R E] {N N' : ModuleCat Aᵐᵒᵖ} (g h : N ⟶ N') : matlisDualOpMap R E (g + h) = matlisDualOpMap R E g + matlisDualOpMap R E h

instance ModuleCat.instAdditiveOppositeMulOppositeMatlisDualOp (R : Type u) [CommRing R] {A : Type t} [Ring A] [Algebra R A] (E : Type v) [AddCommGroup E] [Module R E] : (matlisDualOp R E).Additive

noncomputable def TauCeti.IsInjectiveEnvelope.moduleCatEvalIso {R : Type u} [CommRing R] [IsSemisimpleRing (R ⧸ Ring.jacobson R)] {E : Type v} [AddCommGroup E] [Module R E] [Small.{v, u} R] {f : R ⧸ Ring.jacobson R →ₗ[R] E} {A : Type t} [Ring A] [Algebra R A] (hf : IsInjectiveEnvelope f) (M : ModuleCat A) (hM : IsFiniteLength R ↑M) : M ≅ ModuleCat.matlisDualOpObj R E (ModuleCat.matlisDualObj R E M)

Matlis biduality for a left A-module M of finite length over R, as an isomorphism M ≅ D_R (D_R M) of bundled modules.

@[simp]

theorem TauCeti.IsInjectiveEnvelope.moduleCatEvalIso_hom_apply {R : Type u} [CommRing R] [IsSemisimpleRing (R ⧸ Ring.jacobson R)] {E : Type v} [AddCommGroup E] [Module R E] [Small.{v, u} R] {f : R ⧸ Ring.jacobson R →ₗ[R] E} {A : Type t} [Ring A] [Algebra R A] (hf : IsInjectiveEnvelope f) (M : ModuleCat A) (hM : IsFiniteLength R ↑M) (x : ↑M) (φ : ↑(ModuleCat.matlisDualObj R E M)) : ((MatlisDual.equivLinearMap R E ↑(ModuleCat.matlisDualObj R E M)) ((ModuleCat.matlisDualOpObjEquiv R E (ModuleCat.matlisDualObj R E M)) ((CategoryTheory.ConcreteCategory.hom (hf.moduleCatEvalIso M hM).hom) x))) φ = ((MatlisDual.equivLinearMap R E ↑M) ((ModuleCat.matlisDualObjEquiv R E M) φ)) x

The isomorphism M ≅ D_R (D_R M) is evaluation.

noncomputable def TauCeti.IsInjectiveEnvelope.moduleCatEvalIsoOp {R : Type u} [CommRing R] [IsSemisimpleRing (R ⧸ Ring.jacobson R)] {E : Type v} [AddCommGroup E] [Module R E] [Small.{v, u} R] {f : R ⧸ Ring.jacobson R →ₗ[R] E} {A : Type t} [Ring A] [Algebra R A] (hf : IsInjectiveEnvelope f) (N : ModuleCat Aᵐᵒᵖ) (hN : IsFiniteLength R ↑N) : N ≅ ModuleCat.matlisDualObj R E (ModuleCat.matlisDualOpObj R E N)

Matlis biduality for a right A-module N of finite length over R, as an isomorphism N ≅ D_R (D_R N) of bundled modules.

@[simp]

theorem TauCeti.IsInjectiveEnvelope.moduleCatEvalIsoOp_hom_apply {R : Type u} [CommRing R] [IsSemisimpleRing (R ⧸ Ring.jacobson R)] {E : Type v} [AddCommGroup E] [Module R E] [Small.{v, u} R] {f : R ⧸ Ring.jacobson R →ₗ[R] E} {A : Type t} [Ring A] [Algebra R A] (hf : IsInjectiveEnvelope f) (N : ModuleCat Aᵐᵒᵖ) (hN : IsFiniteLength R ↑N) (x : ↑N) (φ : ↑(ModuleCat.matlisDualOpObj R E N)) : ((MatlisDual.equivLinearMap R E ↑(ModuleCat.matlisDualOpObj R E N)) ((ModuleCat.matlisDualObjEquiv R E (ModuleCat.matlisDualOpObj R E N)) ((CategoryTheory.ConcreteCategory.hom (hf.moduleCatEvalIsoOp N hN).hom) x))) φ = ((MatlisDual.equivLinearMap R E ↑N) ((ModuleCat.matlisDualOpObjEquiv R E N) φ)) x

The isomorphism N ≅ D_R (D_R N) is evaluation.

theorem TauCeti.IsInjectiveEnvelope.moduleCatEvalIso_hom_naturality {R : Type u} [CommRing R] [IsSemisimpleRing (R ⧸ Ring.jacobson R)] {E : Type v} [AddCommGroup E] [Module R E] [Small.{v, u} R] {f : R ⧸ Ring.jacobson R →ₗ[R] E} {A : Type t} [Ring A] [Algebra R A] (hf : IsInjectiveEnvelope f) {M M' : ModuleCat A} (g : M ⟶ M') (hM : IsFiniteLength R ↑M) (hM' : IsFiniteLength R ↑M') : CategoryTheory.CategoryStruct.comp g (hf.moduleCatEvalIso M' hM').hom = CategoryTheory.CategoryStruct.comp (hf.moduleCatEvalIso M hM).hom (ModuleCat.matlisDualOpMap R E (ModuleCat.matlisDualMap R E g))

The isomorphism M ≅ D_R (D_R M) is natural in M.

theorem TauCeti.IsInjectiveEnvelope.moduleCatEvalIsoOp_hom_naturality {R : Type u} [CommRing R] [IsSemisimpleRing (R ⧸ Ring.jacobson R)] {E : Type v} [AddCommGroup E] [Module R E] [Small.{v, u} R] {f : R ⧸ Ring.jacobson R →ₗ[R] E} {A : Type t} [Ring A] [Algebra R A] (hf : IsInjectiveEnvelope f) {N N' : ModuleCat Aᵐᵒᵖ} (g : N ⟶ N') (hN : IsFiniteLength R ↑N) (hN' : IsFiniteLength R ↑N') : CategoryTheory.CategoryStruct.comp g (hf.moduleCatEvalIsoOp N' hN').hom = CategoryTheory.CategoryStruct.comp (hf.moduleCatEvalIsoOp N hN).hom (ModuleCat.matlisDualMap R E (ModuleCat.matlisDualOpMap R E g))

The isomorphism N ≅ D_R (D_R N) is natural in N.

theorem TauCeti.IsInjectiveEnvelope.moduleCatEvalIsoOp_matlisDualObj_hom {R : Type u} [CommRing R] [IsSemisimpleRing (R ⧸ Ring.jacobson R)] {E : Type v} [AddCommGroup E] [Module R E] [Small.{v, u} R] {f : R ⧸ Ring.jacobson R →ₗ[R] E} {A : Type t} [Ring A] [Algebra R A] (hf : IsInjectiveEnvelope f) (M : ModuleCat A) (hM : IsFiniteLength R ↑M) (hM' : IsFiniteLength R ↑(ModuleCat.matlisDualObj R E M)) : (hf.moduleCatEvalIsoOp (ModuleCat.matlisDualObj R E M) hM').hom = ModuleCat.matlisDualMap R E (hf.moduleCatEvalIso M hM).inv

Evaluation on the dual D_R M of M is precomposition with the inverse of evaluation on M. This is the triangle identity of the Matlis duality.