Module

RankBound.lean

Nyll.ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.RankBound

6 declarations indexed from sourceView source ↗

Module documentation

Cardinal and finite-rank Schreier bounds

This module defines the cardinal Schreier transform, proves its finite and infinite simplifications, and bounds the topological rank of an open subgroup of a compact Hausdorff totally disconnected group by the classical finite rank transform.

Imports4

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.FreeBasis
Nyll.ProCGroups.GroupTheory.Subgroups
Nyll.ProCGroups.FiniteGeneration.Basic
Mathlib.SetTheory.Cardinal.Finite

Imported by3

def

schreierRankTransformCardinal

L38 ↗

ReidemeisterSchreier.Profinite.schreierRankTransformCardinal

Documentation

Cardinal form of the Schreier rank transform for an open subgroup of finite index \(n\). For finite rank this is the usual Schreier transform \(1+n(d-1)\). For infinite cardinals the finite-index transform stabilizes at the original cardinal.

Source context 8 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.FiniteGeneration
open ReidemeisterSchreier.Discrete.OpenSubgroups
universe u

Lean source · statement

def schreierRankTransformCardinal (κ : Cardinal) (n : ℕ) : Cardinal

theorem

schreierRankTransformCardinal_natCast

L45 ↗

ReidemeisterSchreier.Profinite.schreierRankTransformCardinal_natCast

Documentation

On a finite cardinal, the cardinal Schreier transform agrees with the usual natural-number formula.

Source context 8 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.FiniteGeneration
open ReidemeisterSchreier.Discrete.OpenSubgroups
universe u

Lean source · statement

theorem schreierRankTransformCardinal_natCast (d n : ℕ) :
    schreierRankTransformCardinal (d : Cardinal) n =
      (_root_.ReidemeisterSchreier.Schreier.rankTransform d n : Cardinal)

theorem

schreierRankTransformCardinal_eq_self_of_aleph0_le

L52 ↗

ReidemeisterSchreier.Profinite.schreierRankTransformCardinal_eq_self_of_aleph0_le

Documentation

A finite-index Schreier transform fixes every infinite cardinal.

Source context 8 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.FiniteGeneration
open ReidemeisterSchreier.Discrete.OpenSubgroups
universe u

Lean source · statement

theorem schreierRankTransformCardinal_eq_self_of_aleph0_le
    {κ : Cardinal} (hκ : Cardinal.aleph0 ≤ κ) (n : ℕ) :
    schreierRankTransformCardinal κ n = κ

theorem

schreierRankTransformCardinal_mk_finite

L61 ↗

ReidemeisterSchreier.Profinite.schreierRankTransformCardinal_mk_finite

Documentation

For a finite input cardinal, the Schreier rank-transform cardinal is the corresponding finite Schreier value.

Source context 8 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.FiniteGeneration
open ReidemeisterSchreier.Discrete.OpenSubgroups
universe u

Lean source · statement

theorem schreierRankTransformCardinal_mk_finite (X : Type u) [Finite X] (n : ℕ) :
    schreierRankTransformCardinal (Cardinal.mk X) n =
      (_root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) n : Cardinal)

theorem

schreierRankTransformCardinal_mk_infinite

L71 ↗

ReidemeisterSchreier.Profinite.schreierRankTransformCardinal_mk_infinite

Documentation

For an infinite input cardinal, the finite-index Schreier rank transform is the same infinite cardinal.

Source context 8 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.FiniteGeneration
open ReidemeisterSchreier.Discrete.OpenSubgroups
universe u

Lean source · statement

theorem schreierRankTransformCardinal_mk_infinite (X : Type u) [Infinite X] (n : ℕ) :
    schreierRankTransformCardinal (Cardinal.mk X) n = Cardinal.mk X

theorem

topologicalRank_openSubgroup_le_rankTransform_of_topologicalRank_eq_nat

L80 ↗

ReidemeisterSchreier.Profinite.topologicalRank_openSubgroup_le_rankTransform_of_topologicalRank_eq_nat

Documentation

An open subgroup of a finitely generated profinite group satisfies the usual Schreier bound on the minimal number of topological generators.

Source context 8 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.FiniteGeneration
open ReidemeisterSchreier.Discrete.OpenSubgroups
universe u

Lean source · statement

theorem topologicalRank_openSubgroup_le_rankTransform_of_topologicalRank_eq_nat
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    {d : ℕ} (hd : Generation.topologicalRank G = d)
    (U : OpenSubgroup G) :
    Generation.topologicalRank ↥(U : Subgroup G) ≤
      (_root_.ReidemeisterSchreier.Schreier.rankTransform d (Nat.card (G ⧸ (U : Subgroup G))) :
          Cardinal)

Module documentation

Cardinal and finite-rank Schreier bounds

Declarations

schreierRankTransformCardinal

schreierRankTransformCardinal_natCast

schreierRankTransformCardinal_eq_self_of_aleph0_le

schreierRankTransformCardinal_mk_finite

schreierRankTransformCardinal_mk_infinite

topologicalRank_openSubgroup_le_rankTransform_of_topologicalRank_eq_nat