Profinite CN-groups

DefinitionPronilpotent subgroup#✓fully proved

A subgroup \(H\) of a group \(G\) carrying a topology is pronilpotent when, for every open normal subgroup \(N\) of \(G\), the image of \(H\) in the quotient \(G/N\) is nilpotent.

For a closed subgroup of a profinite group this says that \(H\) is an inverse limit of finite nilpotent groups, since the subgroups \(H \cap N\) are cofinal among the open normal subgroups of \(H\).

def IsPronilpotent {G : Type} [Group G] [TopologicalSpace G] (H : Subgroup G) : Prop :=
  ∀ (N : Subgroup G) [N.Normal], IsOpen (N : Set G) →
    Group.IsNilpotent (H.map (QuotientGroup.mk' N))

Used by 1

Used byProblem of a finitely generated non-prosoluble profinite CN-group (Kourovka 20.90)

DefinitionProblem of a finitely generated non-prosoluble profinite CN-group (Kourovka 20.90)#✓fully proved

The statement that there is an infinite profinite group \(G\), that is, a compact, Hausdorff, totally disconnected topological group, such that \(G\) is topologically finitely generated (the closure of the subgroup generated by some finite set is \(G\)), the centralizer of every non-trivial element of \(G\) is pronilpotent (so \(G\) is a CN-group), and \(G\) is not prosoluble: for some open normal subgroup \(N\) of \(G\), the quotient \(G/N\) is not soluble.

def existsFGInfiniteProfiniteCNGroupNotProsoluble : Prop :=
  ∃ (G : Type) (_ : Group G) (_ : TopologicalSpace G) (_ : IsTopologicalGroup G)
    (_ : CompactSpace G) (_ : T2Space G) (_ : TotallyDisconnectedSpace G),
    Infinite G ∧ (∃ s : Finset G, (Subgroup.closure (s : Set G)).topologicalClosure = ⊤) ∧
    (∀ g : G, g ≠ 1 → IsPronilpotent (Subgroup.centralizer {g})) ∧
    ¬ ∀ (N : Subgroup G) [N.Normal], IsOpen (N : Set G) → Group.IsSolvable (G ⧸ N)

Uses 1 · Used by 1

Statement usesPronilpotent subgroup

Used byA finitely generated non-prosoluble profinite CN-group exists

TheoremA finitely generated non-prosoluble profinite CN-group exists#●ready to prove

There is an infinite profinite group \(G\), that is, a compact, Hausdorff, totally disconnected topological group, such that \(G\) is topologically finitely generated (the closure of the subgroup generated by some finite set is \(G\)), the centralizer of every non-trivial element of \(G\) is pronilpotent, and \(G\) is not prosoluble: for some open normal subgroup \(N\) of \(G\), the quotient \(G/N\) is not soluble. This answers Kourovka Problem 20.90.

Kinyon and Urban (Section 3.35) give an infinite two-generated closed subgroup of \(\mathrm{SL}_2(\mathbb{F}_4[[t]])\) that maps onto \(\mathrm{SL}_2(\mathbb{F}_4) \cong A_5\) and in which every non-identity element has abelian, hence pronilpotent, centralizer.

public theorem_wanted existsFGInfiniteProfiniteCNGroupNotProsoluble_holds :
    existsFGInfiniteProfiniteCNGroupNotProsoluble

Sources

• E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 20.90 (P. Shumyatsky); resolution: M. Kinyon and J. Urban, Results on problems from the Kourovka Notebook, preprint (September 2026), Kourovka Notebook site, Section 3.35: a two-generated closed subgroup G of SL₂(F₄[[t]]) that is infinite, maps onto SL₂(F₄) ≅ A₅ by reduction modulo t (so it is not prosoluble), and in which the centralizer of every non-identity element is abelian; an AI solution confirmed by P. Shumyatsky, Kourovka Notebook (21st issue), Problem 20.90: An example is found, https://kourovkanotebookorg.wordpress.com/wp-content/uploads/2026/09/kourovka-mathematics.pdf.

Uses 1

Statement usesProblem of a finitely generated non-prosoluble profinite CN-group (Kourovka 20.90)

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.