The peripheral automorphism group as a profinite group

Let F be a topologically finitely generated pro-p group, so that the group ContinuousAut F of its continuous automorphisms is profinite for the congruence topology. For a finite family x : Fin r → F, the peripheral graph is the set of pairs (φ, u) of a continuous automorphism and a p-adic unit such that φ is peripheral of exponent u for x. Each of the r + 1 defining conditions IsConj (y ^ u) (φ y), for y in the peripheral tuple of x, pulls back the closed conjugacy relation of F along the jointly continuous map (φ, u) ↦ (y ^ u, φ y), so the graph is closed in ContinuousAut F × ℤ_[p]ˣ.

The group peripheralAut hF x of peripheral automorphisms is the projection of the graph to the first factor. Since ℤ_[p]ˣ is compact, that projection is a closed map, so peripheralAut hF x is a closed subgroup of the profinite group ContinuousAut F, hence a profinite group itself. This is the topological input for taking profinite and p-adic powers of peripheral automorphisms.

For the basis of a free pro-p group of positive rank the exponent character exponent hF e hr : peripheralAut hF (basis e) →* ℤ_[p]ˣ has the peripheral graph as its graph, so it is continuous by the closed graph theorem for maps into a compact space.

Main results

• TauCeti.Peripheral.isClosed_peripheralGraph: the pairs (φ, u) with IsPeripheralAut hF x u φ form a closed subset of ContinuousAut F × ℤ_[p]ˣ.
• TauCeti.Peripheral.isClosed_peripheralAut: peripheralAut hF x is closed in ContinuousAut F.
• TauCeti.Peripheral.compactSpace_peripheralAut, TauCeti.Peripheral.totallyDisconnectedSpace_peripheralAut: peripheralAut hF x is a profinite group; for the basis of a marked free pro-p group these are instances.
• TauCeti.Peripheral.graph_exponent: the graph of the exponent character is the peripheral graph of the basis.
• TauCeti.Peripheral.continuous_exponent: the exponent character is continuous.

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.isClosed_peripheralGraph {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) (hfg : IsTopologicallyFinitelyGenerated F) : IsClosed {q : ContinuousAut F × ℤ_[p]ˣ | IsPeripheralAut hF x q.2 q.1}

The peripheral graph is closed. For a topologically finitely generated pro-p group F and a family x, the pairs (φ, u) of a continuous automorphism and a p-adic unit with IsPeripheralAut hF x u φ form a closed subset of ContinuousAut F × ℤ_[p]ˣ.

theorem TauCeti.Peripheral.isClosed_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) (hfg : IsTopologicallyFinitelyGenerated F) : IsClosed ↑(peripheralAut hF x)

The peripheral automorphisms form a closed subgroup of ContinuousAut F for the congruence topology, when F is topologically finitely generated.

theorem TauCeti.Peripheral.compactSpace_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) (hfg : IsTopologicallyFinitelyGenerated F) : CompactSpace ↥(peripheralAut hF x)

The peripheral automorphism group of a topologically finitely generated pro-p group is compact.

theorem TauCeti.Peripheral.totallyDisconnectedSpace_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) (hfg : IsTopologicallyFinitelyGenerated F) : TotallyDisconnectedSpace ↥(peripheralAut hF x)

The peripheral automorphism group of a topologically finitely generated pro-p group is totally disconnected.

instance TauCeti.Peripheral.compactSpace_peripheralAut_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)) : CompactSpace ↥(peripheralAut hF (basis e))

The peripheral automorphism group of a marked free pro-p group of finite rank is compact.

instance TauCeti.Peripheral.totallyDisconnectedSpace_peripheralAut_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)) : TotallyDisconnectedSpace ↥(peripheralAut hF (basis e))

The peripheral automorphism group of a marked free pro-p group of finite rank is totally disconnected.

theorem TauCeti.Peripheral.graph_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) : Function.graph ⇑(exponent hF e hr) = (fun (q : ↥(peripheralAut hF (basis e)) × ℤ_[p]ˣ) => (↑q.1, q.2)) ⁻¹' {q : ContinuousAut F × ℤ_[p]ˣ | IsPeripheralAut hF (basis e) q.2 q.1}

The graph of the exponent character is the peripheral graph of the basis, pulled back to the peripheral automorphism group.

theorem TauCeti.Peripheral.continuous_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) : Continuous ⇑(exponent hF e hr)

The exponent character is continuous. Its graph is closed, being the peripheral graph of the basis, and its target ℤ_[p]ˣ is compact.