A submodule is essential if every submodule disjoint from it is zero. For any submodule N of M, Zorn's lemma gives a maximal submodule P disjoint from N. The image of N in M / P is then essential: the inverse image of a submodule disjoint from that image is a larger submodule disjoint from N, so maximality forces it to equal P.
An essential submodule meets every nonzero submodule nontrivially.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Purity
universe u v
variable {R : Type u} [Ring R]
variable {M : Type v} [AddCommGroup M] [Module R M]def IsEssentialSubmodule (N : Submodule R M) : PropEvery submodule has a submodule maximal among those disjoint from it. The maximality assertion concerns actual submodules of the given ambient module, so no choice of a larger universe is required.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Purity
universe u v
variable {R : Type u} [Ring R]
variable {M : Type v} [AddCommGroup M] [Module R M]theorem exists_maximal_disjoint_submodule (N : Submodule R M) :
∃ P : Submodule R M, Disjoint N P ∧
∀ L : Submodule R M, Disjoint N L → P ≤ L → L = PQuotienting by a maximal disjoint submodule gives an essential extension of the image of the original submodule.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Purity
universe u v
variable {R : Type u} [Ring R]
variable {M : Type v} [AddCommGroup M] [Module R M]theorem exists_disjoint_essential_quotient (N : Submodule R M) :
∃ P : Submodule R M, Disjoint N P ∧
IsEssentialSubmodule (N.map P.mkQ)