Existence of injective envelopes

Every module has an injective envelope (Eckmann–Schopf). More precisely, every embedding i : M →ₗ[R] Q into an injective module restricts to an injective envelope of M inside Q (LinearMap.exists_isInjectiveEnvelope_submodule), and since every module embeds into an injective module, every module has an injective envelope in its own universe (TauCeti.exists_isInjectiveEnvelope). By TauCeti.IsInjectiveEnvelope.exists_linearEquiv this envelope is unique up to isomorphism. In particular this provides the injective hull E(k) of the residue field of a local ring, the dualizing module of Matlis duality.

The envelope is a maximal essential extension E of the image of M inside Q, which exists by Zorn's lemma: a union of a chain of essential extensions is an essential extension (TauCeti.isEssential_comap_subtype_sSup). To see that E is injective, choose by Zorn's lemma a submodule K of Q maximal among those disjoint from E. Then E embeds in Q ⧸ K with essential image (TauCeti.isEssential_range_mkQ_comp_subtype), the inclusion of E into Q extends along this embedding to a map φ : Q ⧸ K →ₗ[R] Q, and the essential image forces φ to be injective. The range of φ is then an essential extension of M containing E, hence equals E, so Q → Q ⧸ K → E retracts Q onto E and E is injective as a retract of an injective module.

Main results

• LinearMap.exists_isInjectiveEnvelope_submodule: an embedding into an injective module restricts to an injective envelope inside that module.
• TauCeti.exists_isInjectiveEnvelope: every module has an injective envelope.

References

• B. Eckmann, A. Schopf, Über injektive Moduln, Arch. Math. 4 (1953), 75–78.
• T. Y. Lam, Lectures on Modules and Rings, §3D.

theorem LinearMap.exists_isInjectiveEnvelope_submodule {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {Q : Type w} [AddCommGroup Q] [Module R Q] [Module.Injective R Q] (i : M →ₗ[R] Q) (hi : Function.Injective ⇑i) : ∃ (P : Submodule R Q) (hP : i.range ≤ P), TauCeti.IsInjectiveEnvelope (codRestrict P i ⋯)

Injective envelopes inside an injective module. Every embedding into an injective module restricts to an injective envelope inside that module: some submodule P of Q containing the image is injective, with the image essential in P.

theorem TauCeti.exists_isInjectiveEnvelope (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] [Small.{v, u} R] : ∃ (Q : Type v) (x : AddCommGroup Q) (x_1 : Module R Q) (i : M →ₗ[R] Q), IsInjectiveEnvelope i

Existence of injective envelopes. Every module has an injective envelope, in its own universe.