Matlis duality for modules of finite length

Let R be a commutative local ring with residue field κ, and let ι : κ → E be an injective envelope of κ. The Matlis dual of an R-module M is D(M) = Hom_R(M, E). This file proves the finite-length case of Matlis duality: D preserves length, and the evaluation map M → D(D(M)) is an isomorphism for every module of finite length. No Noetherian hypothesis is needed. These are the base cases from which the duality between Artinian modules and finite modules over the completion is built, by passing to the submodules killed by powers of the maximal ideal. Length preservation and biduality are the cogenerator criteria of TauCeti/Algebra/Module/Injective/Cogenerator.lean, applied to the computation of D(κ).

Main declarations

• TauCeti.residueFieldLinearMapEquiv: D(κ) ≅ κ. Every linear map κ → E is ι composed with multiplication by a residue, because the image of ι is the only simple submodule of an essential extension of κ. Injectivity of E is not used.
• TauCeti.injective_applyₗ_of_injective: as soon as E is injective and contains a copy of κ, the evaluation map M → D(D(M)) is injective for every M, so E is a cogenerator.
• TauCeti.IsInjectiveEnvelope.length_linearMap: length D(M) = length M for every module M, of finite length or not.
• TauCeti.IsInjectiveEnvelope.bijective_applyₗ and TauCeti.IsInjectiveEnvelope.evalEquiv: biduality for modules of finite length.
• TauCeti.annihilator_torsionBySet_of_injective: if E is injective and contains a copy of κ, then the annihilator of E[J] is J, for every ideal J.
• TauCeti.IsInjectiveEnvelope.exists_eq_smul_subtype: for an ideal J with R ⧸ J of finite length, every linear map E[J] → E is the inclusion multiplied by a scalar.

References

• The Stacks Project, Section 47.7, Matlis duality, Tag 08Z1.
• W. Bruns, J. Herzog, Cohen–Macaulay rings, Section 3.2.

noncomputable def TauCeti.residueFieldLinearMapEquiv {R : Type u} [CommRing R] [IsLocalRing R] {E : Type v} [AddCommGroup E] [Module R E] {ι : IsLocalRing.ResidueField R →ₗ[R] E} (hι : Function.Injective ⇑ι) (hess : IsEssential ι.range) : IsLocalRing.ResidueField R ≃ₗ[R] IsLocalRing.ResidueField R →ₗ[R] E

The Matlis dual of the residue field is the residue field: for an embedding ι of κ with essential range, a ↦ (b ↦ ι (a * b)) is an isomorphism κ ≅ Hom_R(κ, E).

@[simp]

theorem TauCeti.residueFieldLinearMapEquiv_apply_apply {R : Type u} [CommRing R] [IsLocalRing R] {E : Type v} [AddCommGroup E] [Module R E] {ι : IsLocalRing.ResidueField R →ₗ[R] E} (hι : Function.Injective ⇑ι) (hess : IsEssential ι.range) (a b : IsLocalRing.ResidueField R) : ((residueFieldLinearMapEquiv hι hess) a) b = ι (a * b)

theorem TauCeti.injective_applyₗ_of_injective {R : Type u} [CommRing R] [IsLocalRing R] {E : Type v} [AddCommGroup E] [Module R E] {ι : IsLocalRing.ResidueField R →ₗ[R] E} [Small.{v, u} R] [Module.Injective R E] (hι : Function.Injective ⇑ι) {M : Type w} [AddCommGroup M] [Module R M] : Function.Injective ⇑LinearMap.applyₗ

If E is injective and contains a copy of the residue field, then E is a cogenerator: the evaluation map M → Hom_R(Hom_R(M, E), E) is injective for every module M.

theorem TauCeti.annihilator_torsionBySet_of_injective {R : Type u} [CommRing R] [IsLocalRing R] {E : Type v} [AddCommGroup E] [Module R E] {ι : IsLocalRing.ResidueField R →ₗ[R] E} [Small.{v, u} R] [Module.Injective R E] (hι : Function.Injective ⇑ι) (J : Ideal R) : (Submodule.torsionBySet R E ↑J).annihilator = J

If E is injective and contains a copy of the residue field, then the elements of E killed by an ideal J have annihilator exactly J.

theorem TauCeti.IsInjectiveEnvelope.length_linearMap {R : Type u} [CommRing R] [IsLocalRing R] {E : Type v} [AddCommGroup E] [Module R E] {ι : IsLocalRing.ResidueField R →ₗ[R] E} [Small.{v, u} R] (hι : IsInjectiveEnvelope ι) (M : Type w) [AddCommGroup M] [Module R M] : Module.length R (M →ₗ[R] E) = Module.length R M

Matlis duality preserves length. For an injective envelope E of the residue field of a local ring, Hom_R(M, E) has the same length as M, for every module M. In particular M has finite length exactly when its Matlis dual does.

theorem TauCeti.IsInjectiveEnvelope.bijective_applyₗ {R : Type u} [CommRing R] [IsLocalRing R] {E : Type v} [AddCommGroup E] [Module R E] {ι : IsLocalRing.ResidueField R →ₗ[R] E} [Small.{v, u} R] (hι : IsInjectiveEnvelope ι) {M : Type w} [AddCommGroup M] [Module R M] (hM : IsFiniteLength R M) : Function.Bijective ⇑LinearMap.applyₗ

Matlis biduality for modules of finite length. For an injective envelope E of the residue field of a local ring, the evaluation map M → Hom_R(Hom_R(M, E), E) is bijective for every module M of finite length.

noncomputable def TauCeti.IsInjectiveEnvelope.evalEquiv {R : Type u} [CommRing R] [IsLocalRing R] {E : Type v} [AddCommGroup E] [Module R E] {ι : IsLocalRing.ResidueField R →ₗ[R] E} [Small.{v, u} R] (hι : IsInjectiveEnvelope ι) {M : Type w} [AddCommGroup M] [Module R M] (hM : IsFiniteLength R M) : M ≃ₗ[R] (M →ₗ[R] E) →ₗ[R] E

Matlis biduality for a module M of finite length, as the linear equivalence M ≃ Hom_R(Hom_R(M, E), E) given by evaluation.

@[simp]

theorem TauCeti.IsInjectiveEnvelope.evalEquiv_apply_apply {R : Type u} [CommRing R] [IsLocalRing R] {E : Type v} [AddCommGroup E] [Module R E] {ι : IsLocalRing.ResidueField R →ₗ[R] E} [Small.{v, u} R] (hι : IsInjectiveEnvelope ι) {M : Type w} [AddCommGroup M] [Module R M] (hM : IsFiniteLength R M) (m : M) (f : M →ₗ[R] E) : ((hι.evalEquiv hM) m) f = f m

theorem TauCeti.IsInjectiveEnvelope.exists_eq_smul_subtype {R : Type u} [CommRing R] [IsLocalRing R] {E : Type v} [AddCommGroup E] [Module R E] {ι : IsLocalRing.ResidueField R →ₗ[R] E} [Small.{v, u} R] (hι : IsInjectiveEnvelope ι) {J : Ideal R} (hJ : IsFiniteLength R (R ⧸ J)) (g : ↥(Submodule.torsionBySet R E ↑J) →ₗ[R] E) : ∃ (r : R), g = r • (Submodule.torsionBySet R E ↑J).subtype

Linear maps out of a layer of the hull are scalar. Let E be an injective envelope of the residue field and J an ideal with R ⧸ J of finite length. Every linear map E[J] → E is the inclusion multiplied by a scalar.