Module

ClosedAndCosets.lean

Nyll.ProCGroups.ProC.OpenNormalSubgroups.ClosedAndCosets

4 declarations indexed from sourceView source ↗

Module documentation

Closed subgroups and cosets

This file expresses closed subgroups as intersections of open subgroups and develops separation by open subgroups. It also proves the disjointness and clopen properties of the relevant cosets.

Imports1

Nyll.ProCGroups.Profinite.OpenSubgroups

Imported by4

theorem

closedSubgroup_eq_sInf_open

L27 ↗

ProCGroups.ProC.closedSubgroup_eq_sInf_open

Documentation

A closed subgroup of a profinite group is the intersection of all open subgroups containing it.

Source context 4 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem closedSubgroup_eq_sInf_open [CompactSpace G] [TotallyDisconnectedSpace G]
    (H : ClosedSubgroup G) :
    (H : Subgroup G) = sInf {N : Subgroup G | IsOpen (N : Set G) ∧ (H : Subgroup G) ≤ N}

theorem

exists_not_mem_of_iInf_eq_bot

L77 ↗

ProCGroups.ProC.exists_not_mem_of_iInf_eq_bot

Documentation

If the intersection of a family of subgroups is trivial, every nonidentity element is omitted by at least one member of the family.

Source context 4 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {G : Type u} [Group G]

Lean source · statement

theorem exists_not_mem_of_iInf_eq_bot {ι : Type v} (U : ι → Subgroup G)
    (hU : iInf U = (⊥ : Subgroup G)) {x : G} (hx : x ≠ 1) :
    ∃ i : ι, x ∉ U i

theorem

disjoint_leftCoset_of_not_mem

L92 ↗

ProCGroups.ProC.disjoint_leftCoset_of_not_mem

Documentation

Distinct left cosets of a subgroup are disjoint.

Source context 4 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {G : Type u} [Group G]

Lean source · statement

theorem disjoint_leftCoset_of_not_mem (U : Subgroup G) {x y : G} (hxy : x⁻¹ * y ∉ U) :
    Disjoint {g : G | x⁻¹ * g ∈ U} {g : G | y⁻¹ * g ∈ U}

theorem

isClopen_leftCoset_openSubgroup

L103 ↗

ProCGroups.ProC.isClopen_leftCoset_openSubgroup

Documentation

The left coset of an open subgroup is clopen.

Source context 5 commands

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

namespace ProCGroups.ProC
universe u v
section
variable {G : Type u} [Group G]
variable [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem isClopen_leftCoset_openSubgroup (U : OpenSubgroup G) (x : G) :
    IsClopen {g : G | x⁻¹ * g ∈ (U : Subgroup G)}

Module documentation

Closed subgroups and cosets

Declarations

closedSubgroup_eq_sInf_open

exists_not_mem_of_iInf_eq_bot

disjoint_leftCoset_of_not_mem

isClopen_leftCoset_openSubgroup