NYLL
Module

MinimalPower.lean

Nyll.ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.MinimalPower
3 declarations indexed from sourceView source ↗

Module documentation

Pointed bases controlled by a minimal generator power

If the first positive power of a distinguished generator entering an open subgroup is nontrivial, this module constructs a finite converging-set basis containing that power and refines the finite-rank Schreier basis theorem while retaining the distinguished basis element.

Imports1
Imported by1

Declarations

theorem

exists_compactPointedBasis_openSubgroup_of_minGeneratorPower

L34 ↗
ReidemeisterSchreier.Profinite.exists_compactPointedBasis_openSubgroup_of_minGeneratorPower
Documentation

This is the pointed profinite Reidemeister--Schreier theorem over a converging-set basis, with a prescribed minimal generator power landing in the 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
theorem exists_compactPointedBasis_openSubgroup_of_minGeneratorPower
    (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) (x : X) {N : ℕ}
    (hN : 0 < N)
    (hpow : (ι x) ^ N ∈ (H : Subgroup F))
    (hmin : ∀ m : ℕ, 0 < m → m < N → (ι x) ^ m ∉ (H : Subgroup F)) :
    ∃ κ : OpenSubgroupRightQuotient H × OnePoint X → ↥(H : Subgroup F),
      Continuous κ ∧
      (∀ q : OpenSubgroupRightQuotient H, κ (q, OnePoint.infty) = 1) ∧
      κ (openSubgroupRightCoset H (1 : F), OnePoint.infty) = 1 ∧
      (⟨(ι x) ^ N, hpow⟩ : ↥(H : Subgroup F)) ∈ Set.range κ ∧
      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
theorem

exists_finiteConvergingSetBasis_openSubgroup_of_minimalGeneratorPower

L150 ↗
ReidemeisterSchreier.Profinite.exists_finiteConvergingSetBasis_openSubgroup_of_minimalGeneratorPower
Documentation

Finite-rank pointed control over a converging-set free pro-\(C\) group: if \(x^N\) is the first positive power of a basis element landing in \(H\), and this power is nontrivial, the finite converging-set basis model for \(H\) can be chosen so that \(x^N\) lies in the basis image.

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_finiteConvergingSetBasis_openSubgroup_of_minimalGeneratorPower
    {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} [Finite 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) (x : X) {N : ℕ}
    (hN : 0 < N)
    (hpow : (ι x) ^ N ∈ (H : Subgroup F))
    (hpow_ne : (ι x) ^ N ≠ 1)
    (hmin : ∀ m : ℕ, 0 < m → m < N → (ι x) ^ m ∉ (H : Subgroup F)) :
    ∃ Fdata : EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (C := C),
      ∃ e : Fdata.carrier ≃ₜ* ↥(H : Subgroup F),
        (⟨(ι x) ^ N, hpow⟩ : ↥(H : Subgroup F)) ∈
          Set.range (e ∘ Fdata.inclusion) ∧
        Finite Fdata.basis
theorem

exists_basis_openSubgroup_of_extensionClosed_finiteRank_of_minimalGeneratorPower

L224 ↗
ReidemeisterSchreier.Profinite.exists_basis_openSubgroup_of_extensionClosed_finiteRank_of_minimalGeneratorPower
Documentation

Finite-rank pointed profinite Reidemeister--Schreier theorem: if \(x^N\) is the first positive power of the chosen ambient basis element landing in \(H\), and this power is nontrivial, then one can choose a finite-rank basis model of \(H\) whose basis image contains \(x^N\).

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_basis_openSubgroup_of_extensionClosed_finiteRank_of_minimalGeneratorPower
    (C : ProCGroups.FiniteGroupClass.{u})
    (hVar : ProCGroups.FiniteGroupClass.Variety C)
    (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
    (hExt : ProCGroups.FiniteGroupClass.ExtensionClosed C)
    (hcyc :
      ∃ (A : Type u) (_ : Group A) (_ : Finite A),
        C A ∧ IsCyclic A ∧ Nontrivial A)
    {X : Type u} [Finite 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) (x : X) {N : ℕ}
    (hN : 0 < N)
    (hpow : (ι x) ^ N ∈ (H : Subgroup F))
    (hpow_ne : (ι x) ^ N ≠ 1)
    (hmin : ∀ m : ℕ, 0 < m → m < N → (ι x) ^ m ∉ (H : Subgroup F)) :
    ∃ Fdata : EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (C := C),
      ∃ e : Fdata.carrier ≃ₜ* ↥(H : Subgroup F),
        (⟨(ι x) ^ N, hpow⟩ : ↥(H : Subgroup F)) ∈
          Set.range (e ∘ Fdata.inclusion) ∧
        Cardinal.mk Fdata.basis =
          (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H :
              Subgroup F))) :
            Cardinal)

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