ProCGroups.Profinite.OpenSubgroups

10 Theorem | 1 Definition

This module studies open subgroups for pro cgroups. An open subgroup is open as a subset. An open subgroup is closed as a subset.

Open this file on GitHub

import

Mathlib.GroupTheory.OrderOfElement
Mathlib.Topology.Algebra.ClopenNhdofOne

Imported by

Theorem ProCGroups.openSubgroup_isOpen GitHub

theorem openSubgroup_isOpen (U : OpenSubgroup G) :
    IsOpen ((U : Subgroup G) : Set G)

An open subgroup is open as a subset.

Show proof

Theorem ProCGroups.openSubgroup_isClosed GitHub

theorem openSubgroup_isClosed [ContinuousMul G] (U : OpenSubgroup G) :
    IsClosed ((U : Subgroup G) : Set G)

An open subgroup is closed as a subset.

Show proof

Theorem ProCGroups.openNormalSubgroup_isOpen GitHub

theorem openNormalSubgroup_isOpen (U : OpenNormalSubgroup G) :
    IsOpen ((U : Subgroup G) : Set G)

An open normal subgroup is open as a subset.

Show proof

Theorem ProCGroups.openNormalSubgroup_isClosed GitHub

theorem openNormalSubgroup_isClosed [ContinuousMul G] (U : OpenNormalSubgroup G) :
    IsClosed ((U : Subgroup G) : Set G)

An open normal subgroup is closed as a subset.

Show proof

Definition ProCGroups.OpenNormalSubgroup.comap GitHub

def comap {H : Type v} [Group H] [TopologicalSpace H]
    (f : G →* H) (hf : Continuous f) (U : OpenNormalSubgroup H) : OpenNormalSubgroup G :=
  { toOpenSubgroup := U.toOpenSubgroup.comap f hf
    isNormal' := by
      change ((U : Subgroup H).comap f).Normal
      infer_instance }

Pull back an open normal subgroup along a continuous homomorphism.

Theorem ProCGroups.OpenNormalSubgroup.toSubgroup_comap GitHub

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

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

Show proof

Theorem ProCGroups.OpenNormalSubgroup.mem_comap GitHub

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

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

Show proof

Theorem ProCGroups.openSubgroup_finiteQuotient GitHub

theorem openSubgroup_finiteQuotient [ContinuousMul G] [CompactSpace G]
    (U : OpenSubgroup G) :
    Finite (G ⧸ (U : Subgroup G))

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

Show proof

Theorem ProCGroups.openNormalSubgroup_finiteQuotient GitHub

theorem openNormalSubgroup_finiteQuotient [ContinuousMul G] [CompactSpace G]
    (U : OpenNormalSubgroup G) :
    Finite (G ⧸ (U : Subgroup G))

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

Show proof

Theorem ProCGroups.exists_pos_pow_mem_openSubgroup GitHub

theorem exists_pos_pow_mem_openSubgroup [ContinuousMul G] [CompactSpace G]
    (U : OpenSubgroup G) (g : G) :
    ∃ n : ℕ, 0 < n ∧ g ^ n ∈ (U : Subgroup G)

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

Show proof

Theorem ProCGroups.subgroup_isOpen_iff_isClosed_finite_quotient GitHub

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)

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.

Show proof

ProCGroups.Profinite.OpenSubgroups

Declarations