NYLL
Module

InjectiveModuleEnvelope.lean

Nyll.EtaleFundamentalGroups.Purity.InjectiveModuleEnvelope
1 declaration indexed from sourceView source ↗

Module documentation

Injective envelopes inside an injective ambient module

Choose a maximal essential extension E of a submodule N inside an injective module M. Quotienting M by a maximal submodule disjoint from E gives an essential extension of E. Injectivity of M extends the inclusion of E to a map from this quotient into M. Its image is again an essential extension of N, hence equals E by maximality.

The resulting map M → E retracts the inclusion. Extending maps from ideals into M and composing with this retraction proves Baer's criterion for E.

Imports7
Imported by2

Declarations

theorem

exists_injective_essential_extension

L35 ↗
EtaleFundamentalGroups.Purity.exists_injective_essential_extension
Documentation

A submodule of an injective module admits an injective essential extension within that same ambient module.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace EtaleFundamentalGroups.Purity
universe u
Lean source · statement
theorem exists_injective_essential_extension
    {R M : Type u} [Ring R] [AddCommGroup M] [Module R M]
    [Module.Injective R M] (N : Submodule R M) :
    ∃ E : Submodule R M, N ≤ E ∧
      IsEssentialSubmodule (N.comap E.subtype) ∧ Module.Injective R E

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.