Injective envelopes

An injective envelope of a module M is an embedding f : M →ₗ[R] Q into an injective module whose image is essential in Q (TauCeti.IsEssential). This is the notion dual to the projective cover of TauCeti/Algebra/Module/ProjectiveCover/Basic.lean; Mathlib has injective objects but no injective envelopes, and this file supplies the predicate together with the two facts everything downstream rests on.

Both rest on the minimality packaged in TauCeti.IsEssential.injective_of_injective_comp: a map out of the target of an envelope whose composite with the envelope is injective is itself injective, the image of an envelope being too large for the kernel of such a map to avoid it. This is the sense in which the essential-image condition makes an envelope minimal, and read backwards it is TauCeti.isInjectiveEnvelope_iff_forall_injective: the envelopes of M are exactly the essential monomorphisms from M into an injective module.

The first fact is that an essential extension maps into every embedding into an injective module: if Q' is injective and g : M →ₗ[R] Q' is injective, then g factors as h ∘ₗ f with h : Q →ₗ[R] Q' injective (TauCeti.IsEssential.exists_injective, stated at the essential-monomorphism level its proof uses and specialized to an envelope through TauCeti.IsInjectiveEnvelope.isEssential_range). The second is that an injective envelope is unique: any two injective envelopes of M differ by a linear equivalence commuting with the structure maps (TauCeti.IsInjectiveEnvelope.exists_linearEquiv). Uniqueness is what makes "the" injective envelope a well-defined object.

Existence of injective envelopes is a separate matter, and is not proved here; nothing below assumes it, every statement being conditional on an envelope being given. Over a finite-dimensional algebra the indecomposable injectives arise as the envelopes of the simple modules.

Universes

Mathlib's Module.Injective states its extension property only for source and target in the universe of the injective module, and the universe-polymorphic form Module.Injective.extension_property costs a Small.{·} R hypothesis on the ring. That hypothesis is carried here on exactly the results that extend a map along an embedding, once per module used as an extension target; it is automatic whenever R and that module live in the same universe.

Main definitions

• TauCeti.IsInjectiveEnvelope: f : M →ₗ[R] Q is injective, Q is an injective module, and the range of f is essential.

Main results

• TauCeti.isInjectiveEnvelope_id: an injective module is its own injective envelope.
• TauCeti.isInjectiveEnvelope_iff_forall_injective: an embedding into an injective module is an injective envelope exactly when it is an essential monomorphism.
• TauCeti.IsEssential.exists_injective: a given embedding of M with essential range maps, by an embedding, into every embedding of M into an injective module. When its own target is moreover injective — that is, when the given embedding is an injective envelope — this is the universal property of the envelope.
• TauCeti.IsInjectiveEnvelope.bijective_of_comp_eq and TauCeti.IsInjectiveEnvelope.exists_linearEquiv: uniqueness, first as bijectivity of any comparison map between two envelopes and then as the existence of an isomorphism under M.
• TauCeti.IsInjectiveEnvelope.comp: precomposing an injective envelope with an embedding that itself has essential range again gives an injective envelope.
• TauCeti.isInjectiveEnvelope_subtype_iff: the concrete family of envelopes, N ↪ Q is an injective envelope of a submodule N of an injective Q exactly when N is essential; over an atomic submodule lattice TauCeti.isEssential_iff_forall_atom_le reads this off the simple submodules.

References

This implements the injective-envelope half of the "projective covers and injective envelopes" bullet of Layer 3 of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md ("dually injectiveEnvelope M"), whose projective half is TauCeti/Algebra/Module/ProjectiveCover/Basic.lean. As on the projective side, the bullet is not discharged by this file: existence of envelopes, and hence a canonical injectiveEnvelope M chosen by it, remains.

See I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, Section I.5, and T. Y. Lam, Lectures on Modules and Rings, §3.

structure TauCeti.IsInjectiveEnvelope {R : Type u} {M : Type v} {Q : Type w} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup Q] [Module R Q] (f : M →ₗ[R] Q) : Prop

An injective envelope of M: an embedding into an injective module whose range is essential. The essential range is the minimality of the envelope: it says exactly that no proper submodule of Q containing the image can be split off, equivalently that every map out of Q whose composite with f is injective is injective already (TauCeti.isInjectiveEnvelope_iff_forall_injective).

• moduleInjective : Module.Injective R Q

  The ambient module is injective.

• injective : Function.Injective ⇑f

  The structure map is an embedding.

• isEssential_range : IsEssential f.range

  Minimality: the range is essential, so the envelope cannot be shrunk.

theorem TauCeti.isInjectiveEnvelope_id {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module.Injective R M] : IsInjectiveEnvelope LinearMap.id

An injective module is its own injective envelope, along the identity.

theorem TauCeti.isInjectiveEnvelope_iff_forall_injective {R : Type u} {M : Type v} {Q : Type w} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup Q] [Module R Q] [Module.Injective R Q] {f : M →ₗ[R] Q} (hf : Function.Injective ⇑f) : IsInjectiveEnvelope f ↔ ∀ {Q' : Type w} [inst : AddCommMonoid Q'] [inst_1 : Module R Q'] (h : Q →ₗ[R] Q'), Function.Injective ⇑(h ∘ₗ f) → Function.Injective ⇑h

Injective envelopes are the essential monomorphisms into an injective module. An embedding f : M →ₗ[R] Q into an injective module is an injective envelope exactly when every map out of Q whose composite with f is injective is itself injective.

theorem TauCeti.IsEssential.exists_injective {R : Type u} {M : Type v} {Q : Type w} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup Q] [Module R Q] [Small.{w', u} R] {Q' : Type w'} [AddCommGroup Q'] [Module R Q'] [Module.Injective R Q'] {f : M →ₗ[R] Q} (hrange : IsEssential f.range) (hf : Function.Injective ⇑f) {g : M →ₗ[R] Q'} (hg : Function.Injective ⇑g) : ∃ (h : Q →ₗ[R] Q'), h ∘ₗ f = g ∧ Function.Injective ⇑h

An essential embedding maps into every embedding into an injective module. An embedding f : M →ₗ[R] Q with essential range receives every embedding of M into an injective module, by an embedding. Injectivity of Q plays no part, so this holds of any essential extension of M; applied through TauCeti.IsInjectiveEnvelope.isEssential_range it is the universal property of the injective envelope.

theorem TauCeti.IsInjectiveEnvelope.bijective_of_comp_eq {R : Type u} {M : Type v} {Q : Type w} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup Q] [Module R Q] [Small.{w, u} R] {Q' : Type u_1} [AddCommGroup Q'] [Module R Q'] {f : M →ₗ[R] Q} {f' : M →ₗ[R] Q'} (hf : IsInjectiveEnvelope f) (hf'inj : Function.Injective ⇑f') (hf'range : IsEssential f'.range) {h : Q →ₗ[R] Q'} (hcomp : h ∘ₗ f = f') : Function.Bijective ⇑h

Uniqueness of the injective envelope, in comparison-map form. A map from the target of an injective envelope of M to an essential extension of M that commutes with the structure maps is automatically an isomorphism; the target need only be an essential extension, not itself an envelope.

theorem TauCeti.IsInjectiveEnvelope.exists_linearEquiv {R : Type u} {M : Type v} {Q : Type w} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup Q] [Module R Q] [Small.{w, u} R] [Small.{w', u} R] {Q' : Type w'} [AddCommGroup Q'] [Module R Q'] {f : M →ₗ[R] Q} {f' : M →ₗ[R] Q'} (hf : IsInjectiveEnvelope f) (hf' : IsInjectiveEnvelope f') : ∃ (e : Q ≃ₗ[R] Q'), ↑e ∘ₗ f = f'

Uniqueness of the injective envelope. Two injective envelopes of the same module are related by a linear equivalence commuting with the structure maps; in particular the ambient module of an injective envelope is well defined up to isomorphism.

theorem TauCeti.IsInjectiveEnvelope.comp {R : Type u} {M : Type v} {Q : Type w} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup Q] [Module R Q] {N : Type u_1} [AddCommGroup N] [Module R N] {f : M →ₗ[R] Q} (hf : IsInjectiveEnvelope f) {g : N →ₗ[R] M} (hg : Function.Injective ⇑g) (hgrange : IsEssential g.range) : IsInjectiveEnvelope (f ∘ₗ g)

Precomposing an injective envelope with an embedding whose range is essential again gives an injective envelope.

Submodules

The inclusions of an injective module are the source of concrete injective envelopes: a submodule of an injective module is enveloped by it exactly when it is essential.

@[simp]

theorem TauCeti.isInjectiveEnvelope_subtype_iff {R : Type u} {Q : Type w} [Ring R] [AddCommGroup Q] [Module R Q] [Module.Injective R Q] {N : Submodule R Q} : IsInjectiveEnvelope N.subtype ↔ IsEssential N

When the inclusion of a submodule of an injective module is an injective envelope. The inclusion N →ₗ[R] Q of a submodule of an injective module is an injective envelope precisely when N is essential.