EtaleFundamentalGroups.Purity.isEssentialSubmodule_comap_subtype_iff
Essentiality in a submodule is equivalent to the ambient disjointness test restricted to submodules lying in that submodule.
Source context 4 commands
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]Lean source · statement
theorem isEssentialSubmodule_comap_subtype_iff
(N S : Submodule R M) (hNS : N ≤ S) :
IsEssentialSubmodule (N.comap S.subtype) ↔
∀ L : Submodule R M, L ≤ S → Disjoint N L → L = ⊥