The peripheral automorphism group and its exponent character

The continuous automorphisms preserving every peripheral conjugacy class up to a common unit power form a subgroup peripheralAut. This construction applies to any finite family in a pro-p group, including its cusp. Composition multiplies the exponents and inversion inverts them.

For a marked free pro-p group of positive rank, the exponent is uniquely determined and defines the homomorphism exponent to ℤ_[p]ˣ. The peripheral-power theorem makes this character surjective. Its kernel consists precisely of the automorphisms preserving each peripheral conjugacy class without a power; in particular, it contains the inner automorphisms. This character is the algebraic input to studying peripheral automorphisms as a topological group and splitting their exponent over principal units.

Main results

• IsPeripheralAut.mul, IsPeripheralAut.inv: the laws for peripheral exponents.
• mem_peripheralAut_iff: membership is the existence of a peripheral exponent.
• peripheralAut_le_peripheralPermAut: peripheral automorphisms are peripheral up to the trivial permutation.
• exponent_eq_iff: the exponent character is characterized by the peripheral predicate.
• exponent_surjective: every unit occurs as an exponent.
• mem_ker_exponent_iff: the kernel is the exponent-one part.
• exponent_conj: inner automorphisms have exponent one.
• permData_inclusion, permData_fst_eq_one_iff: in rank at least two, a peripheral automorphism has permutation data (1, exponent φ), and the trivial permutation characterizes peripheralAut inside peripheralPermAut.

References

• Y. Ihara, "Braids, Galois groups, and some arithmetic functions", Proc. ICM Kyoto 1990, 99–120, for peripheral automorphisms of free pro-p groups and their common exponent.

theorem TauCeti.Peripheral.IsPeripheralAut.mul {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 v : ℤ_[p]ˣ} {φ ψ : ContinuousAut F} (hφ : IsPeripheralAut hF x u φ) (hψ : IsPeripheralAut hF x v ψ) : IsPeripheralAut hF x (u * v) (φ * ψ)

Composition of peripheral automorphisms multiplies their exponents.

theorem TauCeti.Peripheral.IsPeripheralAut.inv {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} (hφ : IsPeripheralAut hF x u φ) : IsPeripheralAut hF x u⁻¹ φ⁻¹

The inverse of a peripheral automorphism has inverse exponent.

def TauCeti.Peripheral.peripheralAut {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) : Subgroup (ContinuousAut F)

The continuous automorphisms peripheral for x with some common unit exponent.

@[simp]

theorem TauCeti.Peripheral.mem_peripheralAut_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) (φ : ContinuousAut F) : φ ∈ peripheralAut hF x ↔ ∃ (u : ℤ_[p]ˣ), IsPeripheralAut hF x u φ

Membership in the peripheral automorphism group means admitting a unit exponent.

theorem TauCeti.Peripheral.range_conj_le_peripheralAut {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) : ContinuousAut.conj.range ≤ peripheralAut hF x

Every inner automorphism belongs to the peripheral automorphism group.

theorem TauCeti.Peripheral.peripheralAut_le_peripheralPermAut {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) : peripheralAut hF x ≤ peripheralPermAut hF x

Peripheral automorphisms are peripheral up to the trivial permutation.

def TauCeti.Peripheral.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) : F →* ↥(peripheralAut hF x)

Inner automorphisms viewed as peripheral automorphisms.

@[simp]

theorem TauCeti.Peripheral.coe_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) : ↑((conj hF x) g) = ContinuousAut.conj g

noncomputable def TauCeti.Peripheral.exponent {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) : ↥(peripheralAut hF (basis e)) →* ℤ_[p]ˣ

The unique common unit exponent of a peripheral automorphism of a marked free pro-p group of positive rank.

theorem TauCeti.Peripheral.isPeripheralAut_exponent {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) (φ : ↥(peripheralAut hF (basis e))) : IsPeripheralAut hF (basis e) ((exponent hF e hr) φ) ↑φ

The exponent character supplies a peripheral exponent for its argument.

@[simp]

theorem TauCeti.Peripheral.exponent_eq_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)) (hr : 0 < r) (φ : ↥(peripheralAut hF (basis e))) (u : ℤ_[p]ˣ) : (exponent hF e hr) φ = u ↔ IsPeripheralAut hF (basis e) u ↑φ

The exponent of a peripheral automorphism is u exactly when it is peripheral of exponent u.

theorem TauCeti.Peripheral.exponent_surjective {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) : Function.Surjective ⇑(exponent hF e hr)

Every unit of ℤ_[p] is an exponent of a peripheral automorphism.

theorem TauCeti.Peripheral.mem_ker_exponent_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)) (hr : 0 < r) (φ : ↥(peripheralAut hF (basis e))) : φ ∈ (exponent hF e hr).ker ↔ IsPeripheralAut hF (basis e) 1 ↑φ

The kernel consists exactly of the automorphisms preserving all peripheral conjugacy classes with exponent one.

@[simp]

theorem TauCeti.Peripheral.exponent_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) (e : F ≃ₜ* freeProP p (Fin r)) (hr : 0 < r) (g : F) : (exponent hF e hr) ((conj hF (basis e)) g) = 1

Inner automorphisms have exponent one.

@[simp]

theorem TauCeti.Peripheral.permData_inclusion {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 : 2 ≤ r) (φ : ↥(peripheralAut hF (basis e))) : (permData hF e hr) ((Subgroup.inclusion ⋯) φ) = (1, (exponent hF e ⋯) φ)

A peripheral automorphism has the trivial permutation, and its exponent, as permutation data.

theorem TauCeti.Peripheral.permData_fst_eq_one_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)) (hr : 2 ≤ r) (φ : ↥(peripheralPermAut hF (basis e))) : ((permData hF e hr) φ).1 = 1 ↔ ↑φ ∈ peripheralAut hF (basis e)

The permutation of a permutation-peripheral automorphism is trivial exactly when the automorphism is peripheral.