Nottingham group

DefinitionNottingham condition on automorphisms of power series#✓fully proved

Let \(R\) be a commutative ring. A ring automorphism \(\varphi\) of the power series ring \(R[[x]]\) satisfies the Nottingham condition when \(\varphi(x) - x\) lies in the ideal generated by \(x^2\), that is, when \(\varphi(x) = x(1 + a_1 x + a_2 x^2 + \cdots)\) for some \(a_1, a_2, \ldots \in R\).

For a prime \(p\) and \(R = \mathbb{Z}/p\mathbb{Z}\), every ring automorphism of \(R[[x]]\) is \(R\)-linear and preserves the maximal ideal, so it is the substitution \(x \mapsto \varphi(x)\); the automorphisms satisfying the Nottingham condition then form the Nottingham group \(N(R)\).

def IsNottingham {R : Type*} [CommRing R] (φ : RingAut (PowerSeries R)) : Prop :=
  φ PowerSeries.X - PowerSeries.X ∈ Ideal.span {PowerSeries.X ^ 2}

Used by 1

Used byKourovka Problem 12.24 (free subgroups of the Nottingham group)

DefinitionKourovka Problem 12.24 (free subgroups of the Nottingham group)#✓fully proved

For every prime \(p\) there is an injective group homomorphism from the free group \(F_2\) on two generators to the group of ring automorphisms of \((\mathbb{Z}/p\mathbb{Z})[[x]]\) whose image consists of automorphisms \(\varphi\) with \(\varphi(x) - x \in (x^2)\), that is, of elements of the Nottingham group \(N(\mathbb{Z}/p\mathbb{Z})\).

def nottinghamContainsFreeGroup : Prop :=
  ∀ p : ℕ, p.Prime → ∃ f : FreeGroup (Fin 2) →* RingAut (PowerSeries (ZMod p)),
    Function.Injective f ∧ ∀ g, IsNottingham (f g)

Uses 1 · Used by 1

Statement usesNottingham condition on automorphisms of power series

Used byThe Nottingham group contains a free subgroup of rank 2

TheoremThe Nottingham group contains a free subgroup of rank 2#●ready to prove

For every prime \(p\) there is an injective group homomorphism \(f\) from the free group \(F_2\) on two generators to the group of ring automorphisms of the power series ring \((\mathbb{Z}/p\mathbb{Z})[[x]]\) such that, for every \(g \in F_2\), the automorphism \(\varphi = f(g)\) satisfies \(\varphi(x) - x \in (x^2)\); that is, the Nottingham group \(N(\mathbb{Z}/p\mathbb{Z})\) contains a copy of \(F_2\).

The Kourovka Archive answers 12.24 "Yes, it does" (R. Camina, 1997). Camina embeds, for every prime \(p\), every countably based pro-\(p\) group in \(N(\mathbb{F}_p)\), where \(\mathbb{F}_p = \mathbb{Z}/p\mathbb{Z}\); the free pro-\(p\) group of rank \(2\) contains \(F_2\), since free groups are residually \(p\).

public theorem_wanted nottinghamContainsFreeGroup_holds : nottinghamContainsFreeGroup

Sources

• 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.24 (D. L. Johnson); resolution: R. Camina, J. Algebra 196 (1997), no. 1, 101-113, Camina's theorem that every countably based (in particular every finitely generated) pro-p group embeds in N(F_p); Kourovka Archive, Problem 12.24.

Uses 1

Statement usesKourovka Problem 12.24 (free subgroups of the Nottingham group)

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.