Module

BasisTheorems.lean

Nyll.ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.BasisTheorems

8 declarations indexed from sourceView source ↗

Module documentation

From exact Schreier generators to free pro-\(C\) bases

This module turns the exact right-Schreier generation theorem into completion and basis statements. It isolates finite-quotient lifting, compares dense abstract free groups with their pro-\(C\) completions, and constructs compact pointed and converging-set bases for open subgroups.

Imports3

Imported by2

def

DenseAbstractSchreierFiniteQuotientLiftProperty

L35 ↗

ReidemeisterSchreier.Profinite.DenseAbstractSchreierFiniteQuotientLiftProperty

Documentation

Finite-discrete quotient lift property for a dense abstract Schreier model of an open subgroup.

Source context 7 commands

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

open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.FreeProC
open ProCGroups.ProC
universe u

Lean source · statement

def DenseAbstractSchreierFiniteQuotientLiftProperty
    (C : ProCGroups.FiniteGroupClass.{u})
    {F : Type u} [Group F] [TopologicalSpace F]
    (H : OpenSubgroup F)
    {Y : Type u}
    (φY : FreeGroup Y →* ↥(H : Subgroup F)) : Prop

theorem

denseAbstractSchreierFiniteQuotientLiftProperty_of_equiv

L49 ↗

ReidemeisterSchreier.Profinite.denseAbstractSchreierFiniteQuotientLiftProperty_of_equiv

Documentation

Transport the finite-quotient lift property across an abstract free-group equivalence.

Source context 7 commands

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

open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.FreeProC
open ProCGroups.ProC
universe u

Lean source · statement

theorem denseAbstractSchreierFiniteQuotientLiftProperty_of_equiv
    (C : ProCGroups.FiniteGroupClass.{u})
    {F : Type u} [Group F] [TopologicalSpace F]
    (H : OpenSubgroup F)
    {L : Type u} [Group L]
    {Y : Type u}
    (eY : FreeGroup Y ≃* L)
    (ψ : L →* ↥(H : Subgroup F))
    (hψfinite :
      ∀ {Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
        [Finite Q] [DiscreteTopology Q],
        C Q →
        ∀ χL : L →* Q,
          ∃! φbar : ↥(H : Subgroup F) →* Q,
            Continuous φbar ∧ φbar.comp ψ = χL) :
    DenseAbstractSchreierFiniteQuotientLiftProperty
      (C := C) H (ψ.comp eY.toMonoidHom)

theorem

isProCCompletion_denseAbstractSchreier_of_finiteQuotientLifts

L105 ↗

ReidemeisterSchreier.Profinite.isProCCompletion_denseAbstractSchreier_of_finiteQuotientLifts

Documentation

A dense abstract Schreier model with the finite-discrete quotient lift property is the pro-\(C\) completion of that abstract free group.

Source context 7 commands

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

open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.FreeProC
open ProCGroups.ProC
universe u

Lean source · statement

theorem isProCCompletion_denseAbstractSchreier_of_finiteQuotientLifts
    (C : ProCGroups.FiniteGroupClass.{u})
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
    (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
    {X : Type u}
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
      [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    {ι : X → F}
    (hF : IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) X F ι)
    (H : OpenSubgroup F)
    {Y : Type u}
    [TopologicalSpace (FreeGroup Y)] [IsTopologicalGroup (FreeGroup Y)]
    {φY : FreeGroup Y →ₜ* ↥(H : Subgroup F)}
    (hφYdense : DenseRange φY)
    (hfinite :
      DenseAbstractSchreierFiniteQuotientLiftProperty (C := C) H φY.toMonoidHom) :
    ProCGroups.Completion.IsProCCompletion
      (C)
      (FreeGroup Y) ↥(H : Subgroup F) φY

theorem

subgroup_le_topologicalClosure_of_topologicallyGenerates_local

L153 ↗

ReidemeisterSchreier.Profinite.subgroup_le_topologicalClosure_of_topologicallyGenerates_local

Documentation

A topologically generating subset of an open subgroup generates a dense subgroup after including it into the ambient group.

Source context 7 commands

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

open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.FreeProC
open ProCGroups.ProC
universe u

Lean source · statement

theorem subgroup_le_topologicalClosure_of_topologicallyGenerates_local
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (H : OpenSubgroup G)
    {S : Set ↥(H : Subgroup G)}
    (hS : Generation.TopologicallyGenerates (G := ↥(H : Subgroup G)) S) :
    (H : Subgroup G) ≤
      (Subgroup.closure (((↑) : ↥(H : Subgroup G) → G) '' S)).topologicalClosure

theorem

topologicallyFinitelyGenerated_of_openSubgroup_local

L186 ↗

ReidemeisterSchreier.Profinite.topologicallyFinitelyGenerated_of_openSubgroup_local

Documentation

If an open subgroup is topologically finitely generated, then so is the ambient compact group.

Source context 7 commands

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

open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.FreeProC
open ProCGroups.ProC
universe u

Lean source · statement

theorem topologicallyFinitelyGenerated_of_openSubgroup_local
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G]
    (H : OpenSubgroup G)
    (hH : ProCGroups.FiniteGeneration.TopologicallyFinitelyGenerated ↥(H : Subgroup G)) :
    ProCGroups.FiniteGeneration.TopologicallyFinitelyGenerated G

theorem

isProCCompletion_freeGroupLift_of_finiteBasis

L258 ↗

ReidemeisterSchreier.Profinite.isProCCompletion_freeGroupLift_of_finiteBasis

Documentation

A finite converging-set free pro-\(C\) basis realizes the pro-\(C\) completion of the abstract free group on the same basis.

Source context 7 commands

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

open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.FreeProC
open ProCGroups.ProC
universe u

Lean source · statement

theorem isProCCompletion_freeGroupLift_of_finiteBasis
    {C : ProCGroups.FiniteGroupClass.{u}}
    (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
    (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
    {X : Type u} [Finite X]
    [TopologicalSpace (FreeGroup X)] [IsTopologicalGroup (FreeGroup X)]
    [DiscreteTopology (FreeGroup X)]
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
      [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    {ι : X → F}
    (hF : IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) X F ι) :
    ProCGroups.Completion.IsProCCompletion
      (C)
      (FreeGroup X) F
      { toMonoidHom := FreeGroup.lift ι
        continuous_toFun := continuous_of_discreteTopology }

theorem

isProCCompletion_freeGroupLift_of_exactGeneratingFamily_of_completion

L339 ↗

ReidemeisterSchreier.Profinite.isProCCompletion_freeGroupLift_of_exactGeneratingFamily_of_completion

Documentation

If a finite generating family has the same cardinality as an abstract free model whose completion is the target, then that family realizes the same pro-C completion. The finite index type is arbitrary in the ambient universe.

Source context 7 commands

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

open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.FreeProC
open ProCGroups.ProC
universe u

Lean source · statement

theorem isProCCompletion_freeGroupLift_of_exactGeneratingFamily_of_completion
    {C : ProCGroups.FiniteGroupClass.{u}}
    (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
    (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
    (hQuot : ProCGroups.FiniteGroupClass.QuotientClosed C)
    (hcyc :
      ∃ (A : Type u) (_ : Group A) (_ : Finite A),
        C A ∧ IsCyclic A ∧ Nontrivial A)
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
      [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
    {Y Z : Type u} [Finite Z]
    [TopologicalSpace (FreeGroup Y)] [IsTopologicalGroup (FreeGroup Y)]
    [DiscreteTopology (FreeGroup Y)]
    [TopologicalSpace (FreeGroup Z)] [IsTopologicalGroup (FreeGroup Z)]
    [DiscreteTopology (FreeGroup Z)]
    (hYZcard : Nat.card Y = Nat.card Z)
    {φY : FreeGroup Y →ₜ* H}
    (hCompY :
      ProCGroups.Completion.IsProCCompletion
        (C) (FreeGroup Y) H φY)
    {κ : Z → H}
    (hκ : Generation.GeneratesAndConvergesToOneAlongOpenSubgroups (G := H) (Set.range κ)) :
    ProCGroups.Completion.IsProCCompletion
      (C)
      (FreeGroup Z) H
      { toMonoidHom := FreeGroup.lift κ
        continuous_toFun := continuous_of_discreteTopology }

theorem

exists_compactPointedBasis_openSubgroup_of_freeProCOnConvergingSet

L443 ↗

ReidemeisterSchreier.Profinite.exists_compactPointedBasis_openSubgroup_of_freeProCOnConvergingSet

Documentation

Compact pointed basis bridge: adjoining the point at infinity to a discrete converging basis, the open subgroup inherits a compact pointed right Schreier basis.

Source context 7 commands

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

open scoped Topology Pointwise
namespace ReidemeisterSchreier
namespace Profinite
open ProCGroups
open ProCGroups.FreeProC
open ProCGroups.ProC
universe u

Lean source · statement

theorem exists_compactPointedBasis_openSubgroup_of_freeProCOnConvergingSet
    (C : ProCGroups.FiniteGroupClass.{u})
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
    (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
    (hExt : ProCGroups.FiniteGroupClass.ExtensionClosed C)
    {X : Type u}
    [TopologicalSpace X] [DiscreteTopology X]
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
      [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    {ι : X → F}
    (hF : IsEpimorphicallyFreeProCGroupOnConvergingSet
      (C := C) X F ι)
    (H : OpenSubgroup F) :
    ∃ κ : OpenSubgroupRightQuotient H × OnePoint X → ↥(H : Subgroup F),
      Continuous κ ∧
      (∀ q : OpenSubgroupRightQuotient H, κ (q, OnePoint.infty) = 1) ∧
      κ (openSubgroupRightCoset H (1 : F), OnePoint.infty) = 1 ∧
      IsCompact (Set.range κ) ∧
      IsClosed (Set.range κ) ∧
      IsEpimorphicallyPointedFreeProCGroupOn
        (C := C)
        (Set.range κ)
        ⟨κ (openSubgroupRightCoset H (1 : F), OnePoint.infty),
          ⟨(openSubgroupRightCoset H (1 : F), OnePoint.infty), rfl⟩⟩
        ↥(H : Subgroup F) Subtype.val

Module documentation

From exact Schreier generators to free pro-\(C\) bases

Declarations