Peripheral automorphisms of exponent -1

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})⁻¹, and write P_i := x_0 ⋯ x_{i-1} for the initial products of the basis (Mathlib's Fin.partialProd). This file constructs explicit peripheral automorphisms of exponent -1.

• The reflection. The continuous automorphism reflect with x_i ↦ P_i * x_i⁻¹ * P_i⁻¹ inverts every initial product P_i, in particular the full product x_0 ⋯ x_{r-1}, so it sends the cusp to its inverse on the nose. It is therefore peripheral of exponent -1 in every rank, with conjugator P_i⁻¹ on x_i and 1 on the cusp, and it is an involution.
• The rank-two inversion. In rank two, every automorphism inverting both basis elements is also peripheral of exponent -1: it sends z = (x_0 x_1)⁻¹ to x_1 x_0 = x_0⁻¹ * z⁻¹ * x_0, with conjugator x_0 on the cusp.
• Inversion fails in rank at least three. For r ≥ 3, no automorphism inverting every basis element is peripheral, for any exponent. It sends z to (x_0⁻¹ ⋯ x_{r-1}⁻¹)⁻¹, and the continuous homomorphism to the Heisenberg group over 𝔽_p with x_0 ↦ a, x_1 ↦ b, x_2 ↦ (a b)⁻¹ and x_i ↦ 1 for i ≥ 3, where a and b do not commute, kills z but not its image: the latter maps to (a b)⁻¹ b a ≠ 1.

Automorphisms with prescribed values on the basis exist by the automorphism criterion for conjugated unit powers (TauCeti.IsProP.exists_continuousAut_apply_eq_conj_padicPow_const), and they are unique since the basis generates F topologically.

Main definitions

• TauCeti.Peripheral.reflect: the reflection x_i ↦ P_i * x_i⁻¹ * P_i⁻¹.

Main results

• TauCeti.Peripheral.reflect_basis, TauCeti.Peripheral.eq_reflect_iff: the values of the reflection on the basis, which characterize it.
• TauCeti.Peripheral.reflect_partialProd, TauCeti.Peripheral.reflect_cusp: the reflection inverts every initial product of the basis and the cusp. Its simp normal form, after TauCeti.Peripheral.map_cusp, is TauCeti.Peripheral.cusp_reflect_comp_basis.
• TauCeti.Peripheral.reflect_mul_reflect: the reflection is an involution.
• TauCeti.Peripheral.isPeripheralAut_reflect: the reflection is peripheral of exponent -1.
• TauCeti.Peripheral.isPeripheralAut_of_apply_basis_eq_inv_two: in rank two such an automorphism is peripheral of exponent -1, with cusp conjugator x_0 (TauCeti.Peripheral.apply_cusp_of_apply_basis_eq_inv_two).
• TauCeti.Peripheral.exists_inversion_two: the rank-two inversion exists, with these properties.
• TauCeti.Peripheral.not_isPeripheralAut_of_apply_basis_eq_inv: in rank at least three it is peripheral of no exponent.

References

• Y. Ihara, "Braids, Galois groups, and some arithmetic functions", Proc. ICM Kyoto 1990, 99–120, for peripheral automorphisms of free pro-p groups of rank two, among them the one attached to complex conjugation.

noncomputable def TauCeti.Peripheral.reflect {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin r)) : ContinuousAut F

The reflection. The continuous automorphism of F sending each basis element x_i to P_i * x_i⁻¹ * P_i⁻¹, where P_i = x_0 ⋯ x_{i-1} is the initial product of the basis. It is characterized by its values on the basis (TauCeti.Peripheral.eq_reflect_iff).

@[simp]

theorem TauCeti.Peripheral.reflect_basis {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin r)) (i : Fin r) : (reflect hF e) (basis e i) = Fin.partialProd (basis e) i.castSucc * (basis e i)⁻¹ * (Fin.partialProd (basis e) i.castSucc)⁻¹

The reflection sends x_i to P_i * x_i⁻¹ * P_i⁻¹.

theorem TauCeti.Peripheral.eq_reflect_iff {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin r)) (φ : ContinuousAut F) : φ = reflect hF e ↔ ∀ (i : Fin r), φ (basis e i) = Fin.partialProd (basis e) i.castSucc * (basis e i)⁻¹ * (Fin.partialProd (basis e) i.castSucc)⁻¹

A continuous automorphism of F is the reflection exactly when it sends every basis element x_i to P_i * x_i⁻¹ * P_i⁻¹.

@[simp]

theorem TauCeti.Peripheral.reflect_partialProd {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin r)) (j : Fin (r + 1)) : (reflect hF e) (Fin.partialProd (basis e) j) = (Fin.partialProd (basis e) j)⁻¹

The reflection inverts every initial product P_j = x_0 ⋯ x_{j-1} of the basis.

theorem TauCeti.Peripheral.reflect_cusp {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin r)) : (reflect hF e) (cusp (basis e)) = (cusp (basis e))⁻¹

The reflection sends the cusp to its inverse.

@[simp]

theorem TauCeti.Peripheral.cusp_reflect_comp_basis {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin r)) : cusp (⇑(reflect hF e) ∘ basis e) = (cusp (basis e))⁻¹

The cusp of the reflected basis is the inverse of the cusp. This is the simp normal form of TauCeti.Peripheral.reflect_cusp, whose left-hand side TauCeti.Peripheral.map_cusp rewrites.

@[simp]

theorem TauCeti.Peripheral.reflect_mul_reflect {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin r)) : reflect hF e * reflect hF e = 1

The reflection is an involution.

@[simp]

theorem TauCeti.Peripheral.inv_reflect {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin r)) : (reflect hF e)⁻¹ = reflect hF e

The reflection is its own inverse.

theorem TauCeti.Peripheral.isPeripheralAut_reflect {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin r)) : IsPeripheralAut hF (basis e) (-1) (reflect hF e)

The reflection is peripheral of exponent -1, with conjugator P_i⁻¹ on x_i and 1 on the cusp.

theorem TauCeti.Peripheral.apply_cusp_of_apply_basis_eq_inv_two {p : ℕ} {F : Type u_1} [Group F] [TopologicalSpace F] (e : F ≃ₜ* freeProP p (Fin 2)) {φ : ContinuousAut F} (hφ : ∀ (i : Fin 2), φ (basis e i) = (basis e i)⁻¹) : φ (cusp (basis e)) = (basis e 0)⁻¹ * (cusp (basis e))⁻¹ * basis e 0

In rank two, an automorphism inverting both basis elements sends the cusp z = (x_0 x_1)⁻¹ to x_1 x_0 = x_0⁻¹ * z⁻¹ * x_0.

theorem TauCeti.Peripheral.isPeripheralAut_of_apply_basis_eq_inv_two {p : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin 2)) {φ : ContinuousAut F} (hφ : ∀ (i : Fin 2), φ (basis e i) = (basis e i)⁻¹) : IsPeripheralAut hF (basis e) (-1) φ

The rank-two inversion is peripheral. In rank two, an automorphism inverting both basis elements is peripheral of exponent -1, with conjugator 1 on the basis and x_0 on the cusp.

theorem TauCeti.Peripheral.exists_inversion_two {p : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (e : F ≃ₜ* freeProP p (Fin 2)) : ∃ (φ : ContinuousAut F), (∀ (i : Fin 2), φ (basis e i) = (basis e i)⁻¹) ∧ φ (cusp (basis e)) = (basis e 0)⁻¹ * (cusp (basis e))⁻¹ * basis e 0 ∧ IsPeripheralAut hF (basis e) (-1) φ

The rank-two inversion. In rank two, some continuous automorphism inverts both basis elements. It sends the cusp z = (x_0 x_1)⁻¹ to x_0⁻¹ * z⁻¹ * x_0 and is peripheral of exponent -1.

theorem TauCeti.Peripheral.not_isPeripheralAut_of_apply_basis_eq_inv {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))) {φ : ContinuousAut F} (hφ : ∀ (i : Fin (n + 3)), φ (basis e i) = (basis e i)⁻¹) (u : ℤ_[p]ˣ) : ¬IsPeripheralAut hF (basis e) u φ

Inversion is not peripheral in rank at least three. For r ≥ 3, an automorphism inverting every basis element is peripheral of no exponent: it sends the cusp to (x_0⁻¹ ⋯ x_{r-1}⁻¹)⁻¹, which is not conjugate to any p-adic power of the cusp.