Power and bracket in degree zero of the lower p-series

Away from degree zero the power operator π on the graded pieces of the lower p-series commutes with the bracket (TauCeti.gradedPow_gradedBracket_left, TauCeti.gradedPow_gradedBracket_right). This file treats the remaining case, where the powered input has degree zero. The binomial collection formula for ⁅a ^ n, b⁆ and ⁅a, b ^ n⁆ produces a correction term: for x of degree zero,

[π x, y] = π [x, y] + (p choose 2) • [x, [x, y]],

and symmetrically [x, π y] = π [x, y] + (p choose 2) • [y, [x, y]] for y of degree zero. For odd p the correction vanishes, so π commutes with the bracket in every degree; for p = 2 it is the iterated bracket [[x, y], x], resp. [[x, y], y]. These are the counterparts for the bracket of the degree-zero additivity defect π (x + y) = π x + π y + (p choose 2) • [y, x] (TauCeti.gradedPow_add_zero), and together with the results away from degree zero they describe π on the whole graded Lie algebra. The file also records that a degree-zero class brackets trivially with its iterated p-powers, [π^j x, x] = 0 (TauCeti.gradedBracket_gradedPowIter_self).

Main results

• TauCeti.mk_commutatorElement_pow_left, TauCeti.mk_commutatorElement_pow_right: the collection formulas for ⁅a ^ n, b⁆ and ⁅a, b ^ n⁆ modulo λ_{k+3} when the unpowered input lies in λ_k.
• TauCeti.gradedBracket_gradedPow_zero_left, TauCeti.gradedBracket_gradedPow_zero_right: the degree-zero corrections (p choose 2) • [x, [x, y]] and (p choose 2) • [y, [x, y]].
• TauCeti.gradedPow_gradedBracket_left_of_odd, TauCeti.gradedPow_gradedBracket_right_of_odd: for odd p, π [x, y] = [π x, y] = [x, π y] in every degree.
• TauCeti.gradedBracket_gradedPow_zero_left_of_two, TauCeti.gradedBracket_gradedPow_zero_right_of_two: for p = 2, [π x, y] = π [x, y] + [[x, y], x] and [x, π y] = π [x, y] + [[x, y], y].
• TauCeti.gradedPow_gradedBracket_left_zero, TauCeti.gradedPow_gradedBracket_left_zero_of_odd, TauCeti.gradedPow_gradedBracket_zero_zero: the identities for a bracket [x, y] with y of degree zero, where π [x, y] and [π x, y] have the same degree and no transport is needed.
• TauCeti.gradedBracket_gradedPowIter_self: [π^j x, x] = 0 for x of degree zero, the class of ⁅g ^ (p ^ j), g⁆ = 1.

References

• J. Labute, Classification of Demushkin groups, Canadian J. Math. 19 (1967), §1, Propositions 1 and 2.

theorem TauCeti.mk_commutatorElement_pow_left {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {a b : G} (hb : b ∈ pLowerCentralSeries p G k) (n : ℕ) : ↑⁅a ^ n, b⁆ = ↑(⁅a, b⁆ ^ n * ⁅a, ⁅a, b⁆⁆ ^ n.choose 2)

Collection of a powered commutator modulo λ_{k+3}. The iterated commutator lies in λ_{k+2}, so its image is central and the binomial formula applies.

theorem TauCeti.mk_commutatorElement_pow_right {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {j : ℕ} {a b : G} (ha : a ∈ pLowerCentralSeries p G j) (n : ℕ) : ↑⁅a, b ^ n⁆ = ↑(⁅a, b⁆ ^ n * ⁅b, ⁅a, b⁆⁆ ^ n.choose 2)

Collection in the right input modulo λ_{j+3}. The correction involves ⁅b, ⁅a, b⁆⁆; reversing the outer commutator would change its sign.

theorem TauCeti.gradedBracket_gradedPow_zero_left {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} (x : gradedPiece p G 0) (y : gradedPiece p G k) : gradedCast p G ⋯ (((gradedBracket p G 1 k) (gradedPow p G 0 x)) y) = gradedPow p G (0 + k + 1) (((gradedBracket p G 0 k) x) y) + p.choose 2 • gradedCast p G ⋯ (((gradedBracket p G 0 (0 + k + 1)) x) (((gradedBracket p G 0 k) x) y))

The correction to [π x, y] = π [x, y] when x has degree zero is (p choose 2) • [x, [x, y]], transported to the degree of π [x, y].

theorem TauCeti.gradedBracket_gradedPow_zero_right {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {j : ℕ} (x : gradedPiece p G j) (y : gradedPiece p G 0) : gradedCast p G ⋯ (((gradedBracket p G j 1) x) (gradedPow p G 0 y)) = gradedPow p G (j + 0 + 1) (((gradedBracket p G j 0) x) y) + p.choose 2 • gradedCast p G ⋯ (((gradedBracket p G 0 (j + 0 + 1)) y) (((gradedBracket p G j 0) x) y))

The correction to [x, π y] = π [x, y] when y has degree zero is (p choose 2) • [y, [x, y]], with the inner bracket in this order.

theorem TauCeti.gradedPow_gradedBracket_left_of_odd {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hp : Odd p) {j k : ℕ} (x : gradedPiece p G j) (y : gradedPiece p G k) : gradedPow p G (j + k + 1) (((gradedBracket p G j k) x) y) = gradedCast p G ⋯ (((gradedBracket p G (j + 1) k) (gradedPow p G j x)) y)

For odd p, the power operator commutes with the bracket on the left in every degree, including degree zero. No primality assumption is needed.

theorem TauCeti.gradedPow_gradedBracket_right_of_odd {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hp : Odd p) {j k : ℕ} (x : gradedPiece p G j) (y : gradedPiece p G k) : gradedPow p G (j + k + 1) (((gradedBracket p G j k) x) y) = gradedCast p G ⋯ (((gradedBracket p G j (k + 1)) x) (gradedPow p G k y))

For odd p, the power operator commutes with the bracket on the right in every degree, including degree zero. No primality assumption is needed.

theorem TauCeti.gradedBracket_gradedPow_zero_left_of_two {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hp : p = 2) {k : ℕ} (x : gradedPiece p G 0) (y : gradedPiece p G k) : gradedCast p G ⋯ (((gradedBracket p G 1 k) (gradedPow p G 0 x)) y) = gradedPow p G (0 + k + 1) (((gradedBracket p G 0 k) x) y) + gradedCast p G ⋯ (((gradedBracket p G (0 + k + 1) 0) (((gradedBracket p G 0 k) x) y)) x)

For p = 2 and x of degree zero, [π x, y] = π [x, y] + [[x, y], x]. The last term has this orientation because every graded piece is killed by 2.

theorem TauCeti.gradedBracket_gradedPow_zero_right_of_two {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hp : p = 2) {j : ℕ} (x : gradedPiece p G j) (y : gradedPiece p G 0) : gradedCast p G ⋯ (((gradedBracket p G j 1) x) (gradedPow p G 0 y)) = gradedPow p G (j + 0 + 1) (((gradedBracket p G j 0) x) y) + gradedCast p G ⋯ (((gradedBracket p G (j + 0 + 1) 0) (((gradedBracket p G j 0) x) y)) y)

For p = 2 and y of degree zero, [x, π y] = π [x, y] + [[x, y], y]. The inner bracket retains the order [x, y].

Brackets with a degree-zero class, without transport of degrees

theorem TauCeti.gradedPow_gradedBracket_left_zero {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {j : ℕ} (hj : 1 ≤ j) (x : gradedPiece p G j) (y : gradedPiece p G 0) : gradedPow p G (j + 1) (((gradedBracket p G j 0) x) y) = ((gradedBracket p G (j + 1) 0) (gradedPow p G j x)) y

π against a bracket with a degree-zero class, away from degree zero: π [x, y] = [π x, y] for x ∈ gr_j(G) with j ≥ 1 and y ∈ gr_0(G). Both sides lie in gr_{j+2}(G), so no transport of degrees is needed.

theorem TauCeti.gradedPow_gradedBracket_left_zero_of_odd {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hp : Odd p) {j : ℕ} (x : gradedPiece p G j) (y : gradedPiece p G 0) : gradedPow p G (j + 1) (((gradedBracket p G j 0) x) y) = ((gradedBracket p G (j + 1) 0) (gradedPow p G j x)) y

For odd p, π [x, y] = [π x, y] for y of degree zero, in every degree of x.

theorem TauCeti.gradedPow_gradedBracket_zero_zero {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x y : gradedPiece p G 0) : gradedPow p G 1 (((gradedBracket p G 0 0) x) y) = ((gradedBracket p G 1 0) (gradedPow p G 0 x)) y + p.choose 2 • ((gradedBracket p G 1 0) (((gradedBracket p G 0 0) x) y)) x

π against a bracket of two degree-zero classes: π [x, y] = [π x, y] + (p choose 2) • [[x, y], x] in gr_2(G). For odd p the correction vanishes, and for p = 2 it is [[x, y], x].

Brackets with iterated p-powers

@[simp]

theorem TauCeti.gradedBracket_gradedPowIter_self {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (j : ℕ) (x : gradedPiece p G 0) : ((gradedBracket p G j 0) (gradedPowIter p G j x)) x = 0

A degree-zero class brackets trivially with its iterated p-powers: [π^j x, x] = 0, since it is the class of the commutator ⁅g ^ (p ^ j), g⁆ = 1.