Peripheral systems of free pro-p groups

Let F be a group with a marked topological isomorphism e : F ≃ₜ* freeProP p (Fin r) to the free pro-p group of rank r. The basis x_0, …, x_{r-1} of F is the image of the canonical generators under e.symm, and the cusp is z := (x_0 ⋯ x_{r-1})⁻¹, the inverse of the ordered product of the basis, so that x_0 ⋯ x_{r-1} · z = 1. The r + 1 elements x_0, …, x_{r-1}, z form the peripheral tuple; for r = 2 their conjugacy classes are the classes of the loops around 0, 1 and ∞ in the pro-p fundamental group of the thrice-punctured line.

A continuous automorphism φ of a pro-p group is peripheral of exponent u ∈ ℤ_pˣ for a family x when it carries every element y of the peripheral tuple of x to a conjugate of the p-adic power y ^ u. The predicate is stated with IsConj rather than with named conjugators, so that it is a property of φ alone.

Inner automorphisms are peripheral of exponent one, and for the basis of a free pro-p group of positive rank the exponent of a peripheral automorphism is determined by the automorphism: it is the scalar by which φ acts on the class of x_0 in the abelianization ℤ_p ^ r.

Main definitions

• TauCeti.Peripheral.basis: the basis i ↦ e.symm (freeProP.of i) transported along a marked isomorphism e to the standard free pro-p group.
• TauCeti.Peripheral.cusp: the inverse ((List.ofFn x).prod)⁻¹ of the ordered product of a family x.
• TauCeti.Peripheral.peripheralTuple: the family x_0, …, x_{r-1}, cusp x indexed by Fin (r + 1).
• TauCeti.Peripheral.IsPeripheralAut: a continuous automorphism carries each element of the peripheral tuple to a conjugate of its p-adic power by a unit u.

Main results

• TauCeti.Peripheral.topologicalClosure_closure_range_basis: the basis generates F topologically.
• TauCeti.Peripheral.topologicalClosure_closure_range_peripheralTuple_comp_succ: so does the peripheral tuple of the basis without its first entry.
• TauCeti.Peripheral.hom_ext_basis: continuous homomorphisms out of F into a Hausdorff monoid that agree on the basis are equal.
• TauCeti.Peripheral.prod_mul_cusp, TauCeti.Peripheral.prod_ofFn_peripheralTuple: the defining relation x_0 ⋯ x_{r-1} · cusp x = 1, and the ordered product of the peripheral tuple is 1.
• TauCeti.Peripheral.exponentSum_cusp_basis, TauCeti.Peripheral.toAdd_exponentSum_peripheralTuple: in the abelianization ℤ_p ^ r the peripheral tuple of the basis has the classes e_0, …, e_{r-1} and -(e_0 + ⋯ + e_{r-1}).
• TauCeti.Peripheral.isPeripheralAut_of_apply_eq_conj: an automorphism carrying each x i and the cusp to explicit conjugates of their u-th powers is peripheral of exponent u.
• TauCeti.Peripheral.isPeripheralAut_conj: inner automorphisms are peripheral of exponent one.
• TauCeti.Peripheral.IsPeripheralAut.exponent_unique: in positive rank, the exponent of a peripheral automorphism with respect to the basis is unique.

References

• Y. Ihara, "Braids, Galois groups, and some arithmetic functions", Proc. ICM Kyoto 1990, 99–120, for peripheral automorphisms x ↦ x ^ λ, y ↦ f⁻¹ y ^ λ f of free pro-p groups of rank two and the role of the third conjugacy class.

noncomputable def TauCeti.Peripheral.basis {p r : ℕ} {F : Type u_1} [Group F] [TopologicalSpace F] (e : F ≃ₜ* freeProP p (Fin r)) : Fin r → F

The basis of F transported from the standard free pro-p group along a marked isomorphism e: the preimages e.symm (freeProP.of i) of the canonical generators.

theorem TauCeti.Peripheral.basis_apply {p r : ℕ} {F : Type u_1} [Group F] [TopologicalSpace F] (e : F ≃ₜ* freeProP p (Fin r)) (i : Fin r) : basis e i = e.symm (freeProP.of i)

@[simp]

theorem TauCeti.Peripheral.map_basis {p r : ℕ} {F : Type u_1} [Group F] [TopologicalSpace F] (e : F ≃ₜ* freeProP p (Fin r)) (i : Fin r) : e (basis e i) = freeProP.of i

theorem TauCeti.Peripheral.topologicalClosure_closure_range_basis {p r : ℕ} {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] (e : F ≃ₜ* freeProP p (Fin r)) : (Subgroup.closure (Set.range (basis e))).topologicalClosure = ⊤

The basis generates F topologically.

theorem TauCeti.Peripheral.hom_ext_basis {p r : ℕ} {F : Type u_1} [Group F] [TopologicalSpace F] {M : Type u_2} [Monoid M] [TopologicalSpace M] [T2Space M] (e : F ≃ₜ* freeProP p (Fin r)) {f g : F →ₜ* M} (h : ∀ (i : Fin r), f (basis e i) = g (basis e i)) : f = g

Two continuous homomorphisms out of F into a Hausdorff monoid that agree on the basis are equal.

def TauCeti.Peripheral.cusp {G : Type u_1} [Group G] {r : ℕ} (x : Fin r → G) : G

The cusp of a family x : Fin r → G: the inverse (x_0 ⋯ x_{r-1})⁻¹ of the product of the family in order. The product is a List.prod, since G need not be commutative.

theorem TauCeti.Peripheral.cusp_def {G : Type u_1} [Group G] {r : ℕ} (x : Fin r → G) : cusp x = (List.ofFn x).prod⁻¹

@[simp]

theorem TauCeti.Peripheral.inv_cusp {G : Type u_1} [Group G] {r : ℕ} (x : Fin r → G) : (cusp x)⁻¹ = (List.ofFn x).prod

@[simp]

theorem TauCeti.Peripheral.prod_mul_cusp {G : Type u_1} [Group G] {r : ℕ} (x : Fin r → G) : (List.ofFn x).prod * cusp x = 1

The defining relation of the cusp: x_0 ⋯ x_{r-1} · cusp x = 1.

@[simp]

theorem TauCeti.Peripheral.cusp_fin_one {G : Type u_1} [Group G] (x : Fin 1 → G) : cusp x = (x 0)⁻¹

The cusp of a one-element family is the inverse of its element.

@[simp]

theorem TauCeti.Peripheral.map_cusp {G : Type u_1} {H : Type u_2} [Group G] [Group H] {r : ℕ} {M : Type u_3} [FunLike M G H] [MonoidHomClass M G H] (f : M) (x : Fin r → G) : f (cusp x) = cusp (⇑f ∘ x)

Homomorphisms carry the cusp of a family to the cusp of its image.

def TauCeti.Peripheral.peripheralTuple {G : Type u_1} [Group G] {r : ℕ} (x : Fin r → G) : Fin (r + 1) → G

The peripheral tuple of a family x : Fin r → G: the family x_0, …, x_{r-1}, cusp x, indexed by Fin (r + 1).

@[simp]

theorem TauCeti.Peripheral.peripheralTuple_castSucc {G : Type u_1} [Group G] {r : ℕ} (x : Fin r → G) (i : Fin r) : peripheralTuple x i.castSucc = x i

@[simp]

theorem TauCeti.Peripheral.peripheralTuple_last {G : Type u_1} [Group G] {r : ℕ} (x : Fin r → G) : peripheralTuple x (Fin.last r) = cusp x

theorem TauCeti.Peripheral.prod_ofFn_peripheralTuple {G : Type u_1} [Group G] {r : ℕ} (x : Fin r → G) : (List.ofFn (peripheralTuple x)).prod = 1

The ordered product of the peripheral tuple is 1.

@[simp]

theorem TauCeti.Peripheral.map_peripheralTuple {G : Type u_1} {H : Type u_2} [Group G] [Group H] {r : ℕ} {M : Type u_3} [FunLike M G H] [MonoidHomClass M G H] (f : M) (x : Fin r → G) (i : Fin (r + 1)) : f (peripheralTuple x i) = peripheralTuple (⇑f ∘ x) i

Homomorphisms carry the peripheral tuple of a family to the peripheral tuple of its image.

theorem TauCeti.Peripheral.topologicalClosure_closure_range_peripheralTuple_comp_succ {p r : ℕ} {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] (e : F ≃ₜ* freeProP p (Fin r)) : (Subgroup.closure (Set.range (peripheralTuple (basis e) ∘ Fin.succ))).topologicalClosure = ⊤

The peripheral tuple of the basis without its first entry still generates F topologically: the first entry is recovered from the others through the relation prod_mul_cusp.

theorem TauCeti.Peripheral.exponentSum_cusp_basis {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F] [TopologicalSpace F] (e : F ≃ₜ* freeProP p (Fin r)) : (freeProP.exponentSum p (Fin r)) (e (cusp (basis e))) = Multiplicative.ofAdd (-1)

The exponent vector of the cusp of the basis is -(e_0 + ⋯ + e_{r-1}).

theorem TauCeti.Peripheral.toAdd_exponentSum_peripheralTuple {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F] [TopologicalSpace F] (e : F ≃ₜ* freeProP p (Fin r)) (i : Fin (r + 1)) : Multiplicative.toAdd ((freeProP.exponentSum p (Fin r)) (e (peripheralTuple (basis e) i))) = Fin.lastCases (motive := fun (x : Fin (r + 1)) => Fin r → ℤ_[p]) (-1) (fun (j : Fin r) => Pi.single j 1) i

The exponent vectors of the peripheral tuple of the basis are the coordinate vectors e_0, …, e_{r-1} and, at the cusp, minus their sum.

def TauCeti.Peripheral.IsPeripheralAut {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (x : Fin r → F) (u : ℤ_[p]ˣ) (φ : ContinuousAut F) : Prop

A continuous automorphism φ of a pro-p group is peripheral of exponent u for a family x when it carries every element y of the peripheral tuple x_0, …, x_{r-1}, cusp x to a conjugate of the p-adic power y ^ u.

@[simp]

theorem TauCeti.Peripheral.isPeripheralAut_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) (x : Fin r → F) (u : ℤ_[p]ˣ) (φ : ContinuousAut F) : IsPeripheralAut hF x u φ ↔ (∀ (i : Fin r), IsConj (hF.padicPow (x i) ↑u) (φ (x i))) ∧ IsConj (hF.padicPow (cusp x) ↑u) (φ (cusp x))

An automorphism is peripheral of exponent u exactly when it carries each x_i and the cusp to conjugates of their u-th powers.

theorem TauCeti.Peripheral.isPeripheralAut_of_apply_eq_conj {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) {x : Fin r → F} {u : ℤ_[p]ˣ} {φ : ContinuousAut F} {c : Fin r → F} {d : F} (hc : ∀ (i : Fin r), φ (x i) = (c i)⁻¹ * hF.padicPow (x i) ↑u * c i) (hd : φ (cusp x) = d⁻¹ * hF.padicPow (cusp x) ↑u * d) : IsPeripheralAut hF x u φ

An automorphism carrying each x i to (c i)⁻¹ * x i ^ u * c i and the cusp z to d⁻¹ * z ^ u * d is peripheral of exponent u for x.

theorem TauCeti.Peripheral.isPeripheralAut_conj {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (x : Fin r → F) (g : F) : IsPeripheralAut hF x 1 (ContinuousAut.conj g)

Inner automorphisms are peripheral of exponent one.

theorem TauCeti.Peripheral.isPeripheralAut_one {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP p F) (x : Fin r → F) : IsPeripheralAut hF x 1 1

The identity is peripheral of exponent one.

theorem TauCeti.Peripheral.IsPeripheralAut.exponent_unique {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)} (hr : 0 < r) {u v : ℤ_[p]ˣ} {φ : ContinuousAut F} (hu : IsPeripheralAut hF (basis e) u φ) (hv : IsPeripheralAut hF (basis e) v φ) : u = v

The exponent of a peripheral automorphism is determined. For a free pro-p group of positive rank with its basis, an automorphism peripheral of exponents u and v has u = v. The exponent is the scalar by which the automorphism acts on the class of x_0 in the abelianization ℤ_p ^ r.