NYLL
Module

EssentialModuleMaximalExtension.lean

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

Module documentation

Maximal essential extensions inside a fixed module

Zorn's lemma applied to essential extensions of a given submodule produces a maximal one inside the chosen ambient module. For a chain, essentiality of the supremum is checked elementwise: an element of a disjoint submodule already belongs to one member of the chain and hence must vanish there. This keeps the construction in the original universe.

Imports2
Imported by2

Declarations

theorem

exists_maximal_essential_extension

L29 ↗
EtaleFundamentalGroups.Purity.exists_maximal_essential_extension
Documentation

A submodule admits a maximal essential extension inside any fixed ambient module.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Purity
universe u v
variable {R : Type u} [Ring R]
  {M : Type v} [AddCommGroup M] [Module R M]
Lean source · statement
theorem exists_maximal_essential_extension (N : Submodule R M) :
    ∃ E : Submodule R M, N ≤ E ∧
      IsEssentialSubmodule (N.comap E.subtype) ∧
      ∀ S : Submodule R M, E ≤ S →
        IsEssentialSubmodule (N.comap S.subtype) → S = E

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