Documentation

TauCeti.Topology.Algebra.Group.Profinite.Free.Peripheral.Diagonal

The diagonal power map is not peripheral in rank at least three #

Let F be a free pro-p group of rank r with basis x_0, …, x_{r-1} and cusp z = (x_0 ⋯ x_{r-1})⁻¹. For a unit u ∈ ℤ_pˣ, the diagonal power map is the continuous automorphism x_i ↦ x_i ^ u of F, where ^ u is the p-adic power; it exists by the automorphism criterion for conjugated unit powers (TauCeti.IsProP.exists_continuousAut_apply_eq_conj_padicPow_const). It carries every basis element to a conjugate of its u-th power, trivially. This file shows that for r ≥ 3 and u ≠ 1 it does not do so on the cusp: the peripheral condition on the basis alone does not imply it on the cusp.

The obstruction is the value x_0 ^ u ⋯ x_{r-1} ^ u of the diagonal power map on the product x_0 ⋯ x_{r-1}, which is not conjugate to any p-adic power of x_0 ⋯ x_{r-1} once u ≠ 0, 1. To see this, map F to the Heisenberg group over ℤ_p by x_0 ↦ a = (1, 0, 0), x_1 ↦ b = (0, 1, 0), x_2 ↦ (a b)⁻¹ and x_i ↦ 1 for i ≥ 3. This kills x_0 ⋯ x_{r-1}, hence all its powers and their conjugates, but sends x_0 ^ u ⋯ x_{r-1} ^ u to a ^ u b ^ u ((a b)⁻¹) ^ u = (0, 0, u choose 2), by the power formula TauCeti.HeisenbergGroup.padicPow_eq, and u choose 2 = u (u - 1) / 2 is nonzero for u ≠ 0, 1. This adapts the Heisenberg detection argument of TauCeti.Peripheral.not_isPeripheralAut_of_apply_basis_eq_inv (in Peripheral/Reflection.lean) from the Heisenberg group over 𝔽_p to the one over ℤ_p, so that it also detects u ≡ 1 mod p.

In rank two the analogous statement is false: at u = -1 the diagonal power map is the inversion of TauCeti.Peripheral.exists_inversion_two, which is peripheral.

Main results #

References #

theorem TauCeti.Peripheral.not_isConj_diagonalPow {p : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] {n : ℕ} (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin (n + 3))) {u : ℤ_[p]} (hu₀ : u ≠ 0) (hu₁ : u ≠ 1) (v : ℤ_[p]) :
¬IsConj (hF.padicPow (List.ofFn (basis e)).prod v) (List.ofFn fun (i : Fin (n + 3)) => hF.padicPow (basis e i) u).prod

The diagonal power is not conjugate to a power of the product. For a free pro-p group of rank at least three and u ∈ ℤ_p other than 0 and 1, the product x_0 ^ u ⋯ x_{r-1} ^ u of the u-th powers of the basis is not conjugate to any p-adic power (x_0 ⋯ x_{r-1}) ^ v.

theorem TauCeti.Peripheral.not_isPeripheralAut_of_apply_basis_eq_padicPow {p : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] {n : ℕ} (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin (n + 3))) {u : ℤ_[p]ˣ} (hu : u ≠ 1) {φ : ContinuousAut F} (hφ : ∀ (i : Fin (n + 3)), φ (basis e i) = hF.padicPow (basis e i) ↑u) (v : ℤ_[p]ˣ) :

The diagonal power map is not peripheral in rank at least three. For a free pro-p group of rank at least three and a unit u ≠ 1, a continuous automorphism sending every basis element x_i to x_i ^ u is peripheral of no exponent: it sends the cusp to (x_0 ^ u ⋯ x_{r-1} ^ u)⁻¹, which is not conjugate to any p-adic power of the cusp.

theorem TauCeti.Peripheral.exists_diagonalPow_not_isPeripheralAut {p : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] {n : ℕ} (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin (n + 3))) {u : ℤ_[p]ˣ} (hu : u ≠ 1) :
∃ (φ : ContinuousAut F), (∀ (i : Fin (n + 3)), φ (basis e i) = hF.padicPow (basis e i) ↑u) ∧ ∀ (v : ℤ_[p]ˣ), ¬IsPeripheralAut hF (basis e) v φ

The diagonal power map. For a free pro-p group of rank at least three and a unit u ≠ 1, some continuous automorphism sends every basis element x_i to its u-th power x_i ^ u, and it is peripheral of no exponent. So an automorphism carrying every basis element to a conjugate of its u-th power need not do so on the cusp.