Matlis duality over a semilocal ring

Let R be a commutative ring whose quotient R ⧸ J(R) by the Jacobson radical is a semisimple ring, for instance a commutative Artinian ring. This file proves Matlis duality for modules of finite length over R, with dualizing module an injective hull E of R ⧸ J(R): the dual D(M) = Hom_R(M, E) has the same length as M, and the evaluation map M → D(D(M)) is an isomorphism for every M of finite length. Over a commutative Artinian ring E itself has finite length, so D sends modules of finite length to modules of finite length and is inverse to itself there up to evaluation. No locality is assumed; over a local ring R ⧸ J(R) is the residue field, the case treated in TauCeti/RingTheory/MatlisDuality/FiniteLength.lean.

The argument applies the cogenerator criteria of TauCeti/Algebra/Module/Injective/Cogenerator.lean: an injective module E such that Hom_R(R ⧸ 𝔪, E) has length one for every maximal ideal 𝔪 gives a duality preserving length, with biduality on modules of finite length. For the injective hull of R ⧸ J(R), every map from R ⧸ 𝔪 lands in the essential image of R ⧸ J(R), and Hom_R(R ⧸ 𝔪, R ⧸ J(R)) is simple: it is nonzero because the semisimple module R ⧸ J(R) has R ⧸ 𝔪 as a direct summand, and it is at most one-dimensional over R ⧸ 𝔪 because J(R) is a radical ideal.

Main results

• Ideal.length_linearMap_quotient_jacobson_eq_one: Hom_R(R ⧸ 𝔪, R ⧸ J(R)) has length one.
• TauCeti.IsInjectiveEnvelope.length_linearMap_quotient_jacobson and TauCeti.IsInjectiveEnvelope.bijective_applyₗ_quotient_jacobson: Matlis duality for modules of finite length over R.
• TauCeti.IsInjectiveEnvelope.isFiniteLength_quotient_jacobson and TauCeti.exists_isInjectiveEnvelope_quotient_jacobson: over a commutative Artinian ring, every injective hull of R ⧸ J(R) has finite length, and one exists in the universe of R.

References

• M. Auslander, I. Reiten, S. O. Smalø, Representation Theory of Artin Algebras, Section II.3, Theorems 3.1 and 3.3.
• The Stacks Project, Section 47.7, Matlis duality, Tag 08Z1.

theorem Ideal.length_linearMap_quotient_jacobson_eq_one {R : Type u} [CommRing R] [IsSemisimpleRing (R ⧸ Ring.jacobson R)] (𝔪 : Ideal R) [h𝔪 : 𝔪.IsMaximal] : Module.length R (R ⧸ 𝔪 →ₗ[R] R ⧸ Ring.jacobson R) = 1

Each simple module occurs once in R ⧸ J(R). If R ⧸ J(R) is a semisimple ring, then for every maximal ideal 𝔪 the module Hom_R(R ⧸ 𝔪, R ⧸ J(R)) is simple.

theorem TauCeti.IsInjectiveEnvelope.length_linearMap_quotient_jacobson {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} (hf : IsInjectiveEnvelope f) (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 hull E of R ⧸ J(R), where R ⧸ J(R) is a semisimple ring, Hom_R(M, E) has the same length as M, for every module M.

theorem TauCeti.IsInjectiveEnvelope.bijective_applyₗ_quotient_jacobson {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} (hf : IsInjectiveEnvelope f) {M : Type w} [AddCommGroup M] [Module R M] (hM : IsFiniteLength R M) : Function.Bijective ⇑LinearMap.applyₗ

Matlis biduality over a semilocal ring. For an injective hull E of R ⧸ J(R), where R ⧸ J(R) is a semisimple ring, the evaluation map M → Hom_R(Hom_R(M, E), E) is bijective for every module M of finite length.

theorem TauCeti.IsInjectiveEnvelope.isFiniteLength_quotient_jacobson {R : Type u} [CommRing R] [IsArtinianRing R] {E : Type v} [AddCommGroup E] [Module R E] [Small.{v, u} R] {f : R ⧸ Ring.jacobson R →ₗ[R] E} (hf : IsInjectiveEnvelope f) : IsFiniteLength R E

Over a commutative Artinian ring, every injective hull of R ⧸ J(R) has finite length.

theorem TauCeti.exists_isInjectiveEnvelope_quotient_jacobson (R : Type u) [CommRing R] [IsArtinianRing R] : ∃ (E : Type u) (x : AddCommGroup E) (x_1 : Module R E) (f : R ⧸ Ring.jacobson R →ₗ[R] E), IsInjectiveEnvelope f ∧ IsFiniteLength R E

The injective cogenerator of a commutative Artinian ring. R ⧸ J(R) has an injective hull of finite length.