Injective envelopes inside finite-length injectives

Every embedding into a finite-length injective module can be restricted to an injective envelope. Thus, to obtain finite-length injective envelopes, it suffices to construct finite-length injective modules containing the modules in question. This is useful for finite-dimensional algebras, where finite powers of the dual regular module provide such embeddings.

The ambient ring and module may have different universes; Small is needed for the universe-polymorphic extension property of an injective module.

References

• T. Y. Lam, Lectures on Modules and Rings, Section 3.

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

Every embedding into a finite-length injective module restricts to an injective envelope inside that ambient module. In particular the envelope is itself of finite length.