Lifting peripheral product identities

For a family x in a pro-p group and an exponent u ∈ ℤ_p, the peripheral defect is the ordered product of chosen conjugates of the u-th powers of the entries of x and of its cusp. Its n-th level consists of the conjugators for which this product lies in the n-th term of the closed lower central series.

For the basis of a finite-rank free pro-p group, every pair of conjugators lies at level one. More importantly, a pair at any positive level can be corrected into one at the next level by multiplying its conjugators by elements one step lower in the central series. The correction at the first basis element is kept trivial. Iterating this result gives compatible approximate solutions to the peripheral product identity.

In rank at least two no term of the closed lower central series of a free pro-p group is trivial, so no single level reduces to the exact peripheral product identity merely because its term γ_n vanishes. Passing from these approximate solutions to an exact one uses all the levels at once, through compactness.

Main definitions

• TauCeti.Peripheral.defect: the ordered peripheral product for chosen conjugators.
• TauCeti.Peripheral.level: the conjugators whose defect lies in a specified closed lower-central-series term.

Main results

• TauCeti.Peripheral.forall_mem_level_iff: conjugators lie in every peripheral level exactly when their defect is trivial.
• TauCeti.Peripheral.level_one_eq_univ: every choice of conjugators has defect in γ₁.
• TauCeti.Peripheral.exists_mem_level_succ: a positive-level solution can be corrected to the next level while keeping the correction at the first basis element trivial.
• TauCeti.Peripheral.closedLowerCentralSeries_ne_bot: in rank at least two, no term of the closed lower central series is trivial.

noncomputable def TauCeti.Peripheral.defect {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]) (c : Fin r → F) (d : F) : F

The defect of conjugators c on a family x and d on its cusp: the ordered product of the corresponding conjugates of their u-th powers.

theorem TauCeti.Peripheral.defect_def {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]) (c : Fin r → F) (d : F) : defect hF x u c d = (List.ofFn fun (i : Fin r) => (c i)⁻¹ * hF.padicPow (x i) u * c i).prod * (d⁻¹ * hF.padicPow (cusp x) u * d)

The peripheral defect is the ordered product of the conjugated powers of the family followed by the conjugated power of its cusp.

theorem TauCeti.Peripheral.continuous_defect {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]) : Continuous fun (cd : (Fin r → F) × F) => defect hF x u cd.1 cd.2

The peripheral defect is continuous as a function of all its conjugators.

def TauCeti.Peripheral.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]) (n : ℕ) : Set ((Fin r → F) × F)

The n-th peripheral level is the set of conjugators whose defect lies in the n-th term of the closed lower central series.

@[simp]

theorem TauCeti.Peripheral.mem_level_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]) (n : ℕ) (cd : (Fin r → F) × F) : cd ∈ level hF x u n ↔ defect hF x u cd.1 cd.2 ∈ closedLowerCentralSeries F n

Membership in a peripheral level means exactly that the corresponding defect lies in the specified closed lower-central-series term.

theorem TauCeti.Peripheral.isClosed_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]) (n : ℕ) : IsClosed (level hF x u n)

Every peripheral level is closed.

theorem TauCeti.Peripheral.level_antitone {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]) : Antitone (level hF x u)

The peripheral levels form a decreasing family.

theorem TauCeti.Peripheral.forall_mem_level_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]) (cd : (Fin r → F) × F) : (∀ (n : ℕ), cd ∈ level hF x u n) ↔ defect hF x u cd.1 cd.2 = 1

A pair of conjugators lies in every peripheral level exactly when its defect is trivial: in a pro-p group the terms of the closed lower central series have trivial intersection.

@[simp]

theorem TauCeti.Peripheral.level_one_eq_univ {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]) : level hF x u 1 = Set.univ

Every choice of conjugators is in the first peripheral level. In the topological abelianization, conjugation disappears, p-adic powers become scalar multiplication, and the classes of the family and its cusp sum to zero.

theorem TauCeti.Peripheral.exists_mem_level_succ {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 : ℕ) (hn : 1 ≤ n) (c : Fin r → F) (d : F) (h : (c, d) ∈ level hF (basis e) (↑u) n) : ∃ (c' : Fin r → F) (d' : F), (∀ (i : Fin r), c' i ∈ closedLowerCentralSeries F (n - 1)) ∧ d' ∈ closedLowerCentralSeries F (n - 1) ∧ (∀ (h0 : 0 < r), c' ⟨0, h0⟩ = 1) ∧ (fun (i : Fin r) => c i * c' i, d * d') ∈ level hF (basis e) (↑u) (n + 1)

A pair of conjugators whose defect lies in γ_n, for positive n, can be corrected so that its defect lies in γ_{n+1}. The corrections lie in γ_{n-1}, and the correction at the first basis element is trivial. The unit hypothesis on u is used to rescale the required graded correction.

theorem TauCeti.Peripheral.closedLowerCentralSeries_ne_bot {p r : ℕ} [Fact (Nat.Prime p)] {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] (e : F ≃ₜ* freeProP p (Fin r)) (hr : 2 ≤ r) (n : ℕ) : closedLowerCentralSeries F n ≠ ⊥

The closed lower central series of a free pro-p group of rank at least two never vanishes. For a group F presented as free pro-p on r ≥ 2 generators, no term γ_n of its closed lower central series is trivial. So no level TauCeti.Peripheral.level reduces to the exact peripheral product identity merely because its term γ_n vanishes: the corrections of TauCeti.Peripheral.exists_mem_level_succ control the defect at each finite stage only modulo a nontrivial subgroup.