The Heisenberg group over a pro-p ring is pro-p

Let R be a compact Hausdorff topological ring whose additive group is pro-p. Then the Heisenberg group HeisenbergGroup R, with the topology of R × R × R, is pro-p (TauCeti.HeisenbergGroup.isProP). It is an extension

1 → R → HeisenbergGroup R → R × R → 1,

where R embeds as the central z-axis (0, 0, z) and the quotient map forgets the z-coordinate, and pro-p groups are closed under extensions with compact total group (TauCeti.IsProP.of_ker_isProP).

Over the p-adic integers this gives the compact, totally disconnected pro-p group HeisenbergGroup ℤ_[p] of nilpotency class two (TauCeti.HeisenbergGroup.isProP_padicInt). By the universal property of free pro-p groups it receives a continuous homomorphism from a free pro-p group sending two chosen generators to (1, 0, 0) and (0, 1, 0); since their commutator is (0, 0, 1), this detects the brackets of generators in the graded Lie ring of the closed lower central series of a free pro-p group. Two facts make the detection work: the closed lower central series of the Heisenberg group over a Hausdorff topological ring stops at γ_2 = 1 (TauCeti.HeisenbergGroup.closedLowerCentralSeries_two_eq_bot), and the p-adic powers of (0, 0, z) are the elements (0, 0, c z).

More generally, the p-adic powers in HeisenbergGroup ℤ_[p] are given by the same polynomial formula as the natural powers, (x, y, z) ^ c = (c x, c y, c z + (c choose 2) x y), with the binomial coefficient of the binomial ring ℤ_[p].

Main results

• TauCeti.HeisenbergGroup.isProP: the Heisenberg group over a compact Hausdorff topological ring with pro-p additive group is pro-p.
• TauCeti.HeisenbergGroup.isProP_padicInt: the Heisenberg group over ℤ_[p] is pro-p.
• TauCeti.HeisenbergGroup.padicPow_eq: the p-adic power of (x, y, z) by c is (c x, c y, c z + (c choose 2) x y).
• TauCeti.HeisenbergGroup.padicPow_mk_zero_zero: the p-adic power of (0, 0, z) by c is (0, 0, c z).

References

• L. Ribes and P. Zalesskii, Profinite Groups, 2nd ed., Section 2.2.

theorem TauCeti.HeisenbergGroup.isProP {p : ℕ} {R : Type u_1} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R] (hR : IsProP p (Multiplicative R)) : IsProP p (HeisenbergGroup R)

The Heisenberg group over a compact Hausdorff topological ring whose additive group is pro-p is pro-p.

theorem TauCeti.HeisenbergGroup.isProP_padicInt (p : ℕ) [Fact (Nat.Prime p)] : IsProP p (HeisenbergGroup ℤ_[p])

The Heisenberg group over the p-adic integers is pro-p.

theorem TauCeti.HeisenbergGroup.padicPow_eq {p : ℕ} [Fact (Nat.Prime p)] (a : HeisenbergGroup ℤ_[p]) (c : ℤ_[p]) : ⋯.padicPow a c = { x := c * a.x, y := c * a.y, z := c * a.z + Ring.choose c 2 * (a.x * a.y) }

The power formula for p-adic exponents: in the Heisenberg group over ℤ_[p], (x, y, z) ^ c = (c x, c y, c z + (c choose 2) x y), where c choose 2 is the binomial coefficient Ring.choose c 2 of the binomial ring ℤ_[p].

@[simp]

theorem TauCeti.HeisenbergGroup.padicPow_mk_zero_zero {p : ℕ} [Fact (Nat.Prime p)] (z c : ℤ_[p]) : ⋯.padicPow { x := 0, y := 0, z := z } c = { x := 0, y := 0, z := c * z }

The p-adic power of an element (0, 0, z) of the z-axis of the Heisenberg group over ℤ_[p] by c is (0, 0, c z).