Documentation

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

The peripheral conjugators cannot all coincide #

Let F be a free pro-p group of rank r ≥ 2 with basis x_0, …, x_{r-1} and cusp z = (x_0 ⋯ x_{r-1})⁻¹. The peripheral-power theorem (TauCeti.Peripheral.exists_peripheralAut) produces, for every unit u ∈ ℤ_pˣ, an automorphism φ with φ (x i) = (c i)⁻¹ * x i ^ u * c i and φ z = d⁻¹ * z ^ u * d, where ^ u is the p-adic power. This file shows that for every u ∈ ℤ_p other than 0 and 1, in particular for every unit u ≠ 1, no endomorphism φ of F satisfies these equations with the r + 1 conjugators c 0, …, c (r-1), d all equal.

A common conjugator g would make ψ := g * φ (·) * g⁻¹ carry every x_i to x_i ^ u and the cusp to z ^ u on the nose, so x_0 ^ u ⋯ x_{r-1} ^ u = (x_0 ⋯ x_{r-1}) ^ u. That identity fails: map F to the Heisenberg group over ℤ_p by x_0 ↦ a = (1, 0, 0), x_1 ↦ b = (0, 1, 0) and x_i ↦ 1 for i ≥ 2. By the power formula TauCeti.HeisenbergGroup.padicPow_eq the central coordinates of a ^ u * b ^ u and (a * b) ^ u are u ^ 2 and u + (u choose 2), which differ by u choose 2 = u (u - 1) / 2 ≠ 0. The same Heisenberg detection argument shows, in rank at least three, that the diagonal power map is not peripheral (TauCeti.Peripheral.not_isConj_diagonalPow).

In rank at least two the conjugators of a peripheral automorphism are therefore genuinely independent data, and the existence theorem cannot be strengthened to a single conjugator.

Main results #

References #

theorem TauCeti.Peripheral.padicPow_prod_basis_ne {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 + 2))) {u : ℤ_[p]} (hu₀ : u ≠ 0) (hu₁ : u ≠ 1) :
hF.padicPow (List.ofFn (basis e)).prod u ≠ (List.ofFn fun (i : Fin (n + 2)) => hF.padicPow (basis e i) u).prod

The power of the product is not the product of the powers. For a free pro-p group of rank at least two and u ∈ ℤ_p other than 0 and 1, the p-adic power (x_0 ⋯ x_{r-1}) ^ u of the ordered product of the basis differs from the ordered product x_0 ^ u ⋯ x_{r-1} ^ u of the powers.

theorem TauCeti.Peripheral.apply_cusp_ne_padicPow_of_apply_basis_eq_padicPow {p : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] {M : Type u_2} [FunLike M F F] [MonoidHomClass M F F] {n : ℕ} (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin (n + 2))) {u : ℤ_[p]} (hu₀ : u ≠ 0) (hu₁ : u ≠ 1) (φ : M) (hφ : ∀ (i : Fin (n + 2)), φ (basis e i) = hF.padicPow (basis e i) u) :
φ (cusp (basis e)) ≠ hF.padicPow (cusp (basis e)) u

No endomorphism is the u-th power on the whole peripheral tuple. For a free pro-p group of rank at least two and u ∈ ℤ_p other than 0 and 1, an endomorphism φ sending every basis element x_i to x_i ^ u does not send the cusp z to z ^ u.

theorem TauCeti.Peripheral.exists_ne_of_apply_eq_conj {p : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] {M : Type u_2} [FunLike M F F] [MonoidHomClass M F F] {n : ℕ} (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin (n + 2))) {u : ℤ_[p]} (hu₀ : u ≠ 0) (hu₁ : u ≠ 1) (φ : M) {c : Fin (n + 2) → F} {d : F} (hc : ∀ (i : Fin (n + 2)), φ (basis e i) = (c i)⁻¹ * hF.padicPow (basis e i) u * c i) (hd : φ (cusp (basis e)) = d⁻¹ * hF.padicPow (cusp (basis e)) u * d) :
∃ (i : Fin (n + 2)), c i ≠ d

The peripheral conjugators are not all equal. For a free pro-p group of rank at least two and u ∈ ℤ_p other than 0 and 1, if an endomorphism φ satisfies φ (x i) = (c i)⁻¹ * x i ^ u * c i for every basis element and φ z = d⁻¹ * z ^ u * d on the cusp, then some c i differs from d.