Module

OpenSubgroup.lean

Nyll.ProCGroups.Topologies.OpenSubgroup

3 declarations indexed from sourceView source ↗

Module documentation

The whole group as an open subgroup

This file records the canonical continuous multiplicative equivalence between a topological group and the subtype of its top open subgroup, together with its forward and inverse formulas.

Imports2

Mathlib.Topology.Algebra.OpenSubgroup
Mathlib.Topology.Algebra.ContinuousMonoidHom

Imported by4

def

topContinuousMulEquiv

L26 ↗

ProCGroups.OpenSubgroup.topContinuousMulEquiv

Documentation

The \(\top\) open subgroup is canonically equivalent to the ambient topological group.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups
namespace OpenSubgroup
universe u

Lean source · statement

def topContinuousMulEquiv
    (G : Type u) [TopologicalSpace G] [Group G] :
    ↥((⊤ : OpenSubgroup G) : Subgroup G) ≃ₜ* G

theorem

topContinuousMulEquiv_apply

L48 ↗

ProCGroups.OpenSubgroup.topContinuousMulEquiv_apply

Documentation

The open-subgroup comparison equivalence evaluates on representatives.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups
namespace OpenSubgroup
universe u

Lean source · statement

theorem topContinuousMulEquiv_apply
    (G : Type u) [TopologicalSpace G] [Group G]
    (x : ↥((⊤ : OpenSubgroup G) : Subgroup G)) :
    topContinuousMulEquiv G x = x.1

theorem

topContinuousMulEquiv_symm_apply

L58 ↗

ProCGroups.OpenSubgroup.topContinuousMulEquiv_symm_apply

Documentation

The inverse comparison equivalence is evaluated by the same coordinate data, read in the opposite direction.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups
namespace OpenSubgroup
universe u

Lean source · full declaration

theorem topContinuousMulEquiv_symm_apply
    (G : Type u) [TopologicalSpace G] [Group G] (x : G) :
    (topContinuousMulEquiv G).symm x = ⟨x, by simp only [_root_.OpenSubgroup.toSubgroup_top,
        Subgroup.mem_top]⟩ :=
  rfl

Module documentation

The whole group as an open subgroup

Declarations

topContinuousMulEquiv

topContinuousMulEquiv_apply

topContinuousMulEquiv_symm_apply