The ℤ_p-bilinear graded bracket of a pro-p group

Let G be a pro-p group and λ_n the lower q-series of G, for any q. Each graded piece λ_n / λ_{n+1} is an abelian pro-p group, hence carries a canonical ℤ_p-module structure. Taking a p-adic power in either argument of a commutator acts on its class by the same p-adic exponent, so the graded bracket is ℤ_p-bilinear.

Main definitions

• TauCeti.IsProP.gradedPieceModule: the canonical ℤ_p-module structure on a graded piece.
• TauCeti.IsProP.gradedPieceModule_def: its identification with the canonical module on the underlying abelian pro-p quotient.

Main results

• TauCeti.IsProP.gradedMk_padicPow, TauCeti.IsProP.gradedMkZero_padicPow: a p-adic power becomes scalar multiplication on a graded piece.
• TauCeti.IsProP.mk_commutatorElement_padicPow_left, TauCeti.IsProP.mk_commutatorElement_padicPow_right: modulo λ_{j+k+2}, a p-adic power in either input of a commutator is the same power of the commutator.
• TauCeti.IsProP.gradedBracket_padicPow_left, TauCeti.IsProP.gradedBracket_padicPow_right: the same statements for classes in the graded pieces.
• TauCeti.IsProP.gradedBracket_smul_left, TauCeti.IsProP.gradedBracket_smul_right: the graded bracket is ℤ_p-linear in each variable.
• TauCeti.IsProP.gradedBracket_gradedMkZero_padicPow_neg_add: the brackets [a^{-u}, b] and [a, b^u] of degree-zero classes cancel.
• TauCeti.IsProP.gradedMk_commutatorElement_inv_conj_padicPow_inv: the commutator of the inverse of a conjugated p-adic power c⁻¹ y ^ u c with x⁻¹ has class u times the graded bracket of the classes of y and x.

References

• M. Lazard, Sur les groupes nilpotents et les anneaux de Lie, Ann. Sci. École Norm. Sup. 71 (1954).

@[instance_reducible]

noncomputable def TauCeti.IsProP.gradedPieceModule {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (q n : ℕ) : Module ℤ_[p] (gradedPiece q G n)

The canonical ℤ_p-module structure on a graded piece of the lower q-series of a pro-p group. It is the module structure on the abelian pro-p quotient λ_n / λ_{n+1}.

Equations

• hG.gradedPieceModule q n = ⋯.module

theorem TauCeti.IsProP.gradedPieceModule_def {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (q n : ℕ) : hG.gradedPieceModule q n = let R := pLowerCentralSeries q G n; let N := (pLowerCentralSeries q G (n + 1)).subgroupOf R; ⋯.module

The graded-piece module is the canonical module on its underlying abelian pro-p quotient.

@[simp]

theorem TauCeti.IsProP.gradedMk_padicPow {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) {q n : ℕ} (x : ↥(pLowerCentralSeries q G n)) (u : ℤ_[p]) : gradedMk q G n ⟨hG.padicPow (↑x) u, ⋯⟩ = u • gradedMk q G n x

In a pro-p group, the class of a p-adic power in a graded piece of the lower q-series is the corresponding ℤ_p-scalar multiple.

@[simp]

theorem TauCeti.IsProP.gradedMkZero_padicPow {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (q : ℕ) (x : G) (u : ℤ_[p]) : gradedMkZero q G (hG.padicPow x u) = u • gradedMkZero q G x

In a pro-p group, the degree-zero class of a p-adic power is the corresponding ℤ_p-scalar multiple.

theorem TauCeti.IsProP.mk_commutatorElement_padicPow_left {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) {q j k : ℕ} (x : ↥(pLowerCentralSeries q G j)) (y : ↥(pLowerCentralSeries q G k)) (u : ℤ_[p]) : ↑⁅hG.padicPow (↑x) u, ↑y⁆ = ↑(hG.padicPow ⁅↑x, ↑y⁆ u)

Modulo λ_{j+k+2}, taking a p-adic power in the left input of a commutator is the same as taking that power of the commutator.

theorem TauCeti.IsProP.mk_commutatorElement_padicPow_right {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) {q j k : ℕ} (x : ↥(pLowerCentralSeries q G j)) (y : ↥(pLowerCentralSeries q G k)) (u : ℤ_[p]) : ↑⁅↑x, hG.padicPow (↑y) u⁆ = ↑(hG.padicPow ⁅↑x, ↑y⁆ u)

Modulo λ_{j+k+2}, taking a p-adic power in the right input of a commutator is the same as taking that power of the commutator.

theorem TauCeti.IsProP.gradedBracket_padicPow_left {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) {q j k : ℕ} (x : ↥(pLowerCentralSeries q G j)) (y : ↥(pLowerCentralSeries q G k)) (u : ℤ_[p]) : ((gradedBracket q G j k) (gradedMk q G j ⟨hG.padicPow (↑x) u, ⋯⟩)) (gradedMk q G k y) = gradedMk q G (j + k + 1) ⟨hG.padicPow ⁅↑x, ↑y⁆ u, ⋯⟩

Taking a p-adic power in the first argument of the graded bracket takes the same power of the bracket class. This is ℤ_p-linearity in the first variable on representatives.

theorem TauCeti.IsProP.gradedBracket_padicPow_right {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) {q j k : ℕ} (x : ↥(pLowerCentralSeries q G j)) (y : ↥(pLowerCentralSeries q G k)) (u : ℤ_[p]) : ((gradedBracket q G j k) (gradedMk q G j x)) (gradedMk q G k ⟨hG.padicPow (↑y) u, ⋯⟩) = gradedMk q G (j + k + 1) ⟨hG.padicPow ⁅↑x, ↑y⁆ u, ⋯⟩

Taking a p-adic power in the second argument of the graded bracket takes the same power of the bracket class. This is ℤ_p-linearity in the second variable on representatives.

theorem TauCeti.IsProP.gradedBracket_smul_left {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) {q j k : ℕ} (u : ℤ_[p]) (x : gradedPiece q G j) (y : gradedPiece q G k) : ((gradedBracket q G j k) (u • x)) y = u • ((gradedBracket q G j k) x) y

The graded bracket of a pro-p group is ℤ_p-linear in its first argument.

theorem TauCeti.IsProP.gradedBracket_smul_right {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) {q j k : ℕ} (u : ℤ_[p]) (x : gradedPiece q G j) (y : gradedPiece q G k) : ((gradedBracket q G j k) x) (u • y) = u • ((gradedBracket q G j k) x) y

The graded bracket of a pro-p group is ℤ_p-linear in its second argument.

theorem TauCeti.IsProP.gradedBracket_gradedMkZero_padicPow_neg_add {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (q : ℕ) (a b : G) (u : ℤ_[p]) : ((gradedBracket q G 0 0) (gradedMkZero q G (hG.padicPow a (-u)))) (gradedMkZero q G b) + ((gradedBracket q G 0 0) (gradedMkZero q G a)) (gradedMkZero q G (hG.padicPow b u)) = 0

The brackets [a^{-u}, b] and [a, b^u] of degree-zero classes cancel: both are the p-adic power, with opposite exponents, of the class of the commutator ⁅a, b⁆.

theorem TauCeti.IsProP.gradedMk_commutatorElement_inv_conj_padicPow_inv {p : ℕ} [Fact (Nat.Prime p)] {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) {q m : ℕ} (y c : G) (x : ↥(pLowerCentralSeries q G m)) (u : ℤ_[p]) : gradedMk q G (0 + m + 1) ⟨⁅(c⁻¹ * hG.padicPow y u * c)⁻¹, ↑x⁻¹⁆, ⋯⟩ = u • ((gradedBracket q G 0 m) (gradedMkZero q G y)) (gradedMk q G m x)

The class of the commutator of the inverse of a conjugated p-adic power c⁻¹ y ^ u c with the inverse of x ∈ λ_m is u times the graded bracket of the classes of y and x.