NYLL
Module

BasisFiniteRank.lean

Nyll.ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.BasisFiniteRank
5 declarations indexed from sourceView source ↗

Module documentation

Finite-rank bases of open subgroups

Starting from a finite converging-set basis, this module constructs a basis of the open subgroup and proves the classical finite Schreier rank formula. The padding lemma works on so that its index lives in the ambient universe; its public generating-family wrapper is indexed by , while the bundled free basis used in the final rank argument retains the lifted carrier.

Imports3
Imported by2

Declarations

theorem

exists_finiteIndexBasisCarrierAndMap_openSubgroup

L36 ↗
ReidemeisterSchreier.Profinite.exists_finiteIndexBasisCarrierAndMap_openSubgroup
Documentation

Finite converging-set basis data for an open subgroup of a free pro-\(C\) group on a finite converging set. The carrier is the open subgroup itself.

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_finiteIndexBasisCarrierAndMap_openSubgroup
    (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) :
    ∃ (B : Type u), Finite B ∧
      ∃ μ : B → ↥(H : Subgroup F),
        IsEpimorphicallyFreeProCGroupOnConvergingSet
          (C := C)
          B ↥(H : Subgroup F) μ
theorem

exists_exactGeneratingFamily_openSubgroup_of_finiteBasis_ulift

L82 ↗
ReidemeisterSchreier.Profinite.exists_exactGeneratingFamily_openSubgroup_of_finiteBasis_ulift
Documentation

An exact-size finite generating family for the open subgroup, indexed by the Schreier rank-transform cardinal. This is a generating family, not a basis: the padding step may repeat the distinguished padding element 1.

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_exactGeneratingFamily_openSubgroup_of_finiteBasis_ulift
    (C : ProCGroups.FiniteGroupClass.{u})
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
    (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
    (hQuot : ProCGroups.FiniteGroupClass.QuotientClosed 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) :
    ∃ κ :
        ULift.{u} (Fin (_root_.ReidemeisterSchreier.Schreier.rankTransform
          (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F))))) →
          ↥(H : Subgroup F),
      Generation.GeneratesAndConvergesToOneAlongOpenSubgroups
        (G := ↥(H : Subgroup F)) (Set.range κ)
theorem

exists_exactGeneratingFamily_openSubgroup_of_finiteBasis

L173 ↗
ReidemeisterSchreier.Profinite.exists_exactGeneratingFamily_openSubgroup_of_finiteBasis
Documentation

An exact-size finite generating family for the open subgroup on the canonical Fin index. The universe lift used to construct the padding embedding remains an implementation detail.

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_exactGeneratingFamily_openSubgroup_of_finiteBasis
    (C : ProCGroups.FiniteGroupClass.{u})
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed C)
    (hIso : ProCGroups.FiniteGroupClass.IsomClosed C)
    (hQuot : ProCGroups.FiniteGroupClass.QuotientClosed 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) :
    ∃ κ :
        Fin (_root_.ReidemeisterSchreier.Schreier.rankTransform
          (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F)))) →
          ↥(H : Subgroup F),
      Generation.GeneratesAndConvergesToOneAlongOpenSubgroups
        (G := ↥(H : Subgroup F)) (Set.range κ)
theorem

exists_basis_openSubgroup_of_extensionClosed_finiteRank

L217 ↗
ReidemeisterSchreier.Profinite.exists_basis_openSubgroup_of_extensionClosed_finiteRank
Documentation

Finite-rank extension-closed variety case using the Schreier rank-transform cardinality bound.

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
    (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) :
    ∃ Fdata : EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (C := C),
      Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F)) ∧
      Cardinal.mk Fdata.basis =
        (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H :
            Subgroup F))) :
          Cardinal)
theorem

exists_basis_openSubgroup_of_melnikovFormation_finiteRank_of_subgroupClosed

L403 ↗
ReidemeisterSchreier.Profinite.exists_basis_openSubgroup_of_melnikovFormation_finiteRank_of_subgroupClosed
Documentation

Finite-rank Melnikov-formation variant with explicit subgroup closure, using the Schreier rank-transform cardinality bound.

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_melnikovFormation_finiteRank_of_subgroupClosed
    (C : ProCGroups.FiniteGroupClass.{u})
    (hC : ProCGroups.FiniteGroupClass.MelnikovFormation C)
    (hSub : ProCGroups.FiniteGroupClass.SubgroupClosed 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) :
    ∃ Fdata : EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u}
        (C := C),
      Nonempty (Fdata.carrier ≃ₜ* ↥(H : Subgroup F)) ∧
      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.