Injective cogenerators over a commutative ring

Let R be a commutative ring and E an injective R-module, with dual D(M) = Hom_R(M, E). This file isolates what E must satisfy for D to behave like Matlis duality. If E receives a nonzero map from R ⧸ 𝔪 for every maximal ideal 𝔪, then E is a cogenerator. If moreover each Hom_R(R ⧸ 𝔪, E) has length one, then D preserves length, by induction on a composition series and exactness of Hom_R(-, E), and the evaluation map M → D(D(M)) is bijective for every module of finite length, an injective map between modules of the same finite length being bijective.

Main results

• TauCeti.injective_applyₗ_of_forall_isMaximal: an injective module receiving a nonzero map from every R ⧸ 𝔪 is a cogenerator.
• TauCeti.length_linearMap_of_isSimpleModule: if each Hom_R(R ⧸ 𝔪, E) has length one, then so does Hom_R(S, E) for every simple module S; injectivity of E is not needed.
• TauCeti.length_linearMap_of_forall_isMaximal and TauCeti.bijective_applyₗ_of_forall_isMaximal: if moreover E is injective, then D preserves length and biduality holds for modules of finite length.

References

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

theorem TauCeti.injective_applyₗ_of_forall_isMaximal {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] [Module.Injective R E] [Small.{v, u} R] (hE : ∀ (𝔪 : Ideal R), 𝔪.IsMaximal → Nontrivial (R ⧸ 𝔪 →ₗ[R] E)) {M : Type w} [AddCommGroup M] [Module R M] : Function.Injective ⇑LinearMap.applyₗ

A cogenerator test. An injective module E that receives a nonzero map from R ⧸ 𝔪 for every maximal ideal 𝔪 is a cogenerator: the evaluation map M → Hom_R(Hom_R(M, E), E) is injective for every module M.

theorem TauCeti.length_linearMap_of_isSimpleModule {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] (hE : ∀ (𝔪 : Ideal R), 𝔪.IsMaximal → Module.length R (R ⧸ 𝔪 →ₗ[R] E) = 1) {S : Type w} [AddCommGroup S] [Module R S] [IsSimpleModule R S] : Module.length R (S →ₗ[R] E) = 1

If Hom_R(R ⧸ 𝔪, E) has length one for every maximal ideal 𝔪, then Hom_R(S, E) has length one for every simple module S.

theorem TauCeti.length_linearMap_of_forall_isMaximal {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] [Module.Injective R E] [Small.{v, u} R] (hE : ∀ (𝔪 : Ideal R), 𝔪.IsMaximal → Module.length R (R ⧸ 𝔪 →ₗ[R] E) = 1) (M : Type w) [AddCommGroup M] [Module R M] : Module.length R (M →ₗ[R] E) = Module.length R M

The dual preserves length. If E is injective and Hom_R(R ⧸ 𝔪, E) has length one for every maximal ideal 𝔪, then Hom_R(M, E) has the same length as M, for every module M. In particular M has finite length exactly when its dual does.

theorem TauCeti.bijective_applyₗ_of_forall_isMaximal {R : Type u} [CommRing R] {E : Type v} [AddCommGroup E] [Module R E] [Module.Injective R E] [Small.{v, u} R] (hE : ∀ (𝔪 : Ideal R), 𝔪.IsMaximal → Module.length R (R ⧸ 𝔪 →ₗ[R] E) = 1) {M : Type w} [AddCommGroup M] [Module R M] (hM : IsFiniteLength R M) : Function.Bijective ⇑LinearMap.applyₗ

Biduality for modules of finite length. If E is injective and Hom_R(R ⧸ 𝔪, E) has length one for every maximal ideal 𝔪, then the evaluation map M → Hom_R(Hom_R(M, E), E) is bijective for every module M of finite length.