Module

OpenSubgroupSections.lean

Nyll.ProCGroups.ProC.Quotients.OpenSubgroupSections

6 declarations indexed from sourceView source ↗

Module documentation

Sections for quotients by open subgroups

Finite quotients by open subgroups admit normalized choice sections, which are continuous because the quotient is discrete. This file records their right-inverse property and derives sections of left-quotient projections with an open lower subgroup.

Imports2

Mathlib.Topology.Algebra.ProperAction.Basic
Nyll.ProCGroups.ProC.Quotients.ClosedSubgroupNeighborhoods

Imported by3

def

quotientOpenSubgroupSection

L33 ↗

ProCGroups.ProC.quotientOpenSubgroupSection

Documentation

A normalized set-theoretic section of the quotient map by an open subgroup. Since the quotient is discrete, this section is automatically continuous.

Source context 6 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.ProC
universe u v
open InverseSystems
variable {G : Type u} [Group G]

Lean source · statement

def quotientOpenSubgroupSection (U : Subgroup G) :
    (G ⧸ U) → G

theorem

quotientOpenSubgroupSection_one

L41 ↗

ProCGroups.ProC.quotientOpenSubgroupSection_one

Documentation

The normalized set-theoretic section sends the identity coset to the identity.

Source context 6 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.ProC
universe u v
open InverseSystems
variable {G : Type u} [Group G]

Lean source · statement

theorem quotientOpenSubgroupSection_one
    (U : Subgroup G) :
    quotientOpenSubgroupSection U (QuotientGroup.mk (s := U) (1 : G)) = 1

theorem

quotientOpenSubgroupSection_rightInverse

L48 ↗

ProCGroups.ProC.quotientOpenSubgroupSection_rightInverse

Documentation

The normalized section is a genuine right inverse to the quotient map.

Source context 6 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.ProC
universe u v
open InverseSystems
variable {G : Type u} [Group G]

Lean source · statement

theorem quotientOpenSubgroupSection_rightInverse
    (U : Subgroup G) :
    Function.RightInverse (quotientOpenSubgroupSection U)
      (QuotientGroup.mk (s := U))

theorem

continuous_quotientOpenSubgroupSection

L61 ↗

ProCGroups.ProC.continuous_quotientOpenSubgroupSection

Documentation

The normalized section by an open subgroup is continuous because the quotient is discrete.

Source context 6 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.ProC
universe u v
open InverseSystems
variable {G : Type u} [Group G]

Lean source · statement

theorem continuous_quotientOpenSubgroupSection
    [TopologicalSpace G]
    [IsTopologicalGroup G]
    (U : Subgroup G) (hU : IsOpen (U : Set G)) :
    Continuous (quotientOpenSubgroupSection U)

theorem

quotient_openNormalSubgroup_hasContinuousSection

L74 ↗

ProCGroups.ProC.quotient_openNormalSubgroup_hasContinuousSection

Documentation

Helper for the finite/open case: the canonical quotient map by an open normal subgroup of a profinite group admits a continuous section normalized by \(s(1)=1\). The actual section data is provided by quotientOpenSubgroupSection.

Source context 6 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.ProC
universe u v
open InverseSystems
variable {G : Type u} [Group G]

Lean source · statement

theorem quotient_openNormalSubgroup_hasContinuousSection
    [TopologicalSpace G]
    [IsTopologicalGroup G]
    (U : OpenNormalSubgroup G) :
    ∃ σ : (G ⧸ (U : Subgroup G)) → G,
      Continuous σ ∧
        Function.RightInverse σ (QuotientGroup.mk' (U : Subgroup G)) ∧
        σ 1 = 1

theorem

leftQuotientProjection_hasContinuousSection_of_openSubgroup

L94 ↗

ProCGroups.ProC.leftQuotientProjection_hasContinuousSection_of_openSubgroup

Documentation

Finite-index case of the section theorem for left quotient projections.

Source context 6 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.ProC
universe u v
open InverseSystems
variable {G : Type u} [Group G]

Lean source · statement

theorem leftQuotientProjection_hasContinuousSection_of_openSubgroup
    [TopologicalSpace G]
    [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (K H : ClosedSubgroup G)
    (hKH : (K : Subgroup G) ≤ (H : Subgroup G))
    (hKopen : IsOpen (((K : Subgroup G).subgroupOf (H : Subgroup G)) : Set H)) :
    ∃ σ : G ⧸ (H : Subgroup G) → G ⧸ (K : Subgroup G),
    Continuous σ ∧
      Function.RightInverse σ
        (leftQuotientProjection (K : Subgroup G) (H : Subgroup G) hKH) ∧
      σ (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)) =
        QuotientGroup.mk (s := (K : Subgroup G)) (1 : G)

Module documentation

Sections for quotients by open subgroups

Declarations

quotientOpenSubgroupSection

quotientOpenSubgroupSection_one

quotientOpenSubgroupSection_rightInverse

continuous_quotientOpenSubgroupSection

quotient_openNormalSubgroup_hasContinuousSection

leftQuotientProjection_hasContinuousSection_of_openSubgroup