NYLL
Module

RightQuotient.lean

Nyll.ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.RightQuotient
13 declarations indexed from sourceView source ↗

Module documentation

Right cosets of open subgroups

For an open subgroup this module specializes the right-coset space used by Schreier rewriting. It supplies the coset action, finiteness under compactness, the discrete quotient topology, and a normalized continuous section of the right-coset projection.

Imports2
Imported by2

Declarations

instance

compactSpace_openSubgroupSubtype

L37 ↗
ReidemeisterSchreier.Profinite.compactSpace_openSubgroupSubtype
Documentation

An open subgroup of a compact topological group is compact in its subtype topology. This standard instance is shared by the bundled profinite and pro-\(C\) subgroup carriers.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.ProC
universe u
section RightQuotientSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
Lean source · statement
instance compactSpace_openSubgroupSubtype
    (H : OpenSubgroup F) [CompactSpace F] :
    CompactSpace ↥(H : Subgroup F)
abbrev

OpenSubgroupRightQuotient

L45 ↗
ReidemeisterSchreier.Profinite.OpenSubgroupRightQuotient
Documentation

The right-coset space \(F/H\), encoded via right quotients.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.ProC
universe u
section RightQuotientSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
Lean source · statement
abbrev OpenSubgroupRightQuotient (H : OpenSubgroup F)
def

openSubgroupRightCoset

L49 ↗
ReidemeisterSchreier.Profinite.openSubgroupRightCoset
Documentation

The right coset of an element modulo an open subgroup.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.ProC
universe u
section RightQuotientSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
Lean source · statement
def openSubgroupRightCoset (H : OpenSubgroup F) (g : F) : OpenSubgroupRightQuotient H
theorem

openSubgroupRightCoset_eq_basepoint_iff_mem

L54 ↗
ReidemeisterSchreier.Profinite.openSubgroupRightCoset_eq_basepoint_iff_mem
Documentation

A right coset is the base coset exactly when its representative lies in the subgroup.

Source context 10 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.ProC
universe u
section RightQuotientSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
omit [IsTopologicalGroup F] in
Lean source · statement
theorem openSubgroupRightCoset_eq_basepoint_iff_mem
    {H : OpenSubgroup F} {g : F} :
    openSubgroupRightCoset H g = openSubgroupRightCoset H (1 : F) ↔
      g ∈ (H : Subgroup F)
theorem

openSubgroupRightCoset_smul

L65 ↗
ReidemeisterSchreier.Profinite.openSubgroupRightCoset_smul
Documentation

The open-subgroup right-coset action sends the coset of \(a\) by \(g\) to the coset of \(a g^{-1}\).

Source context 10 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.ProC
universe u
section RightQuotientSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
omit [IsTopologicalGroup F] in
Lean source · full declaration
theorem openSubgroupRightCoset_smul
    (H : OpenSubgroup F) (g a : F) :
    letI : MulAction F (OpenSubgroupRightQuotient H) :=
      _root_.ReidemeisterSchreier.rightCosetMulAction (H : Subgroup F)
    g • openSubgroupRightCoset H a = openSubgroupRightCoset H (a * g⁻¹) :=
  _root_.ReidemeisterSchreier.rightCosetMulAction_mk_smul (H := (H : Subgroup F)) g a
theorem

openSubgroupRightCoset_inv_smul

L77 ↗
ReidemeisterSchreier.Profinite.openSubgroupRightCoset_inv_smul
Documentation

The open-subgroup right-coset action sends the coset of \(a\) by \(g^{-1}\) to the coset of \(a g\).

Source context 10 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.ProC
universe u
section RightQuotientSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
omit [IsTopologicalGroup F] in
Lean source · full declaration
theorem openSubgroupRightCoset_inv_smul
    (H : OpenSubgroup F) (g a : F) :
    letI : MulAction F (OpenSubgroupRightQuotient H) :=
      _root_.ReidemeisterSchreier.rightCosetMulAction (H : Subgroup F)
    g⁻¹ • openSubgroupRightCoset H a = openSubgroupRightCoset H (a * g) :=
  _root_.ReidemeisterSchreier.rightCosetMulAction_inv_mk_smul (H := (H : Subgroup F)) g a
instance

finite_openSubgroupRightQuotient

L85 ↗
ReidemeisterSchreier.Profinite.finite_openSubgroupRightQuotient
Documentation

Right cosets of an open subgroup are finite because they are equivalent to the left quotient.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.ProC
universe u
section RightQuotientSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
Lean source · statement
instance finite_openSubgroupRightQuotient (H : OpenSubgroup F) [CompactSpace F] :
    Finite (OpenSubgroupRightQuotient H)
instance

fintype_openSubgroupRightQuotient

L92 ↗
ReidemeisterSchreier.Profinite.fintype_openSubgroupRightQuotient
Documentation

Right cosets of an open subgroup inherit a Fintype from compactness.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.ProC
universe u
section RightQuotientSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
Lean source · statement
instance fintype_openSubgroupRightQuotient (H : OpenSubgroup F) [CompactSpace F] :
    Fintype (OpenSubgroupRightQuotient H)
instance

discreteTopology_openSubgroupRightQuotient

L97 ↗
ReidemeisterSchreier.Profinite.discreteTopology_openSubgroupRightQuotient
Documentation

The quotient topology on right cosets of an open subgroup is discrete.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.ProC
universe u
section RightQuotientSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
Lean source · statement
instance discreteTopology_openSubgroupRightQuotient (H : OpenSubgroup F) :
    DiscreteTopology (OpenSubgroupRightQuotient H)
def

openSubgroupRightCosetSection

L133 ↗
ReidemeisterSchreier.Profinite.openSubgroupRightCosetSection
Documentation

A normalized section of the right-coset projection, sending the trivial coset to \(1\).

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.ProC
universe u
section RightQuotientSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
Lean source · statement
def openSubgroupRightCosetSection
    (H : OpenSubgroup F) : OpenSubgroupRightQuotient H → F
theorem

openSubgroupRightCosetSection_spec

L147 ↗
ReidemeisterSchreier.Profinite.openSubgroupRightCosetSection_spec
Documentation

The chosen section of the open-subgroup right quotient projects back to the given right coset.

Source context 10 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.ProC
universe u
section RightQuotientSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
omit [IsTopologicalGroup F] in
Lean source · statement
theorem openSubgroupRightCosetSection_spec
    (H : OpenSubgroup F) (q : OpenSubgroupRightQuotient H) :
    Quotient.mk'' (openSubgroupRightCosetSection (F := F) H q) = q
theorem

openSubgroupRightCosetSection_one

L161 ↗
ReidemeisterSchreier.Profinite.openSubgroupRightCosetSection_one
Documentation

The chosen section of the open-subgroup right quotient sends the identity coset to the identity representative.

Source context 10 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.ProC
universe u
section RightQuotientSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
omit [IsTopologicalGroup F] in
Lean source · statement
theorem openSubgroupRightCosetSection_one
    (H : OpenSubgroup F) :
    openSubgroupRightCosetSection (F := F) H (openSubgroupRightCoset H (1 : F)) = 1
theorem

continuous_openSubgroupRightCosetSection

L171 ↗
ReidemeisterSchreier.Profinite.continuous_openSubgroupRightCosetSection
Documentation

The normalized right-coset section is continuous because the right quotient is discrete. It is a continuity claim, checked through the topology generated by finite-stage projections.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.ProC
universe u
section RightQuotientSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
Lean source · statement
theorem continuous_openSubgroupRightCosetSection
    (H : OpenSubgroup F) :
    Continuous (openSubgroupRightCosetSection (F := F) H)

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