Documentation

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

The peripheral product identity #

Let F be a free pro-p group of rank r with basis x : Fin r → F and cusp z = (∏ i, x i)⁻¹. For every unit u ∈ ℤ_pˣ there are conjugators c : Fin r → F and d in F, with c 0 = 1 when 0 < r, such that

(∏ i, (c i)⁻¹ * x i ^ u * c i) * (d⁻¹ * z ^ u * d) = 1,

where ^ u is the p-adic power; that is, the peripheral defect of (c, d) is trivial. The identity is what makes the continuous endomorphism sending x i to (c i)⁻¹ * x i ^ u * c i carry the cusp z to the conjugate d⁻¹ * z ^ u * d of its u-th power.

The proof has two separate steps. Lifting through the closed lower central series, using the correction step of TauCeti.Peripheral.exists_mem_level_succ, gives normalized conjugators at every peripheral level; this is the only place where u must be a unit. Compactness of the space of conjugators then gives one normalized pair lying in every level at once, and its defect is trivial because the closed lower central series of a pro-p group has trivial intersection.

Main results #

References #

theorem TauCeti.Peripheral.exists_mem_level {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)) (u : ℤ_[p]ˣ) (n : ℕ) :
∃ (c : Fin r → F) (d : F), (∀ (h0 : 0 < r), c ⟨0, h0⟩ = 1) ∧ (c, d) ∈ level hF (basis e) (↑u) n

Solutions at every level. For a unit u, every peripheral level of the basis x = basis e of a free pro-p group contains a pair of conjugators whose conjugator at the first basis element is trivial when the rank is positive.

theorem TauCeti.Peripheral.exists_defect_eq_one_of_forall_exists_mem_level {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]) (h : ∀ (n : ℕ), ∃ (c : Fin r → F) (d : F), (∀ (h0 : 0 < r), c ⟨0, h0⟩ = 1) ∧ (c, d) ∈ level hF x u n) :
∃ (c : Fin r → F) (d : F), (∀ (h0 : 0 < r), c ⟨0, h0⟩ = 1) ∧ defect hF x u c d = 1

The compactness step. If every peripheral level of a family x in a pro-p group contains a pair of conjugators whose conjugator at the first basis element is trivial when the rank is positive, then some such pair has trivial defect. The exponent u need not be a unit.

theorem TauCeti.Peripheral.exists_defect_eq_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) (e : F ≃ₜ* freeProP p (Fin r)) (u : ℤ_[p]ˣ) :
∃ (c : Fin r → F) (d : F), (∀ (h0 : 0 < r), c ⟨0, h0⟩ = 1) ∧ defect hF (basis e) (↑u) c d = 1

The peripheral product identity. For every unit u ∈ ℤ_pˣ, the basis x = basis e of a free pro-p group admits conjugators c on the basis, with c 0 = 1 in positive rank, and d on the cusp such that (∏_i (c i)⁻¹ * x i ^ u * c i) * (d⁻¹ * cusp x ^ u * d) = 1, the product taken in order and ^ u the p-adic power.