NYLL

theorem · Pro-C groups

The Schreier rank of an open subgroup

An open subgroup of a finite-rank free pro-C group is free, with the expected index-dependent rank.

Openness gives finite index, and the rank formula measures exactly how passing to the subgroup changes the number of free generators. The assumptions on C ensure that this process preserves freeness. This is the profinite counterpart of the classical Schreier formula for free groups, developed in the pro-C setting in Ribes and Zalesskii’s monograph.

ProCGroups on GitHub ↗

Mathematical statement

Assume $C$ is closed under isomorphisms, subgroups, quotients, finite direct products, and extensions, and contains a nontrivial finite cyclic group. Let $F$ be epimorphically free pro-$C$ on a finite converging basis $X$, and let $H\le F$ be open. Put $r=|X|$ and $i=[F:H]$.

There is a free pro-$C$ group with a basis of size $$\begin{cases}0,&r=0,\\1+i(r-1),&r\ge1,\end{cases}$$ and a continuous group isomorphism from that group to $H$. The conclusion provides freeness as well as a numerical rank.

Lean code

ReidemeisterSchreier.Profinite.exists_basis_openSubgroup_of_extensionClosed_finiteRank

Published library source ↗Same source in NYLL ↗

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)
In-scope Lean context
open scoped Topology Pointwise

namespace ReidemeisterSchreier

namespace Profinite

open ProCGroups

open ProCGroups.FreeProC

open ProCGroups.ProC

universe u
Full declaration and proof
/--
Finite-rank extension-closed variety case using the Schreier rank-transform cardinality bound.
-/
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) := by
  classical
  rcases hVar.closureBundle_of_isomClosed_extensionClosed hIso hExt with
    ⟨hForm, hSub, hIso', hQuot, hExt'⟩
  let n : ℕ := _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H
      : Subgroup F)))
  rcases exists_finiteIndexBasisCarrierAndMap_openSubgroup
      C hForm hSub hIso' hExt' hF H with
    ⟨B, hBfin, μ, hμfree⟩
  let : Finite B := hBfin
  let Fdata : EpimorphicallyFreeProCGroupOnConvergingSetData
      (C := C) :=
    { basis := B
      carrier :=
        ProCGrp.of C (ProfiniteGrp.of ↥(H : Subgroup F)) hμfree.hasOpenNormalBasisInClass
      inclusion := μ
      isEpimorphicallyFree := hμfree }
  let Fambient : EpimorphicallyFreeProCGroupOnConvergingSetData
      (C := C) :=
    { basis := X
      carrier := ProCGrp.of C (ProfiniteGrp.of F) hF.hasOpenNormalBasisInClass
      inclusion := ι
      isEpimorphicallyFree := hF }
  have hAmbientRank :
      Cardinal.mk X = Generation.topologicalRank F :=
    basisCard_eq_topologicalRank_of_finiteBasis C hQuot hcyc Fambient
  have hdF : Generation.topologicalRank F = Nat.card X := by
    calc
      Generation.topologicalRank F = Cardinal.mk X := hAmbientRank.symm
      _ = (Nat.card X : Cardinal) := (Nat.cast_card (α := X)).symm
  have hdHle :
      Generation.topologicalRank ↥(H : Subgroup F) ≤ (n : Cardinal) := by
    simpa [n] using
      topologicalRank_openSubgroup_le_rankTransform_of_topologicalRank_eq_nat
        (G := F) hdF H
  have hDataBasis :
      Cardinal.mk Fdata.basis = Generation.topologicalRank Fdata.carrier :=
    basisCard_eq_topologicalRank_of_finiteBasis C hQuot hcyc Fdata
  have hle : Cardinal.mk Fdata.basis ≤ (n : Cardinal) := by
    simpa [Fdata] using hDataBasis.trans_le hdHle
  rcases exists_exactGeneratingFamily_openSubgroup_of_finiteBasis_ulift
      C hForm hSub hIso' hQuot hExt' hcyc hF H with
    ⟨κ, hκ⟩
  let : TopologicalSpace (FreeGroup (ULift.{u} (Fin n))) := ⊥
  let : DiscreteTopology (FreeGroup (ULift.{u} (Fin n))) := ⟨rfl⟩
  let φ : FreeGroup (ULift.{u} (Fin n)) →ₜ* ↥(H : Subgroup F) :=
    { toMonoidHom := FreeGroup.lift κ
      continuous_toFun := continuous_of_discreteTopology }
  have hComp :
      ProCGroups.Completion.IsProCCompletion
        (C)
        (FreeGroup (ULift.{u} (Fin n))) ↥(H : Subgroup F) φ := by
    obtain ⟨Y, hYfree, hYcard⟩ :=
      exists_freeBasis_comap_freeGroupLift_of_openSubgroup_of_rankTransform
        (F := F) (X := X) hF.generates_range H
    let βF : FreeGroup X →* F := FreeGroup.lift ι
    let L : Subgroup (FreeGroup X) := Subgroup.comap βF (H : Subgroup F)
    let ψ : L →* ↥(H : Subgroup F) :=
      { toFun := fun g => ⟨βF g.1, g.2⟩
        map_one' := by simp only [OneMemClass.coe_one, map_one, Subgroup.mk_eq_one]
        map_mul' := by
          intro a b
          ext
          simp only [Subgroup.coe_mul, map_mul]}
    let : TopologicalSpace (FreeGroup X) := ⊥
    let : DiscreteTopology (FreeGroup X) := ⟨rfl⟩
    have hβFdense : DenseRange βF :=
      denseRange_freeGroupLift_of_topologicallyGenerates
        (F := F) (X := X) hF.generates_range
    have hψdense : DenseRange ψ := by
      exact denseRange_comapMap_of_openSubgroup (φ := βF) hβFdense H.isOpen'
    let : TopologicalSpace (FreeGroup Y) := ⊥
    let : DiscreteTopology (FreeGroup Y) := ⟨rfl⟩
    let bY : FreeGroupBasis Y L := Classical.choice hYfree
    let eY : FreeGroup Y ≃* L := bY.repr.symm
    let φY : FreeGroup Y →ₜ* ↥(H : Subgroup F) :=
      { toMonoidHom := ψ.comp eY.toMonoidHom
        continuous_toFun := continuous_of_discreteTopology }
    have hψcont : Continuous ψ := by
      simpa using (continuous_of_discreteTopology : Continuous ψ)
    have hφYdense : DenseRange φY := by
      change DenseRange (fun y : FreeGroup Y => ψ (eY y))
      exact hψdense.comp (Function.Surjective.denseRange eY.surjective) hψcont
    have 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 := by
      intro Q _ _ _ _ _ hQ χL
      rcases
          exists_continuousFiniteQuotientLift_of_comap_freeGroupLift
            (C := C)
            (hForm := hForm) (hSub := hSub) (hIso := hIso')
            (hQuot := hQuot) (hExt := hExt')
            (X := X) (F := F) (ι := ι) hF H hQ χL with
        ⟨φbar, hφbarCont, hφbarFac⟩
      refine ⟨φbar, ⟨hφbarCont, hφbarFac⟩, ?_⟩
      intro φbar' hφbar'
      have hEq : (fun h : ↥(H : Subgroup F) => φbar h) = fun h => φbar' h := by
        apply DenseRange.equalizer (f := ψ) hψdense
        · exact hφbarCont
        · exact hφbar'.1
        · funext l
          exact congrArg (fun f : L →* Q => f l) (hφbarFac.trans hφbar'.2.symm)
      apply MonoidHom.ext
      intro h
      simpa using (congrArg (fun f : ↥(H : Subgroup F) → Q => f h) hEq).symm
    have hfinite :
        DenseAbstractSchreierFiniteQuotientLiftProperty
          (C := C) H φY.toMonoidHom := by
      exact denseAbstractSchreierFiniteQuotientLiftProperty_of_equiv
        (C := C) (H := H) (eY := eY) (ψ := ψ) hψfinite
    have hCompY :
        ProCGroups.Completion.IsProCCompletion
          (C)
          (FreeGroup Y) ↥(H : Subgroup F) φY := by
      exact isProCCompletion_denseAbstractSchreier_of_finiteQuotientLifts
        (C := C)
        (hForm := hForm) (hSub := hSub) (hIso := hIso')
        (X := X) (F := F) (ι := ι) hF H hφYdense hfinite
    exact
      isProCCompletion_freeGroupLift_of_exactGeneratingFamily_of_completion
        (C := C) hSub hIso' hQuot hcyc
        (Y := Y) (Z := ULift.{u} (Fin n)) (by simpa [n] using hYcard) hCompY hκ
  have hκfree :
      IsEpimorphicallyFreeProCGroupOnConvergingSet
        (C := C) (ULift.{u} (Fin n)) ↥(H : Subgroup F) κ := by
    have hfree :=
      proCCompletionOfAbstractFreeGroup_is_free
        (C := C)
        (X := ULift.{u} (Fin n)) (Fhat := ↥(H : Subgroup F)) (ι := φ) hComp
    convert hfree using 1
    ext x
    change ((κ x : ↥(H : Subgroup F)) : F) =
      ((FreeGroup.lift κ (FreeGroup.of x) : ↥(H : Subgroup F)) : F)
    simp only [FreeGroup.lift_apply_of]
  let Fexact : EpimorphicallyFreeProCGroupOnConvergingSetData
      (C := C) :=
    { basis := ULift.{u} (Fin n)
      carrier :=
        ProCGrp.of C (ProfiniteGrp.of ↥(H : Subgroup F)) hκfree.hasOpenNormalBasisInClass
      inclusion := κ
      isEpimorphicallyFree := hκfree }
  have hExactBasis :
      Cardinal.mk Fexact.basis = Generation.topologicalRank Fexact.carrier :=
    basisCard_eq_topologicalRank_of_finiteBasis C hQuot hcyc Fexact
  have hExactCard : Cardinal.mk Fexact.basis = (n : Cardinal) := by
    simp only [Cardinal.mk_fintype, Fintype.card_ulift, Fintype.card_fin, Fexact]
  have hge : (n : Cardinal) ≤ Cardinal.mk Fdata.basis := by
    exact le_of_eq <| by
      calc
        (n : Cardinal) = Cardinal.mk Fexact.basis := hExactCard.symm
        _ = Generation.topologicalRank Fexact.carrier := hExactBasis
        _ = Generation.topologicalRank Fdata.carrier := by rfl
        _ = Cardinal.mk Fdata.basis := hDataBasis.symm
  refine ⟨Fdata, ⟨ContinuousMulEquiv.refl _⟩, ?_⟩
  have hCard : Cardinal.mk Fdata.basis = (n : Cardinal) := le_antisymm hle hge
  simpa [n] using hCard
Source credits and license
Copyright (c) 2026 Naganori Yamaguchi (https://github.com/n-yamaguchi-0729). All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Naganori Yamaguchi (assisted by OpenAI Codex)

References

  1. Luis Ribes and Pavel Zalesskii. Profinite Groups. Springer-Verlag Berlin Heidelberg, 2010. Second edition; Ergebnisse der Mathematik und ihrer Grenzgebiete, 3. Folge, volume 40.

Published source: 7d74e3a9.

← All selected results in Pro-C groups