NYLL
Module

OpenSubgroups.lean

Nyll.ProCGroups.Profinite.OpenSubgroups
11 declarations indexed from sourceView source ↗

Module documentation

Open subgroups of compact groups

This module records openness and closedness properties of open (normal) subgroups, constructs their pullbacks, and proves that they have finite index in compact topological groups.

Imports2
  • Mathlib.GroupTheory.OrderOfElement
  • Mathlib.Topology.Algebra.ClopenNhdofOne
Imported by10

Declarations

theorem

openSubgroup_isOpen

L29 ↗
ProCGroups.openSubgroup_isOpen
Documentation

An open subgroup is open as a subset.

Source context 6 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups
universe u v
section OpenSubgroups
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem openSubgroup_isOpen (U : OpenSubgroup G) :
    IsOpen ((U : Subgroup G) : Set G)
theorem

openSubgroup_isClosed

L34 ↗
ProCGroups.openSubgroup_isClosed
Documentation

An open subgroup is closed as a subset.

Source context 6 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups
universe u v
section OpenSubgroups
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem openSubgroup_isClosed [ContinuousMul G] (U : OpenSubgroup G) :
    IsClosed ((U : Subgroup G) : Set G)
theorem

openNormalSubgroup_isOpen

L39 ↗
ProCGroups.openNormalSubgroup_isOpen
Documentation

An open normal subgroup is open as a subset.

Source context 6 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups
universe u v
section OpenSubgroups
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem openNormalSubgroup_isOpen (U : OpenNormalSubgroup G) :
    IsOpen ((U : Subgroup G) : Set G)
theorem

openNormalSubgroup_isClosed

L44 ↗
ProCGroups.openNormalSubgroup_isClosed
Documentation

An open normal subgroup is closed as a subset.

Source context 6 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups
universe u v
section OpenSubgroups
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem openNormalSubgroup_isClosed [ContinuousMul G] (U : OpenNormalSubgroup G) :
    IsClosed ((U : Subgroup G) : Set G)
def

comap

L51 ↗
ProCGroups.OpenNormalSubgroup.comap
Documentation

Pull back an open normal subgroup along a continuous homomorphism.

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups
universe u v
section OpenSubgroups
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroup
Lean source · statement
def comap {H : Type v} [Group H] [TopologicalSpace H]
    (f : G →* H) (hf : Continuous f) (U : OpenNormalSubgroup H) : OpenNormalSubgroup G
theorem

toSubgroup_comap

L60 ↗
ProCGroups.OpenNormalSubgroup.toSubgroup_comap
Documentation

The subgroup underlying the comap of an open subgroup is the subgroup comap.

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups
universe u v
section OpenSubgroups
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroup
Lean source · statement
theorem toSubgroup_comap {H : Type v} [Group H] [TopologicalSpace H]
    (f : G →* H) (hf : Continuous f) (U : OpenNormalSubgroup H) :
    ((OpenNormalSubgroup.comap f hf U : OpenNormalSubgroup G) : Subgroup G) =
      (U : Subgroup H).comap f
theorem

mem_comap

L68 ↗
ProCGroups.OpenNormalSubgroup.mem_comap
Documentation

Membership in the comap of an open subgroup is membership after applying the homomorphism.

Source context 7 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups
universe u v
section OpenSubgroups
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace OpenNormalSubgroup
Lean source · statement
theorem mem_comap {H : Type v} [Group H] [TopologicalSpace H]
    {f : G →* H} {hf : Continuous f} {U : OpenNormalSubgroup H} {x : G} :
    x ∈ OpenNormalSubgroup.comap f hf U ↔ f x ∈ U
theorem

openSubgroup_finiteQuotient

L79 ↗
ProCGroups.openSubgroup_finiteQuotient
Documentation

An open subgroup of a compact topological group has finite coset space, equivalently finite index.

Source context 6 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups
universe u v
section OpenSubgroups
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem openSubgroup_finiteQuotient [ContinuousMul G] [CompactSpace G]
    (U : OpenSubgroup G) :
    Finite (G ⧸ (U : Subgroup G))
theorem

openNormalSubgroup_finiteQuotient

L85 ↗
ProCGroups.openNormalSubgroup_finiteQuotient
Documentation

Any open normal subgroup of a compact topological group has finite quotient.

Source context 6 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups
universe u v
section OpenSubgroups
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem openNormalSubgroup_finiteQuotient [ContinuousMul G] [CompactSpace G]
    (U : OpenNormalSubgroup G) :
    Finite (G ⧸ (U : Subgroup G))
theorem

exists_pos_pow_mem_openSubgroup

L92 ↗
ProCGroups.exists_pos_pow_mem_openSubgroup
Documentation

In a compact topological group, every element has a positive power in any open subgroup.

Source context 6 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups
universe u v
section OpenSubgroups
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem exists_pos_pow_mem_openSubgroup [ContinuousMul G] [CompactSpace G]
    (U : OpenSubgroup G) (g : G) :
    ∃ n : ℕ, 0 < n ∧ g ^ n ∈ (U : Subgroup G)
theorem

subgroup_isOpen_iff_isClosed_finite_quotient

L109 ↗
ProCGroups.subgroup_isOpen_iff_isClosed_finite_quotient
Documentation

In a compact topological group, a subgroup is open if and only if it is closed and the quotient is finite. Equivalently, the subgroup is closed of finite index; in this version, Finite (\(G/U\)) is the most direct encoding of finite index.

Source context 6 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups
universe u v
section OpenSubgroups
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
theorem subgroup_isOpen_iff_isClosed_finite_quotient [ContinuousMul G] [CompactSpace G]
    {U : Subgroup G} :
    IsOpen (U : Set G) ↔ IsClosed (U : Set G) ∧ Finite (G ⧸ U)

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