Free pro-p groups

DefinitionPro-\(p\) group#✓fully proved

For a natural number \(p\), a group \(G\) with a topology is a pro-\(p\) group when \(G\) is compact, Hausdorff and totally disconnected, and every open normal subgroup of \(G\) has index \(p^k\) for some \(k \in \mathbb{N}\).

def IsProP (p : ℕ) (G : Type) [Group G] [TopologicalSpace G] : Prop :=
  CompactSpace G ∧ T2Space G ∧ TotallyDisconnectedSpace G ∧
    ∀ N : Subgroup G, N.Normal → IsOpen (N : Set G) → ∃ k : ℕ, N.index = p ^ k

Used by 1

Used byFree pro-\(p\) group on given generators

DefinitionFree pro-\(p\) group on given generators#✓fully proved

Let \(p\) and \(d\) be natural numbers, \(F\) a topological group and \(x_1, \dots, x_d \in F\). Then \(F\) is a free pro-\(p\) group on \(x_1, \dots, x_d\) when \(F\) is a pro-\(p\) group, the closure of the subgroup generated by \(x_1, \dots, x_d\) is all of \(F\), and for every finite \(p\)-group \(P\) and all \(y_1, \dots, y_d \in P\) there is a group homomorphism \(\varphi \colon F \to P\) with open kernel such that \(\varphi(x_i) = y_i\) for every \(i\).

def IsFreeProPOn (p d : ℕ) (F : Type) [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    (x : Fin d → F) : Prop :=
  IsProP p F ∧ (Subgroup.closure (Set.range x)).topologicalClosure = ⊤ ∧
    ∀ (P : Type) [Group P] [Finite P], IsPGroup p P → ∀ y : Fin d → P,
      ∃ φ : F →* P, IsOpen (φ.ker : Set F) ∧ ∀ i, φ (x i) = y i

Uses 1 · Used by 1

Statement usesPro-\(p\) group

Used byRibes's question on fixed subgroups of free pro-\(p\) groups (Kourovka 12.70)

DefinitionRibes's question on fixed subgroups of free pro-\(p\) groups (Kourovka 12.70)#✓fully proved

The statement that for every prime \(p\), every free pro-\(p\) group \(F\) on finitely many generators \(x_1, \dots, x_d\) and every continuous automorphism \(\Delta \ne 1\) of \(F\) with \(\Delta^{p^k} = 1\) for some \(k \in \mathbb{N}\), the fixed subgroup \(\mathrm{Fix}_F(\Delta) = \{z \in F \mid \Delta(z) = z\}\) has finite rank: there is a finite set \(S \subseteq \mathrm{Fix}_F(\Delta)\) such that the closure of the subgroup generated by \(S\) equals \(\mathrm{Fix}_F(\Delta)\).

def fixedSubgroupFinitelyGenerated : Prop :=
  ∀ p : ℕ, p.Prime → ∀ (d : ℕ) (F : Type) [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    (x : Fin d → F), IsFreeProPOn p d F x →
    ∀ Δ : MulAut F, Continuous Δ → Δ ≠ 1 → (∃ k : ℕ, Δ ^ (p ^ k) = 1) →
      ∃ S : Finset F, (∀ s ∈ S, Δ s = s) ∧
        ((Subgroup.closure (S : Set F)).topologicalClosure : Set F) = {z | Δ z = z}

Uses 1 · Used by 1

Statement usesFree pro-\(p\) group on given generators

Used byFixed subgroup of a free pro-p group is finitely generated

TheoremFixed subgroup of a free pro-p group is finitely generated#●ready to prove

Resolved true: the Kourovka Archive answers 12.70 "Yes, it is finite" (C. Scheiderer, 1999); moreover, the fixed points of a finite p-group of automorphisms of a free pro-p group form a free factor (Herfort, Ribes and Zalesskii, 1999), which has finite rank when F does. Source: E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Archive of Solved Problems, Problem 12.70 (L. Ribes); resolution: C. Scheiderer, Proc. Amer. Math. Soc. 127 (1999), no. 3, 695-700; W. N. Herfort, L. Ribes and P. A. Zalesskii, Forum Math. 11 (1999), no. 1, 49-61, Kourovka Archive, Problem 12.70: Yes, it is finite (Scheiderer); the fixed points of a finite p-group of automorphisms form a free factor (Herfort-Ribes-Zalesskii).

public theorem_wanted fixedSubgroupFinitelyGenerated_holds : fixedSubgroupFinitelyGenerated

Uses 1

Statement usesRibes's question on fixed subgroups of free pro-\(p\) groups (Kourovka 12.70)

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.