Module

SchreierTransversals.lean

Nyll.ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.SchreierTransversals

43 declarations indexed from sourceView source ↗

Module documentation

Schreier sections and oriented cocycles

The source of truth is SchreierCocycleData: it stores a left/right orientation, a section map, the next-coset operation, and the proof that the resulting cocycle lands in the open subgroup. ActualSchreierSection and ActualRightSchreierSection add equivalences with the genuine quotient and the projection/next-coset coherence laws. FiniteSchreierCocycleData carries the finiteness evidence used by Nat.card.

The concrete left- and right-coset constructions below feed this common API. Continuity, closure, generation, and cardinality are proved once for the oriented data rather than repeated as chosen-left/chosen-right wrapper families.

Imports3

Imported by2

abbrev

openSubgroupLeftSchreierSection

L45 ↗

ReidemeisterSchreier.Profinite.openSubgroupLeftSchreierSection

Documentation

The normalized continuous section of the left quotient by an open subgroup.

Source context 11 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section LeftQuotientSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]

Lean source · statement

abbrev openSubgroupLeftSchreierSection (H : OpenSubgroup F) :
    F ⧸ (H : Subgroup F) → F

theorem

openSubgroupLeftSchreierSection_rightInverse

L53 ↗

ReidemeisterSchreier.Profinite.openSubgroupLeftSchreierSection_rightInverse

Documentation

The normalized section of the left quotient is a right inverse to the quotient projection.

Source context 12 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section LeftQuotientSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
omit [IsTopologicalGroup F] in

Lean source · statement

theorem openSubgroupLeftSchreierSection_rightInverse (H : OpenSubgroup F) :
    Function.RightInverse (openSubgroupLeftSchreierSection (F := F) H)
      (QuotientGroup.mk (s := (H : Subgroup F)))

theorem

continuous_openSubgroupLeftSchreierSection

L61 ↗

ReidemeisterSchreier.Profinite.continuous_openSubgroupLeftSchreierSection

Documentation

The corresponding Schreier section is continuous.

Source context 11 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section LeftQuotientSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]

Lean source · statement

theorem continuous_openSubgroupLeftSchreierSection (H : OpenSubgroup F) :
    Continuous (openSubgroupLeftSchreierSection (F := F) H)

theorem

openSubgroupLeftSchreierSection_mk

L69 ↗

ReidemeisterSchreier.Profinite.openSubgroupLeftSchreierSection_mk

Documentation

The Schreier generator component of the corresponding rewriting map.

Source context 12 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section LeftQuotientSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
omit [IsTopologicalGroup F] in

Lean source · statement

theorem openSubgroupLeftSchreierSection_mk
    (H : OpenSubgroup F) (q : F ⧸ (H : Subgroup F)) :
    QuotientGroup.mk (s := (H : Subgroup F))
        (openSubgroupLeftSchreierSection (F := F) H q) = q

theorem

openSubgroupLeftSchreierSection_one

L77 ↗

ReidemeisterSchreier.Profinite.openSubgroupLeftSchreierSection_one

Documentation

The normalized left-quotient section sends the identity coset to the identity.

Source context 12 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section LeftQuotientSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
omit [IsTopologicalGroup F] in

Lean source · statement

theorem openSubgroupLeftSchreierSection_one
    (H : OpenSubgroup F) :
    openSubgroupLeftSchreierSection (F := F) H
        (QuotientGroup.mk (s := (H : Subgroup F)) (1 : F)) = 1

inductive

SchreierOrientation

L92 ↗

ReidemeisterSchreier.Profinite.SchreierOrientation

Documentation

The two cocycle orientations used by left- and right-coset Schreier generators.

Source context 13 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section AbstractSchreierSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {X : Type v}
variable (H : OpenSubgroup F)

Lean source · full declaration

inductive SchreierOrientation where
  /-- The left-oriented cocycle places the inverse of the next representative first. -/
  | left
  /-- The right-oriented cocycle places the inverse of the next representative last. -/
  | right
deriving DecidableEq

def

cocycle

L102 ↗

ReidemeisterSchreier.Profinite.SchreierOrientation.cocycle

Documentation

The oriented Schreier cocycle associated to a section and a next-coset operation.

Source context 14 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section AbstractSchreierSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {X : Type v}
variable (H : OpenSubgroup F)
namespace SchreierOrientation

Lean source · statement

def cocycle {Q : Type u} (o : SchreierOrientation)
    (sec : Q → F) (next : Q → X → Q) (ι : X → F) (q : Q) (x : X) : F

structure

SchreierCocycleData

L115 ↗

ReidemeisterSchreier.Profinite.SchreierCocycleData

Documentation

A section-level Schreier generator package. It abstracts over the quotient type, the left/right cocycle orientation, and the next-coset operation, so the common generator-set, continuity, closure, and cardinality formulation can be formulated once.

Source context 13 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section AbstractSchreierSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {X : Type v}
variable (H : OpenSubgroup F)

Lean source · full declaration

structure SchreierCocycleData where
  /-- The abstract type indexing the chosen coset representatives. -/
  Q : Type u
  /-- Whether the associated Schreier cocycle uses the left- or right-coset formula. -/
  orientation : SchreierOrientation
  /-- The representative in \(F\) assigned to each abstract quotient index. -/
  sectionMap : Q → F
  /-- The quotient index reached after multiplying a representative by a chosen generator. -/
  next : (X → F) → Q → X → Q
  /-- Every oriented cocycle value belongs to the open subgroup \(H\). -/
  cocycle_mem :
    ∀ (ι : X → F) (q : Q) (x : X),
      orientation.cocycle sectionMap (next ι) ι q x ∈ (H : Subgroup F)

structure

ActualSchreierSection

L135 ↗

ReidemeisterSchreier.Profinite.ActualSchreierSection

Documentation

Genuine left-quotient Schreier section data.

The equivalence identifies the abstract cocycle index with the actual quotient F ⧸ H; the remaining fields state that both the representative and the next-coset operation project to that quotient. Thus no arbitrary raw map can masquerade as a quotient projection.

Source context 13 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section AbstractSchreierSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {X : Type v}
variable (H : OpenSubgroup F)

Lean source · full declaration

structure ActualSchreierSection where
  /-- The abstract cocycle and section data. -/
  cocycleData : SchreierCocycleData (F := F) (X := X) H
  /-- Identification of the abstract index type with the left quotient \(F/H\). -/
  quotientEquiv : cocycleData.Q ≃ F ⧸ (H : Subgroup F)
  /-- Each chosen representative projects to its corresponding quotient index. -/
  section_projects :
    ∀ q : cocycleData.Q,
      QuotientGroup.mk (s := (H : Subgroup F)) (cocycleData.sectionMap q) =
        quotientEquiv q
  /-- The next-index operation projects the representative multiplied by the chosen generator. -/
  next_projects :
    ∀ (ι : X → F) (q : cocycleData.Q) (x : X),
      quotientEquiv (cocycleData.next ι q x) =
        QuotientGroup.mk (s := (H : Subgroup F))
          (cocycleData.sectionMap q * ι x)

structure

ActualRightSchreierSection

L156 ↗

ReidemeisterSchreier.Profinite.ActualRightSchreierSection

Documentation

Genuine right-quotient Schreier section data.

This is the right-coset counterpart of ActualSchreierSection; its index type is explicitly identified with OpenSubgroupRightQuotient H.

Source context 13 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section AbstractSchreierSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {X : Type v}
variable (H : OpenSubgroup F)

Lean source · full declaration

structure ActualRightSchreierSection where
  /-- The abstract cocycle and section data. -/
  cocycleData : SchreierCocycleData (F := F) (X := X) H
  /-- Identification of the abstract index type with the right quotient by \(H\). -/
  quotientEquiv : cocycleData.Q ≃ OpenSubgroupRightQuotient H
  /-- Each chosen representative maps to its corresponding right-quotient index. -/
  section_projects :
    ∀ q : cocycleData.Q,
      (Quotient.mk'' (cocycleData.sectionMap q) :
        OpenSubgroupRightQuotient H) = quotientEquiv q
  /-- The next-index operation maps the representative multiplied by the chosen generator. -/
  next_projects :
    ∀ (ι : X → F) (q : cocycleData.Q) (x : X),
      quotientEquiv (cocycleData.next ι q x) =
        (Quotient.mk'' (cocycleData.sectionMap q * ι x) :
          OpenSubgroupRightQuotient H)

structure

FiniteSchreierCocycleData

L176 ↗

ReidemeisterSchreier.Profinite.FiniteSchreierCocycleData

Documentation

A cocycle package together with the finiteness data required by its Nat.card estimates. This prevents a finite-index formula from silently using Nat.card = 0 on an infinite quotient.

Source context 13 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section AbstractSchreierSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {X : Type v}
variable (H : OpenSubgroup F)

Lean source · full declaration

structure FiniteSchreierCocycleData where
  /-- The underlying abstract Schreier cocycle package. -/
  cocycleData : SchreierCocycleData (F := F) (X := X) H
  /-- Finiteness of the generator-index type. -/
  finiteGeneratorIndex : Finite X
  /-- Finiteness of the abstract quotient-index type. -/
  finiteQuotient : Finite cocycleData.Q

def

generator

L189 ↗

ReidemeisterSchreier.Profinite.SchreierCocycleData.generator

Documentation

The subgroup-valued generator attached to an abstract Schreier section.

Source context 15 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section AbstractSchreierSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {X : Type v}
variable (H : OpenSubgroup F)
namespace SchreierCocycleData
variable {H}

Lean source · statement

def generator (S : SchreierCocycleData (F := F) (X := X) H)
    (ι : X → F) (q : S.Q) (x : X) : ↥(H : Subgroup F)

theorem

generator_coe

L196 ↗

ReidemeisterSchreier.Profinite.SchreierCocycleData.generator_coe

Documentation

Forgetting the subgroup proof from a Schreier generator yields its defining cocycle value.

Source context 16 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section AbstractSchreierSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {X : Type v}
variable (H : OpenSubgroup F)
namespace SchreierCocycleData
variable {H}
omit [IsTopologicalGroup F] in

Lean source · statement

theorem generator_coe (S : SchreierCocycleData (F := F) (X := X) H)
    (ι : X → F) (q : S.Q) (x : X) :
    ((S.generator ι q x : ↥(H : Subgroup F)) : F) =
      S.orientation.cocycle S.sectionMap (S.next ι) ι q x

def

generatorSet

L203 ↗

ReidemeisterSchreier.Profinite.SchreierCocycleData.generatorSet

Documentation

Nontrivial generator values of an abstract Schreier section.

Source context 15 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section AbstractSchreierSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {X : Type v}
variable (H : OpenSubgroup F)
namespace SchreierCocycleData
variable {H}

Lean source · statement

def generatorSet (S : SchreierCocycleData (F := F) (X := X) H)
    (ι : X → F) : Set ↥(H : Subgroup F)

def

NontrivialPairs

L211 ↗

ReidemeisterSchreier.Profinite.SchreierCocycleData.NontrivialPairs

Documentation

This type records the nontrivial Schreier pairs whose cocycle values form the abstract Schreier generator set.

Source context 15 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section AbstractSchreierSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {X : Type v}
variable (H : OpenSubgroup F)
namespace SchreierCocycleData
variable {H}

Lean source · statement

def NontrivialPairs (S : SchreierCocycleData (F := F) (X := X) H)
    (ι : X → F) : Type (max u v)

instance

finite_nontrivialPairs

L220 ↗

ReidemeisterSchreier.Profinite.SchreierCocycleData.finite_nontrivialPairs

Documentation

The abstract Schreier generator or next-coset formula is obtained by evaluating the chosen section cocycle.

Source context 16 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section AbstractSchreierSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {X : Type v}
variable (H : OpenSubgroup F)
namespace SchreierCocycleData
variable {H}
omit [IsTopologicalGroup F] in

Lean source · statement

instance finite_nontrivialPairs
    (S : SchreierCocycleData (F := F) (X := X) H) (ι : X → F)
    [Finite X] [Finite S.Q] :
    Finite (S.NontrivialPairs ι)

def

nontrivialPairsToGeneratorSet

L230 ↗

ReidemeisterSchreier.Profinite.SchreierCocycleData.nontrivialPairsToGeneratorSet

Documentation

The tautological map from nontrivial abstract Schreier pairs to the generator value set.

Source context 16 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section AbstractSchreierSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {X : Type v}
variable (H : OpenSubgroup F)
namespace SchreierCocycleData
variable {H}
omit [IsTopologicalGroup F] in

Lean source · statement

def nontrivialPairsToGeneratorSet
    (S : SchreierCocycleData (F := F) (X := X) H) (ι : X → F) :
    S.NontrivialPairs ι → ↥(S.generatorSet ι)

theorem

surjective_nontrivialPairsToGeneratorSet

L240 ↗

ReidemeisterSchreier.Profinite.SchreierCocycleData.surjective_nontrivialPairsToGeneratorSet

Documentation

The map from nontrivial abstract Schreier pairs onto the abstract Schreier generator set is surjective.

Source context 16 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section AbstractSchreierSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {X : Type v}
variable (H : OpenSubgroup F)
namespace SchreierCocycleData
variable {H}
omit [IsTopologicalGroup F] in

Lean source · statement

theorem surjective_nontrivialPairsToGeneratorSet
    (S : SchreierCocycleData (F := F) (X := X) H) (ι : X → F) :
    Function.Surjective (S.nontrivialPairsToGeneratorSet ι)

theorem

natCard_generatorSet_le_nontrivialPairs

L255 ↗

ReidemeisterSchreier.Profinite.SchreierCocycleData.natCard_generatorSet_le_nontrivialPairs

Documentation

Surjectivity of the map from nontrivial Schreier pairs bounds the cardinality of the abstract Schreier generator set by the number of nontrivial pairs.

Source context 16 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section AbstractSchreierSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {X : Type v}
variable (H : OpenSubgroup F)
namespace SchreierCocycleData
variable {H}
omit [IsTopologicalGroup F] in

Lean source · statement

theorem natCard_generatorSet_le_nontrivialPairs
    (S : SchreierCocycleData (F := F) (X := X) H) (ι : X → F)
    [Finite X] [Finite S.Q] :
    Nat.card (S.generatorSet ι) ≤ Nat.card (S.NontrivialPairs ι)

theorem

natCard_nontrivialPairs_le

L267 ↗

ReidemeisterSchreier.Profinite.SchreierCocycleData.natCard_nontrivialPairs_le

Documentation

The number of nontrivial abstract Schreier pairs is bounded by the corresponding finite coset-generator product.

Source context 16 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section AbstractSchreierSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {X : Type v}
variable (H : OpenSubgroup F)
namespace SchreierCocycleData
variable {H}
omit [IsTopologicalGroup F] in

Lean source · statement

theorem natCard_nontrivialPairs_le
    (S : SchreierCocycleData (F := F) (X := X) H) (ι : X → F)
    [Finite X] [Finite S.Q] :
    Nat.card (S.NontrivialPairs ι) ≤ Nat.card S.Q * Nat.card X

theorem

natCard_generatorSet_le

L280 ↗

ReidemeisterSchreier.Profinite.SchreierCocycleData.natCard_generatorSet_le

Documentation

The Schreier generator set has cardinality at most the number of quotient cosets times the number of original generators.

Source context 16 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section AbstractSchreierSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {X : Type v}
variable (H : OpenSubgroup F)
namespace SchreierCocycleData
variable {H}
omit [IsTopologicalGroup F] in

Lean source · statement

theorem natCard_generatorSet_le
    (S : SchreierCocycleData (F := F) (X := X) H) (ι : X → F)
    [Finite X] [Finite S.Q] :
    Nat.card (S.generatorSet ι) ≤ Nat.card S.Q * Nat.card X

theorem

subgroupClosure_generatorSet_eq_closure_range

L291 ↗

ReidemeisterSchreier.Profinite.SchreierCocycleData.subgroupClosure_generatorSet_eq_closure_range

Documentation

The subgroup closure of the abstract Schreier generator set is the closure of the corresponding generator-map range.

Source context 16 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section AbstractSchreierSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {X : Type v}
variable (H : OpenSubgroup F)
namespace SchreierCocycleData
variable {H}
omit [IsTopologicalGroup F] in

Lean source · full declaration

theorem subgroupClosure_generatorSet_eq_closure_range
    (S : SchreierCocycleData (F := F) (X := X) H) (ι : X → F) :
    Subgroup.closure (S.generatorSet ι) =
      Subgroup.closure (Set.range fun p : S.Q × X => S.generator ι p.1 p.2) := by
  simpa [generatorSet] using
    (ProCGroups.Generation.closure_nontrivial_range_eq_closure_range
      (G := ↥(H : Subgroup F))
      (fun p : S.Q × X => S.generator ι p.1 p.2))

theorem

topologicallyGenerates_generatorSet_iff

L304 ↗

ReidemeisterSchreier.Profinite.SchreierCocycleData.topologicallyGenerates_generatorSet_iff

Documentation

The Schreier generator family topologically generates precisely when the corresponding subgroup-generation condition holds.

Source context 15 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section AbstractSchreierSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {X : Type v}
variable (H : OpenSubgroup F)
namespace SchreierCocycleData
variable {H}

Lean source · full declaration

theorem topologicallyGenerates_generatorSet_iff
    {S : SchreierCocycleData (F := F) (X := X) H} {ι : X → F} :
    ProCGroups.Generation.TopologicallyGenerates (G := ↥(H : Subgroup F))
        (S.generatorSet ι) ↔
      ProCGroups.Generation.TopologicallyGenerates (G := ↥(H : Subgroup F))
        (Set.range fun p : S.Q × X => S.generator ι p.1 p.2) := by
  rw [ProCGroups.Generation.topologicallyGenerates_iff_dense,
    ProCGroups.Generation.topologicallyGenerates_iff_dense,
    S.subgroupClosure_generatorSet_eq_closure_range ι]

theorem

generator_eq_one_iff_left

L319 ↗

ReidemeisterSchreier.Profinite.SchreierCocycleData.generator_eq_one_iff_left

Documentation

It characterizes exactly when generator identity with the unit equivalence left is equal to the unit for the chosen Schreier transversal and induced coset representatives.

Source context 16 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section AbstractSchreierSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {X : Type v}
variable (H : OpenSubgroup F)
namespace SchreierCocycleData
variable {H}
omit [IsTopologicalGroup F] in

Lean source · statement

theorem generator_eq_one_iff_left
    {S : SchreierCocycleData (F := F) (X := X) H}
    (hleft : S.orientation = SchreierOrientation.left)
    {ι : X → F} {q : S.Q} {x : X} :
    S.generator ι q x = 1 ↔ S.sectionMap (S.next ι q x) = S.sectionMap q * ι x

theorem

generator_eq_one_iff_right

L340 ↗

ReidemeisterSchreier.Profinite.SchreierCocycleData.generator_eq_one_iff_right

Documentation

The right Schreier generator is trivial exactly in the corresponding unit-representative case.

Source context 16 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section AbstractSchreierSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {X : Type v}
variable (H : OpenSubgroup F)
namespace SchreierCocycleData
variable {H}
omit [IsTopologicalGroup F] in

Lean source · statement

theorem generator_eq_one_iff_right
    {S : SchreierCocycleData (F := F) (X := X) H}
    (hright : S.orientation = SchreierOrientation.right)
    {ι : X → F} {q : S.Q} {x : X} :
    S.generator ι q x = 1 ↔ S.sectionMap (S.next ι q x) = S.sectionMap q * ι x

theorem

generator_eq_of_section_next_eq_one

L362 ↗

ReidemeisterSchreier.Profinite.SchreierCocycleData.generator_eq_of_section_next_eq_one

Documentation

The rewritten Reidemeister--Schreier generator evaluates to the identity when the next section value is the basepoint.

Source context 16 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section AbstractSchreierSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {X : Type v}
variable (H : OpenSubgroup F)
namespace SchreierCocycleData
variable {H}
omit [IsTopologicalGroup F] in

Lean source · statement

theorem generator_eq_of_section_next_eq_one
    (S : SchreierCocycleData (F := F) (X := X) H)
    (ι : X → F) (q : S.Q) (x : X)
    (hnext : S.sectionMap (S.next ι q x) = 1)
    (hmem : S.sectionMap q * ι x ∈ (H : Subgroup F)) :
    S.generator ι q x = ⟨S.sectionMap q * ι x, hmem⟩

theorem

continuous_generator

L379 ↗

ReidemeisterSchreier.Profinite.SchreierCocycleData.continuous_generator

Documentation

The abstract Schreier section generator is the cocycle value determined by the chosen section and next coset.

Source context 15 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section AbstractSchreierSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {X : Type v}
variable (H : OpenSubgroup F)
namespace SchreierCocycleData
variable {H}

Lean source · full declaration

theorem continuous_generator
    (S : SchreierCocycleData (F := F) (X := X) H)
    [TopologicalSpace S.Q] [TopologicalSpace X]
    (ι : X → F)
    (hsection : Continuous S.sectionMap)
    (hnext : Continuous (fun p : S.Q × X => S.next ι p.1 p.2))
    (hι : Continuous ι) :
    Continuous (fun p : S.Q × X => S.generator ι p.1 p.2) := by
  refine Continuous.subtype_mk ?_ ?_
  cases hside : S.orientation with
  | left =>
      have hcont :
          Continuous (fun p : S.Q × X =>
            (S.sectionMap (S.next ι p.1 p.2))⁻¹ * (S.sectionMap p.1 * ι p.2)) :=
        ((hsection.comp hnext).inv).mul
          ((hsection.comp continuous_fst).mul (hι.comp continuous_snd))
      simpa [generator, SchreierOrientation.cocycle, hside, mul_assoc] using hcont
  | right =>
      have hcont :
          Continuous (fun p : S.Q × X =>
            (S.sectionMap p.1 * ι p.2) * (S.sectionMap (S.next ι p.1 p.2))⁻¹) :=
        ((hsection.comp continuous_fst).mul (hι.comp continuous_snd)).mul
          ((hsection.comp hnext).inv)
      simpa [generator, SchreierOrientation.cocycle, hside, mul_assoc] using hcont

theorem

natCard_generatorSet_le

L411 ↗

ReidemeisterSchreier.Profinite.FiniteSchreierCocycleData.natCard_generatorSet_le

Documentation

The generator-cardinality bound with all finiteness evidence carried by the data object rather than repeated as ambient typeclass assumptions.

Source context 15 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section AbstractSchreierSections
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable {X : Type v}
variable (H : OpenSubgroup F)
namespace FiniteSchreierCocycleData
omit [IsTopologicalGroup F] in

Lean source · statement

theorem natCard_generatorSet_le
    (S : FiniteSchreierCocycleData (F := F) (X := X) H) (ι : X → F) :
    Nat.card (S.cocycleData.generatorSet ι) ≤
      Nat.card S.cocycleData.Q * Nat.card X

def

leftSchreierNextCoset

L433 ↗

ReidemeisterSchreier.Profinite.leftSchreierNextCoset

Documentation

The next left coset obtained from a chosen representative and a generator.

Source context 16 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section LeftSchreierGenerators
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable (H : OpenSubgroup F)
variable {X : Type v}
variable (σ : F ⧸ (H : Subgroup F) → F)
variable (hσ : Function.RightInverse σ (QuotientGroup.mk (s := (H : Subgroup F))))
variable (ι : X → F)

Lean source · statement

def leftSchreierNextCoset (q : F ⧸ (H : Subgroup F)) (x : X) : F ⧸ (H : Subgroup F)

def

leftSchreierGenerator

L437 ↗

ReidemeisterSchreier.Profinite.leftSchreierGenerator

Documentation

Left-coset Schreier generator attached to a section of the quotient by an open subgroup.

Source context 16 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section LeftSchreierGenerators
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable (H : OpenSubgroup F)
variable {X : Type v}
variable (σ : F ⧸ (H : Subgroup F) → F)
variable (hσ : Function.RightInverse σ (QuotientGroup.mk (s := (H : Subgroup F))))
variable (ι : X → F)

Lean source · statement

def leftSchreierGenerator
    (hσ : Function.RightInverse σ (QuotientGroup.mk (s := (H : Subgroup F))))
    (q : F ⧸ (H : Subgroup F)) (x : X) :
    ↥(H : Subgroup F)

def

leftSchreierSection

L451 ↗

ReidemeisterSchreier.Profinite.leftSchreierSection

Documentation

The left-coset Schreier data as an instance of the abstract section formulation.

Source context 16 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section LeftSchreierGenerators
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable (H : OpenSubgroup F)
variable {X : Type v}
variable (σ : F ⧸ (H : Subgroup F) → F)
variable (hσ : Function.RightInverse σ (QuotientGroup.mk (s := (H : Subgroup F))))
variable (ι : X → F)

Lean source · full declaration

def leftSchreierSection :
    SchreierCocycleData (F := F) (X := X) H where
  Q := F ⧸ (H : Subgroup F)
  orientation := SchreierOrientation.left
  sectionMap := σ
  next := fun ι q x => leftSchreierNextCoset (F := F) H σ ι q x
  cocycle_mem := by
    intro ι q x
    exact (leftSchreierGenerator (F := F) (H := H) (σ := σ) (hσ := hσ) (ι := ι) q x).property

def

actualLeftSchreierSection

L463 ↗

ReidemeisterSchreier.Profinite.actualLeftSchreierSection

Documentation

The left quotient construction with its projection, section law, and next-coset coherence retained in the type.

Source context 16 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section LeftSchreierGenerators
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable (H : OpenSubgroup F)
variable {X : Type v}
variable (σ : F ⧸ (H : Subgroup F) → F)
variable (hσ : Function.RightInverse σ (QuotientGroup.mk (s := (H : Subgroup F))))
variable (ι : X → F)

Lean source · full declaration

def actualLeftSchreierSection :
    ActualSchreierSection (F := F) (X := X) H where
  cocycleData := leftSchreierSection (F := F) (H := H) (σ := σ) (hσ := hσ)
  quotientEquiv := Equiv.refl _
  section_projects := hσ
  next_projects := by
    intro ι q x
    rfl

theorem

leftSchreierSection_generator

L477 ↗

ReidemeisterSchreier.Profinite.leftSchreierSection_generator

Documentation

The left Schreier section generator is the cocycle value determined by the chosen section and next coset.

Source context 17 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section LeftSchreierGenerators
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable (H : OpenSubgroup F)
variable {X : Type v}
variable (σ : F ⧸ (H : Subgroup F) → F)
variable (hσ : Function.RightInverse σ (QuotientGroup.mk (s := (H : Subgroup F))))
variable (ι : X → F)
omit [IsTopologicalGroup F] in

Lean source · statement

theorem leftSchreierSection_generator
    (q : F ⧸ (H : Subgroup F)) (x : X) :
    (leftSchreierSection (F := F) (H := H) (σ := σ) (hσ := hσ) :
        SchreierCocycleData (F := F) (X := X) H).generator ι q x =
      leftSchreierGenerator (F := F) (H := H) (σ := σ) (hσ := hσ) (ι := ι) q x

instance

instMulActionOpenSubgroupRightQuotient

L497 ↗

ReidemeisterSchreier.Profinite.instMulActionOpenSubgroupRightQuotient

Documentation

The right quotient by an open subgroup carries the natural multiplication action.

Source context 16 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section RightSchreierGenerators
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable (H : OpenSubgroup F)
variable {X : Type v}
variable (τ : OpenSubgroupRightQuotient H → F)
variable (hτ : ∀ q, Quotient.mk'' (τ q) = q)
variable (ι : X → F)

Lean source · statement

instance instMulActionOpenSubgroupRightQuotient :
    MulAction F (OpenSubgroupRightQuotient H)

def

rightSchreierNextCoset

L507 ↗

ReidemeisterSchreier.Profinite.rightSchreierNextCoset

Documentation

The next right Schreier coset is obtained by acting on the current right coset by the inverse of the chosen generator image.

Source context 17 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section RightSchreierGenerators
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable (H : OpenSubgroup F)
variable {X : Type v}
variable (τ : OpenSubgroupRightQuotient H → F)
variable (hτ : ∀ q, Quotient.mk'' (τ q) = q)
variable (ι : X → F)
attribute [-instance] instMulActionOpenSubgroupRightQuotient

Lean source · statement

def rightSchreierNextCoset (q : OpenSubgroupRightQuotient H) (x : X) :
    OpenSubgroupRightQuotient H

def

rightSchreierGenerator

L515 ↗

ReidemeisterSchreier.Profinite.rightSchreierGenerator

Documentation

The Schreier generator formula records the element determined by the chosen representative associated to the chosen transversal and letter.

Source context 17 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section RightSchreierGenerators
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable (H : OpenSubgroup F)
variable {X : Type v}
variable (τ : OpenSubgroupRightQuotient H → F)
variable (hτ : ∀ q, Quotient.mk'' (τ q) = q)
variable (ι : X → F)
attribute [-instance] instMulActionOpenSubgroupRightQuotient

Lean source · statement

def rightSchreierGenerator (q : OpenSubgroupRightQuotient H) (x : X) :
    ↥(H : Subgroup F)

def

rightSchreierSection

L520 ↗

ReidemeisterSchreier.Profinite.rightSchreierSection

Documentation

The right-coset Schreier data as an instance of the abstract section formulation.

Source context 17 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section RightSchreierGenerators
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable (H : OpenSubgroup F)
variable {X : Type v}
variable (τ : OpenSubgroupRightQuotient H → F)
variable (hτ : ∀ q, Quotient.mk'' (τ q) = q)
variable (ι : X → F)
attribute [-instance] instMulActionOpenSubgroupRightQuotient

Lean source · full declaration

def rightSchreierSection :
    SchreierCocycleData (F := F) (X := X) H where
  Q := OpenSubgroupRightQuotient H
  orientation := SchreierOrientation.right
  sectionMap := τ
  next := fun ι q x => rightSchreierNextCoset (F := F) H ι q x
  cocycle_mem := by
    intro ι q x
    exact (rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) q x).property

def

actualRightSchreierSection

L532 ↗

ReidemeisterSchreier.Profinite.actualRightSchreierSection

Documentation

The right quotient construction with its projection, section law, and next-coset coherence retained in the type.

Source context 17 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section RightSchreierGenerators
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable (H : OpenSubgroup F)
variable {X : Type v}
variable (τ : OpenSubgroupRightQuotient H → F)
variable (hτ : ∀ q, Quotient.mk'' (τ q) = q)
variable (ι : X → F)
attribute [-instance] instMulActionOpenSubgroupRightQuotient

Lean source · full declaration

def actualRightSchreierSection :
    ActualRightSchreierSection (F := F) (X := X) H where
  cocycleData := rightSchreierSection (F := F) (H := H) (τ := τ) (hτ := hτ)
  quotientEquiv := Equiv.refl _
  section_projects := hτ
  next_projects := by
    change ∀ (ι : X → F) (q : OpenSubgroupRightQuotient H) (x : X),
      rightSchreierNextCoset (F := F) H ι q x = Quotient.mk'' (τ q * ι x)
    intro ι q x
    calc
      (ι x)⁻¹ • q =
          (ι x)⁻¹ • (Quotient.mk'' (τ q) : OpenSubgroupRightQuotient H) := by
            rw [hτ q]
      _ = Quotient.mk'' (τ q * ι x) := by
            rw [rightCosetMulAction_inv_mk_smul (H := (H : Subgroup F))]

theorem

rightSchreierSection_generator

L553 ↗

ReidemeisterSchreier.Profinite.rightSchreierSection_generator

Documentation

The right Schreier section generator is the cocycle value determined by the chosen section and next coset.

Source context 18 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section RightSchreierGenerators
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable (H : OpenSubgroup F)
variable {X : Type v}
variable (τ : OpenSubgroupRightQuotient H → F)
variable (hτ : ∀ q, Quotient.mk'' (τ q) = q)
variable (ι : X → F)
attribute [-instance] instMulActionOpenSubgroupRightQuotient
omit [IsTopologicalGroup F] in

Lean source · statement

theorem rightSchreierSection_generator
    (q : OpenSubgroupRightQuotient H) (x : X) :
    (rightSchreierSection (F := F) (H := H) (τ := τ) (hτ := hτ) :
        SchreierCocycleData (F := F) (X := X) H).generator ι q x =
      rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) q x

theorem

rightSchreierGenerator_eq_one

L563 ↗

ReidemeisterSchreier.Profinite.rightSchreierGenerator_eq_one

Documentation

The right Schreier generator evaluates to the identity in the target subgroup presentation.

Source context 18 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section RightSchreierGenerators
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable (H : OpenSubgroup F)
variable {X : Type v}
variable (τ : OpenSubgroupRightQuotient H → F)
variable (hτ : ∀ q, Quotient.mk'' (τ q) = q)
variable (ι : X → F)
attribute [-instance] instMulActionOpenSubgroupRightQuotient
omit [IsTopologicalGroup F] in

Lean source · statement

theorem rightSchreierGenerator_eq_one
    {q : OpenSubgroupRightQuotient H} {x : X}
    (hx : ι x = 1) :
    rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) q x = 1

theorem

continuous_rightSchreierNextCoset

L578 ↗

ReidemeisterSchreier.Profinite.continuous_rightSchreierNextCoset

Documentation

The corresponding Schreier next-coset map is continuous.

Source context 21 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section RightSchreierGenerators
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable (H : OpenSubgroup F)
variable {X : Type v}
variable (τ : OpenSubgroupRightQuotient H → F)
variable (hτ : ∀ q, Quotient.mk'' (τ q) = q)
variable (ι : X → F)
attribute [-instance] instMulActionOpenSubgroupRightQuotient
section Topological
variable [TopologicalSpace X]
variable [TopologicalSpace (OpenSubgroupRightQuotient H)]
variable [DiscreteTopology (OpenSubgroupRightQuotient H)]

Lean source · full declaration

theorem continuous_rightSchreierNextCoset
    (hιcont : Continuous ι) :
    Continuous (fun p : OpenSubgroupRightQuotient H × X =>
      rightSchreierNextCoset (F := F) H ι p.1 p.2) := by
  refine (continuous_prod_of_discrete_left).2 ?_
  intro q
  have hqcont :
      Continuous fun x : X => ((ι x)⁻¹ • q : OpenSubgroupRightQuotient H) := by
    rw [continuous_discrete_rng]
    intro q'
    classical
    let a : F := q.out
    let b : F := q'.out
    have hpre :
        (fun x : X => ((ι x)⁻¹ • q : OpenSubgroupRightQuotient H)) ⁻¹' ({q'} :
            Set (OpenSubgroupRightQuotient H)) =
          (fun x : X => b * (ι x)⁻¹ * a⁻¹) ⁻¹' ((H : Subgroup F) : Set F) := by
      ext x
      constructor
      · intro hx
        have hEq :
            (Quotient.mk'' (a * ι x) : OpenSubgroupRightQuotient H) = Quotient.mk'' b := by
          calc
            (Quotient.mk'' (a * ι x) : OpenSubgroupRightQuotient H)
                = (ι x)⁻¹ • (Quotient.mk'' a : OpenSubgroupRightQuotient H) := by
                    rw [rightCosetMulAction_inv_mk_smul (H := (H : Subgroup F)) (ι x) a]
            _ = (ι x)⁻¹ • q := by rw [Quotient.out_eq' q]
            _ = q' := hx
            _ = Quotient.mk'' b := (Quotient.out_eq' q').symm
        have hrel :
            QuotientGroup.rightRel (H : Subgroup F) (a * ι x) b := Quotient.eq''.mp hEq
        simpa [a, b, mul_inv_rev, mul_assoc] using (QuotientGroup.rightRel_apply.mp hrel)
      · intro hx
        change b * (ι x)⁻¹ * a⁻¹ ∈ (H : Subgroup F) at hx
        have hrel :
            QuotientGroup.rightRel (H : Subgroup F) (a * ι x) b := by
          rw [QuotientGroup.rightRel_apply]
          simpa only [a, b, mul_inv_rev, mul_assoc] using hx
        calc
          ((ι x)⁻¹ • q : OpenSubgroupRightQuotient H)
              = (ι x)⁻¹ • (Quotient.mk'' a : OpenSubgroupRightQuotient H) := by
                  rw [Quotient.out_eq' q]
          _ = Quotient.mk'' (a * ι x) := by
                rw [rightCosetMulAction_inv_mk_smul (H := (H : Subgroup F)) (ι x) a]
          _ = Quotient.mk'' b := Quotient.eq''.mpr hrel
          _ = q' := Quotient.out_eq' q'
    rw [show
      (fun x : X => ((ι x)⁻¹ • q : OpenSubgroupRightQuotient H)) ⁻¹' ({q'} :
          Set (OpenSubgroupRightQuotient H)) =
        (fun x : X => b * (ι x)⁻¹ * a⁻¹) ⁻¹' ((H : Subgroup F) : Set F) by
          simpa using hpre]
    exact H.isOpen'.preimage ((continuous_const.mul (hιcont.inv)).mul continuous_const)
  simpa [rightSchreierNextCoset] using hqcont

theorem

continuous_rightSchreierGenerator

L633 ↗

ReidemeisterSchreier.Profinite.continuous_rightSchreierGenerator

Documentation

The corresponding Schreier generator map is continuous.

Source context 21 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section RightSchreierGenerators
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable (H : OpenSubgroup F)
variable {X : Type v}
variable (τ : OpenSubgroupRightQuotient H → F)
variable (hτ : ∀ q, Quotient.mk'' (τ q) = q)
variable (ι : X → F)
attribute [-instance] instMulActionOpenSubgroupRightQuotient
section Topological
variable [TopologicalSpace X]
variable [TopologicalSpace (OpenSubgroupRightQuotient H)]
variable [DiscreteTopology (OpenSubgroupRightQuotient H)]

Lean source · full declaration

theorem continuous_rightSchreierGenerator
    (hτcont : Continuous τ) (hιcont : Continuous ι) :
    Continuous (fun p : OpenSubgroupRightQuotient H × X =>
      rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) p.1 p.2) := by
  let : TopologicalSpace
      (rightSchreierSection (F := F) (H := H) (τ := τ) (hτ := hτ) :
        SchreierCocycleData (F := F) (X := X) H).Q :=
    inferInstanceAs (TopologicalSpace (OpenSubgroupRightQuotient H))
  simpa using
    ((rightSchreierSection (F := F) (H := H) (τ := τ) (hτ := hτ) :
        SchreierCocycleData (F := F) (X := X) H).continuous_generator
      ι hτcont
      (continuous_rightSchreierNextCoset (F := F) (H := H) (ι := ι) hιcont)
      hιcont)

theorem

rightQuotientBasepointProjectionHom_rightSchreierGenerator

L656 ↗

ReidemeisterSchreier.Profinite.rightQuotientBasepointProjectionHom_rightSchreierGenerator

Documentation

The basepoint projection induced by a wreath-product homomorphism evaluates a right Schreier generator by the corresponding left coordinate.

Source context 18 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
open ProCGroups.FreeProC
open ProCGroups.WreathProducts
universe u v
section RightSchreierGenerators
variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
variable (H : OpenSubgroup F)
variable {X : Type v}
variable (τ : OpenSubgroupRightQuotient H → F)
variable (hτ : ∀ q, Quotient.mk'' (τ q) = q)
variable (ι : X → F)
attribute [-instance] instMulActionOpenSubgroupRightQuotient
omit [IsTopologicalGroup F] in

Lean source · statement

theorem rightQuotientBasepointProjectionHom_rightSchreierGenerator
    {A : Type*} [Group A]
    (ψ : F →* PermutationalWreathProduct A (OpenSubgroupRightQuotient H) F)
    (hψ :
      (SemidirectProduct.rightHom :
          PermutationalWreathProduct A (OpenSubgroupRightQuotient H) F →* F).comp ψ =
        MonoidHom.id F)
    (hτpure :
      ∀ q : OpenSubgroupRightQuotient H,
        wreathLeftCoordinate ψ
            (openSubgroupRightCoset H (1 : F)) (τ q) = 1)
    (q : OpenSubgroupRightQuotient H) (x : X) :
    rightQuotientBasepointProjectionHom (H : Subgroup F) ψ hψ
        (rightSchreierGenerator (F := F) (H := H) (τ := τ) (hτ := hτ) (ι := ι) q x) =
      wreathLeftCoordinate ψ q (ι x)

Module documentation

Schreier sections and oriented cocycles

Declarations