A non-unit obstruction to the peripheral product identity

For the basis of a free pro-2 group of rank two, no conjugators make the peripheral defect of exponent 2 belong to the second closed lower-central-series term. In particular, the peripheral product identity cannot be extended from unit exponents to all 2-adic integers. This is an obstruction already in the class-two quotient, rather than only to an exact identity.

The detecting group is the Heisenberg group over ℤ/2: the two standard generators have square 1, but their product has nontrivial central square. Every continuous homomorphism to this group kills the second closed lower-central-series term. The detection construction follows the use of finite Heisenberg groups in TauCeti.Peripheral.not_isPeripheralAut_of_apply_basis_eq_inv.

Main results

• TauCeti.Peripheral.level_two_eq_empty: the second peripheral level at exponent 2 is empty.
• TauCeti.Peripheral.not_exists_peripheral_identity_two: even the normalized product with two conjugators cannot be trivial modulo the second closed lower-central-series term.

@[simp]

theorem TauCeti.Peripheral.level_two_eq_empty {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP 2 F) (e : F ≃ₜ* freeProP 2 (Fin 2)) : level hF (basis e) 2 2 = ∅

For a rank-two free pro-2 group, the second peripheral level at the non-unit exponent 2 is empty, even without normalizing the first conjugator.

theorem TauCeti.Peripheral.not_exists_peripheral_identity_two {F : Type u_1} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F] [TotallyDisconnectedSpace F] (hF : IsProP 2 F) (e : F ≃ₜ* freeProP 2 (Fin 2)) : ¬∃ (c : F) (d : F), hF.padicPow (basis e 0) 2 * (c⁻¹ * hF.padicPow (basis e 1) 2 * c) * (d⁻¹ * hF.padicPow (cusp (basis e)) 2 * d) ∈ closedLowerCentralSeries F 2

At exponent 2, no normalized peripheral product in a rank-two free pro-2 group is trivial even modulo the second closed lower-central-series term.