The graded pieces of the lower p-series

For a topological group G and p : ℕ, the lower p-series λ_k = TauCeti.pLowerCentralSeries p G k is a descending chain of closed normal subgroups with λ_kᵖ ≤ λ_{k+1} and ⁅λ_j, λ_k⁆ ≤ λ_{j+k+1}. This file studies its successive quotients

gr_k(G) = λ_k ⧸ λ_{k+1},

written additively as TauCeti.gradedPiece p G k. Each gr_k(G) is an abelian group killed by p, hence a ZMod p-module. The group commutator induces a biadditive bracket [·, ·] : gr_j(G) × gr_k(G) → gr_{j+k+1}(G), alternating and satisfying the Jacobi identity; the degree shifts by one because the series is 0-based. The p-th power induces the operator π : gr_k(G) → gr_{k+1}(G). Away from degree zero the operator π is additive and commutes with the bracket, because the correction terms of the Hall–Petrescu formula land in higher degree; in degree zero its defect of additivity is (p choose 2) • [y, x], which vanishes for odd p and is the bracket [x, y] for p = 2. A continuous homomorphism induces maps on the graded pieces that are compatible with the bracket and with π.

For a prime p, the graded pieces of a topologically finitely generated profinite group are finite; this is proved in TauCeti.Topology.Algebra.Group.Profinite.ProP.LowerCentralSeries.

Main definitions

• TauCeti.gradedPiece: the graded piece gr_k(G) = λ_k ⧸ λ_{k+1}, written additively, with its ZMod p-module structure.
• TauCeti.gradedMk: the class in gr_k(G) of an element of λ_k.
• TauCeti.gradedPieceInclusion: the injection of gr_k(G) into G ⧸ λ_{k+1}, an isomorphism in degree zero (TauCeti.gradedPieceZeroEquiv).
• TauCeti.gradedBracket: the bracket gr_j(G) →+ gr_k(G) →+ gr_{j+k+1}(G), and its ZMod p-bilinear form TauCeti.gradedBracketLinear.
• TauCeti.gradedPow: the p-power operator π : gr_k(G) → gr_{k+1}(G), and its iterate TauCeti.gradedPowIter π^j : gr_0(G) → gr_j(G) on degree-zero classes.
• TauCeti.gradedPowIterBracket: the iterated p-power π^m [ξ_g, ξ_h] ∈ gr_{m+1}(G) of the bracket of two degree-zero classes, the class of ⁅g, h⁆ ^ (p ^ m).
• TauCeti.gradedMap: the map on graded pieces induced by a continuous homomorphism.

Main results

• TauCeti.quotientPLowerCentralSeriesSuccMulEquiv: λ_k ⧸ λ_{k+1} is the quotient λ_k ⧸ λ_kᵖ[λ_k, G] of λ_k by one step of the lower p-series, through which gr_k(G) inherits its commutativity and its exponent.
• TauCeti.natCard_quotient_pLowerCentralStep_eq_natCard_gradedPiece: for a normal subgroup R = λ_k, the quotient R ⧸ Rᵖ[R, G] has as many elements as gr_k(G).
• TauCeti.gradedBracket_self, TauCeti.gradedBracket_jacobi: the bracket is alternating and satisfies the Jacobi identity.
• TauCeti.gradedPow_add_of_one_le: π is additive in every degree k ≥ 1.
• TauCeti.gradedPow_add_zero, TauCeti.gradedPow_add_zero_of_odd, TauCeti.gradedPow_add_zero_of_two: in degree zero π (x + y) = π x + π y + (p choose 2) • [y, x], so π is additive for odd p, and π (x + y) = π x + π y + [x, y] for p = 2.
• TauCeti.gradedPow_gradedBracket_left, TauCeti.gradedPow_gradedBracket_right: π [x, y] = [π x, y] = [x, π y] away from degree zero.
• TauCeti.gradedMap_gradedBracket, TauCeti.gradedMap_gradedPow: naturality of the bracket and of π.
• TauCeti.gradedMap_symm_gradedMap: the graded map of the inverse of a topological isomorphism inverts the graded map of the isomorphism.
• MulEquiv.gradedPowIter_gradedMkZero_ne_zero_multiplicative_zmod_pow: in a discrete group isomorphic to ℤ/pⁿ⁺¹, π^n of the class of the generator is nonzero.

References

• J. Labute, Classification of Demushkin groups, Canadian J. Math. 19 (1967), §1, Propositions 1 and 2.
• J. D. Dixon, M. P. F. du Sautoy, A. Mann and D. Segal, Analytic pro-p groups, Section 1.2.

Congruences modulo the next term

The image of λ_k in G ⧸ λ_{k+1} is central, so conjugation acts trivially on it and the commutator is bimultiplicative modulo λ_{j+k+2}. Computations combining congruences of different degrees need these statements modulo an arbitrary coarser term λ_{n'}, n' ≤ n, as well.

theorem TauCeti.mk_eq_mk_mul_mk_of_le {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {a b c : G} {n : ℕ} (n' : ℕ) (h : n' ≤ n) (habc : ↑a = ↑b * ↑c) : ↑a = ↑b * ↑c

A congruence mk a = mk b * mk c modulo λ_n holds modulo every λ_{n'} with n' ≤ n.

theorem TauCeti.mk_eq_one_of_mem_pLowerCentralSeries_of_le {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {n : ℕ} (n' : ℕ) {c : G} (hc : c ∈ pLowerCentralSeries p G n) (h : n' ≤ n) : ↑c = 1

The class in G ⧸ λ_{n'} of an element of λ_n is trivial as soon as n' ≤ n.

theorem TauCeti.commute_mk_of_mem_pLowerCentralSeries_of_le {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {n : ℕ} (n' : ℕ) {c : G} (hc : c ∈ pLowerCentralSeries p G n) (h : n' ≤ n + 1) (g : G) : Commute ↑g ↑c

The class of an element of λ_n in G ⧸ λ_{n'} is central as soon as n' ≤ n + 1.

theorem TauCeti.commute_mk_of_mem_pLowerCentralSeries {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {c : G} (hc : c ∈ pLowerCentralSeries p G k) (g : G) : Commute ↑g ↑c

The class of an element of λ_k in G ⧸ λ_{k+1} commutes with every class.

theorem TauCeti.mk_conj_of_mem_pLowerCentralSeries {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {c : G} (hc : c ∈ pLowerCentralSeries p G k) (g : G) : ↑(g * c * g⁻¹) = ↑c

Conjugation acts trivially on the image of λ_k in G ⧸ λ_{k+1}.

theorem TauCeti.mk_commutatorElement_mul_right {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {j k : ℕ} {x y' : G} (hx : x ∈ pLowerCentralSeries p G j) (hy' : y' ∈ pLowerCentralSeries p G k) (y : G) : ↑⁅x, y * y'⁆ = ↑⁅x, y⁆ * ↑⁅x, y'⁆

Modulo λ_{j+k+2}, the commutator ⁅x, ·⁆ of an element x ∈ λ_j is multiplicative on λ_k. Only the second factor has to lie in λ_k.

theorem TauCeti.mk_commutatorElement_mul_left {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {j k : ℕ} {x' y : G} (hx' : x' ∈ pLowerCentralSeries p G j) (hy : y ∈ pLowerCentralSeries p G k) (x : G) : ↑⁅x * x', y⁆ = ↑⁅x, y⁆ * ↑⁅x', y⁆

Modulo λ_{j+k+2}, the commutator ⁅·, y⁆ of an element y ∈ λ_k is multiplicative on λ_j. Only the second factor has to lie in λ_j.

theorem TauCeti.commutatorElement_jacobi_mem_pLowerCentralSeries {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {i j k : ℕ} {a b c : G} (ha : a ∈ pLowerCentralSeries p G i) (hb : b ∈ pLowerCentralSeries p G j) (hc : c ∈ pLowerCentralSeries p G k) : ⁅⁅a, b⁆, c⁆ * ⁅⁅b, c⁆, a⁆ * ⁅⁅c, a⁆, b⁆ ∈ pLowerCentralSeries p G (i + j + k + 2 + 1)

The Jacobi identity modulo λ_{i+j+k+3}: for a ∈ λ_i, b ∈ λ_j and c ∈ λ_k, the product of the three cyclic iterated commutators lies in λ_{i+j+k+3}. It is the Hall–Witt identity, read modulo λ_{i+j+k+3}, where the conjugations it carries act trivially.

The graded pieces

@[reducible, inline]

abbrev TauCeti.gradedPiece (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : Type u

The graded piece gr_k(G) = λ_k ⧸ λ_{k+1} of the lower p-series, written additively. It is an abelian group killed by p, hence a ZMod p-module; for a prime p it is finite when G is a topologically finitely generated profinite group, and not in general.

Equations

• TauCeti.gradedPiece p G k = Additive (↥(TauCeti.pLowerCentralSeries p G k) ⧸ (TauCeti.pLowerCentralSeries p G (k + 1)).subgroupOf (TauCeti.pLowerCentralSeries p G k))

def TauCeti.gradedMk (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) (x : ↥(pLowerCentralSeries p G k)) : gradedPiece p G k

The class in gr_k(G) of an element of λ_k.

Equations

• TauCeti.gradedMk p G k x = Additive.ofMul ↑x

theorem TauCeti.gradedMk_def {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) (x : ↥(pLowerCentralSeries p G k)) : gradedMk p G k x = Additive.ofMul ↑x

The class of x ∈ λ_k in gr_k(G) is its class in the quotient λ_k ⧸ λ_{k+1}, read additively: the unfolding equation of TauCeti.gradedMk, whose definition is sealed outside this module.

theorem TauCeti.gradedMk_surjective {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : Function.Surjective (gradedMk p G k)

theorem TauCeti.gradedMk_eq_gradedMk_iff {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {x y : ↥(pLowerCentralSeries p G k)} : gradedMk p G k x = gradedMk p G k y ↔ ↑↑x = ↑↑y

Two elements of λ_k have the same class in gr_k(G) if and only if they have the same class in G ⧸ λ_{k+1}.

@[simp]

theorem TauCeti.gradedMk_eq_zero_iff {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} {x : ↥(pLowerCentralSeries p G k)} : gradedMk p G k x = 0 ↔ ↑x ∈ pLowerCentralSeries p G (k + 1)

The class of an element of λ_k in gr_k(G) vanishes if and only if the element lies in λ_{k+1}.

@[simp]

theorem TauCeti.gradedMk_mul {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} (x y : ↥(pLowerCentralSeries p G k)) : gradedMk p G k (x * y) = gradedMk p G k x + gradedMk p G k y

@[simp]

theorem TauCeti.gradedMk_one {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : gradedMk p G k 1 = 0

@[simp]

theorem TauCeti.gradedMk_inv {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} (x : ↥(pLowerCentralSeries p G k)) : gradedMk p G k x⁻¹ = -gradedMk p G k x

@[simp]

theorem TauCeti.gradedMk_pow {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} (x : ↥(pLowerCentralSeries p G k)) (n : ℕ) : gradedMk p G k (x ^ n) = n • gradedMk p G k x

@[simp]

theorem TauCeti.gradedMk_zpow {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} (x : ↥(pLowerCentralSeries p G k)) (n : ℤ) : gradedMk p G k (x ^ n) = n • gradedMk p G k x

@[simp]

theorem TauCeti.gradedMk_list_prod {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} (l : List ↥(pLowerCentralSeries p G k)) : gradedMk p G k l.prod = (List.map (gradedMk p G k) l).sum

The class of a product of elements of λ_k is the sum of their classes.

def TauCeti.quotientPLowerCentralSeriesSuccMulEquiv (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : ↥(pLowerCentralSeries p G k) ⧸ (pLowerCentralSeries p G (k + 1)).subgroupOf (pLowerCentralSeries p G k) ≃* ↥(pLowerCentralSeries p G k) ⧸ (pLowerCentralStep p (pLowerCentralSeries p G k)).subgroupOf (pLowerCentralSeries p G k)

The quotient λ_k ⧸ λ_{k+1} is the quotient λ_k ⧸ λ_kᵖ[λ_k, G] of λ_k by one step of the lower p-series, since λ_{k+1} = λ_kᵖ[λ_k, G]: the identity of λ_k descends to a group isomorphism. Through it gr_k(G) inherits the commutativity and the exponent of N ⧸ Nᵖ[N, G] (TauCeti.instIsMulCommutativeQuotientPLowerCentralStep, TauCeti.exponent_quotient_pLowerCentralStep_subgroupOf_dvd).

Equations

• TauCeti.quotientPLowerCentralSeriesSuccMulEquiv p G k = QuotientGroup.quotientMulEquivOfEq ⋯

@[simp]

theorem TauCeti.quotientPLowerCentralSeriesSuccMulEquiv_mk {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) (x : ↥(pLowerCentralSeries p G k)) : (quotientPLowerCentralSeriesSuccMulEquiv p G k) ↑x = ↑x

@[instance_reducible]

instance TauCeti.instCommGroupQuotientPLowerCentralSeries {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : CommGroup (↥(pLowerCentralSeries p G k) ⧸ (pLowerCentralSeries p G (k + 1)).subgroupOf (pLowerCentralSeries p G k))

The quotient λ_k ⧸ λ_{k+1} is an abelian group, with its existing quotient operations: it is the commutative quotient λ_k ⧸ λ_kᵖ[λ_k, G].

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.nsmul_gradedPiece_eq_zero {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} (x : gradedPiece p G k) : p • x = 0

The graded pieces are killed by p: the exponent of λ_k ⧸ λ_kᵖ[λ_k, G] divides p.

theorem TauCeti.choose_two_nsmul_gradedPiece_eq_zero_of_odd {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hp : Odd p) {k : ℕ} (x : gradedPiece p G k) : p.choose 2 • x = 0

For odd p, the graded pieces are killed by p choose 2 = p * ((p - 1) / 2).

@[instance_reducible]

instance TauCeti.instModuleZModGradedPiece {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : Module (ZMod p) (gradedPiece p G k)

The graded pieces are ZMod p-modules, with the canonical action on an abelian group killed by p.

Equations

• TauCeti.instModuleZModGradedPiece k = AddCommGroup.zmodModule ⋯

The inclusion into G ⧸ λ_{k+1}

def TauCeti.gradedPieceInclusion (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : gradedPiece p G k →+ Additive (G ⧸ pLowerCentralSeries p G (k + 1))

The injection of gr_k(G) = λ_k ⧸ λ_{k+1} into G ⧸ λ_{k+1}.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.gradedPieceInclusion_gradedMk {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} (x : ↥(pLowerCentralSeries p G k)) : (gradedPieceInclusion p G k) (gradedMk p G k x) = Additive.ofMul ↑↑x

theorem TauCeti.gradedPieceInclusion_injective {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : Function.Injective ⇑(gradedPieceInclusion p G k)

theorem TauCeti.gradedPieceInclusion_zero_surjective {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Function.Surjective ⇑(gradedPieceInclusion p G 0)

noncomputable def TauCeti.gradedPieceZeroEquiv (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : gradedPiece p G 0 ≃+ Additive (G ⧸ pLowerCentralSeries p G 1)

The degree-zero piece is G ⧸ λ_1. For a profinite group and a prime p, λ_1 is the pro-p Frattini subgroup, so gr_0(G) is the Frattini quotient.

Equations

• TauCeti.gradedPieceZeroEquiv p G = AddEquiv.ofBijective (TauCeti.gradedPieceInclusion p G 0) ⋯

theorem TauCeti.gradedPieceZeroEquiv_gradedMk {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x : ↥(pLowerCentralSeries p G 0)) : (gradedPieceZeroEquiv p G) (gradedMk p G 0 x) = Additive.ofMul ↑↑x

theorem TauCeti.natCard_quotient_pLowerCentralStep_eq_natCard_gradedPiece {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {R : Subgroup G} [R.Normal] {k : ℕ} (hR : R = pLowerCentralSeries p G k) : Nat.card (↥R ⧸ (pLowerCentralStep p R).subgroupOf R) = Nat.card (gradedPiece p G k)

For a normal subgroup R equal to the term λ_k of the lower p-series, the quotient R ⧸ Rᵖ[R, G] is the graded piece gr_k(G) = λ_k ⧸ λ_{k+1}, up to the additive notation; in particular they have the same cardinality. The equation R = λ_k is a hypothesis rather than a substitution, so that the statement applies to the relation subgroup of a presentation, whose quotient type depends on it.

The class of an element of G in degree zero

def TauCeti.gradedMkZero (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) : gradedPiece p G 0

The class in degree zero of an element of G: every element lies in λ_0 = G, and gradedMkZero p G g is its class in gr_0(G) = G ⧸ λ_1.

Equations

• TauCeti.gradedMkZero p G g = TauCeti.gradedMk p G 0 ⟨g, ⋯⟩

theorem TauCeti.continuous_gradedMkZero {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Continuous (gradedMkZero p G)

The class map from a topological group to degree zero of its lower p-series is continuous.

@[simp]

theorem TauCeti.gradedMk_zero {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x : ↥(pLowerCentralSeries p G 0)) : gradedMk p G 0 x = gradedMkZero p G ↑x

The class in degree zero of an element of λ_0 is the class of the underlying element.

theorem TauCeti.gradedMkZero_surjective {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Function.Surjective (gradedMkZero p G)

theorem TauCeti.gradedMkZero_eq_gradedMkZero_iff {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {g h : G} : gradedMkZero p G g = gradedMkZero p G h ↔ ↑g = ↑h

Two elements of G have the same class in gr_0(G) if and only if they have the same class in G ⧸ λ_1.

@[simp]

theorem TauCeti.gradedMkZero_eq_zero_iff {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {g : G} : gradedMkZero p G g = 0 ↔ g ∈ pLowerCentralSeries p G 1

The class of an element in gr_0(G) vanishes if and only if the element lies in λ_1.

@[simp]

theorem TauCeti.gradedMkZero_mul {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g h : G) : gradedMkZero p G (g * h) = gradedMkZero p G g + gradedMkZero p G h

@[simp]

theorem TauCeti.gradedMkZero_one {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : gradedMkZero p G 1 = 0

@[simp]

theorem TauCeti.gradedMkZero_inv {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) : gradedMkZero p G g⁻¹ = -gradedMkZero p G g

@[simp]

theorem TauCeti.gradedMkZero_pow {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) (n : ℕ) : gradedMkZero p G (g ^ n) = n • gradedMkZero p G g

@[simp]

theorem TauCeti.gradedMkZero_list_prod {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (l : List G) : gradedMkZero p G l.prod = (List.map (gradedMkZero p G) l).sum

The degree-zero class of a product of elements of G is the sum of their classes.

theorem TauCeti.gradedMkZero_conj {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (c g : G) : gradedMkZero p G (c⁻¹ * g * c) = gradedMkZero p G g

The degree-zero class is invariant under conjugation, since gr_0(G) is abelian.

@[simp]

theorem TauCeti.gradedPieceZeroEquiv_gradedMkZero {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) : (gradedPieceZeroEquiv p G) (gradedMkZero p G g) = Additive.ofMul ↑g

Transport along an equality of degrees

def TauCeti.gradedCast (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {j k : ℕ} (h : j = k) : gradedPiece p G j → gradedPiece p G k

Transport along an equality of degrees. The bracket and the p-power operator compose into different but equal degree expressions, so the Jacobi identity and the identities relating π to the bracket are stated through this map.

Equations

• TauCeti.gradedCast p G h x = h ▸ x

@[simp]

theorem TauCeti.gradedCast_rfl {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} (x : gradedPiece p G k) : gradedCast p G ⋯ x = x

@[simp]

theorem TauCeti.gradedCast_gradedMk {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {j k : ℕ} (h : j = k) (x : ↥(pLowerCentralSeries p G j)) : gradedCast p G h (gradedMk p G j x) = gradedMk p G k ⟨↑x, ⋯⟩

@[simp]

theorem TauCeti.gradedCast_add {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {j k : ℕ} (h : j = k) (x y : gradedPiece p G j) : gradedCast p G h (x + y) = gradedCast p G h x + gradedCast p G h y

@[simp]

theorem TauCeti.gradedCast_neg {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {j k : ℕ} (h : j = k) (x : gradedPiece p G j) : gradedCast p G h (-x) = -gradedCast p G h x

@[simp]

theorem TauCeti.gradedCast_zero {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {j k : ℕ} (h : j = k) : gradedCast p G h 0 = 0

The bracket

def TauCeti.gradedBracket (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (j k : ℕ) : gradedPiece p G j →+ gradedPiece p G k →+ gradedPiece p G (j + k + 1)

The bracket [·, ·] : gr_j(G) →+ gr_k(G) →+ gr_{j+k+1}(G), induced by the group commutator ⁅x, y⁆ = x * y * x⁻¹ * y⁻¹. The degree shifts by one because the series is 0-based. Its defining equation is TauCeti.gradedBracket_gradedMk.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.gradedBracket_gradedMk {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {j k : ℕ} (x : ↥(pLowerCentralSeries p G j)) (y : ↥(pLowerCentralSeries p G k)) : ((gradedBracket p G j k) (gradedMk p G j x)) (gradedMk p G k y) = gradedMk p G (j + k + 1) ⟨⁅↑x, ↑y⁆, ⋯⟩

The bracket on classes: the defining equation of TauCeti.gradedBracket.

@[simp]

theorem TauCeti.gradedBracket_gradedMkZero {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g h : G) : ((gradedBracket p G 0 0) (gradedMkZero p G g)) (gradedMkZero p G h) = gradedMk p G 1 ⟨⁅g, h⁆, ⋯⟩

The bracket of two degree-zero classes, as the class of the commutator in gr_1(G).

def TauCeti.gradedBracketLinear (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (j k : ℕ) : gradedPiece p G j →ₗ[ZMod p] gradedPiece p G k →ₗ[ZMod p] gradedPiece p G (j + k + 1)

The bracket as a ZMod p-bilinear map gr_j(G) →ₗ[ZMod p] gr_k(G) →ₗ[ZMod p] gr_{j+k+1}(G): the biadditive bracket TauCeti.gradedBracket is automatically ZMod p-bilinear.

Equations

• TauCeti.gradedBracketLinear p G j k = LinearMap.mk₂ (ZMod p) (fun (x : TauCeti.gradedPiece p G j) (y : TauCeti.gradedPiece p G k) => ((TauCeti.gradedBracket p G j k) x) y) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.gradedBracketLinear_apply {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {j k : ℕ} (x : gradedPiece p G j) (y : gradedPiece p G k) : ((gradedBracketLinear p G j k) x) y = ((gradedBracket p G j k) x) y

@[simp]

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

The bracket is alternating: [x, x] = 0 in every degree.

@[simp]

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

The bracket of a commutative group vanishes in every degree, since it is the class of a commutator.

theorem TauCeti.gradedCast_gradedBracket_swap {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {j k : ℕ} (x : gradedPiece p G j) (y : gradedPiece p G k) : gradedCast p G ⋯ (((gradedBracket p G k j) y) x) = -((gradedBracket p G j k) x) y

Skew-symmetry: [y, x] = -[x, y], transported to a common degree.

theorem TauCeti.gradedBracket_jacobi {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {i j k : ℕ} (x : gradedPiece p G i) (y : gradedPiece p G j) (z : gradedPiece p G k) : gradedCast p G ⋯ (((gradedBracket p G (i + j + 1) k) (((gradedBracket p G i j) x) y)) z) + gradedCast p G ⋯ (((gradedBracket p G (j + k + 1) i) (((gradedBracket p G j k) y) z)) x) + gradedCast p G ⋯ (((gradedBracket p G (k + i + 1) j) (((gradedBracket p G k i) z) x)) y) = 0

The Jacobi identity, with the three terms transported to the degree i + j + k + 2.

The p-power operator

def TauCeti.gradedPow (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : gradedPiece p G k → gradedPiece p G (k + 1)

The p-power operator π : gr_k(G) → gr_{k+1}(G), induced by x ↦ x ^ p. It is additive in every degree k ≥ 1 (TauCeti.gradedPow_add_of_one_le); in degree zero its defect of additivity is (p choose 2) • [y, x] (TauCeti.gradedPow_add_zero), which vanishes for odd p (TauCeti.gradedPow_add_zero_of_odd) and is the bracket [x, y] for p = 2 (TauCeti.gradedPow_add_zero_of_two). Its defining equation is TauCeti.gradedPow_gradedMk.

Equations

• TauCeti.gradedPow p G k x = Additive.ofMul (Quotient.map' (fun (y : ↥(TauCeti.pLowerCentralSeries p G k)) => ⟨↑y ^ p, ⋯⟩) ⋯ (Additive.toMul x))

@[simp]

theorem TauCeti.gradedPow_gradedMk {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} (x : ↥(pLowerCentralSeries p G k)) : gradedPow p G k (gradedMk p G k x) = gradedMk p G (k + 1) ⟨↑x ^ p, ⋯⟩

The p-power operator on classes: the defining equation of TauCeti.gradedPow.

@[simp]

theorem TauCeti.gradedPow_zero {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : gradedPow p G k 0 = 0

@[simp]

theorem TauCeti.gradedPow_gradedMkZero {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) : gradedPow p G 0 (gradedMkZero p G g) = gradedMk p G 1 ⟨g ^ p, ⋯⟩

The p-power operator on a degree-zero class, as the class of the p-th power in gr_1(G).

@[simp]

theorem TauCeti.gradedPow_zsmul {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} (n : ℤ) (x : gradedPiece p G k) : gradedPow p G k (n • x) = n • gradedPow p G k x

π commutes with integer multiples, in every degree and for every p: on classes it is (x ^ n) ^ p = (x ^ p) ^ n.

@[simp]

theorem TauCeti.gradedPow_nsmul {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} (n : ℕ) (x : gradedPiece p G k) : gradedPow p G k (n • x) = n • gradedPow p G k x

π commutes with natural multiples, in every degree and for every p.

@[simp]

theorem TauCeti.gradedPow_neg {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} (x : gradedPiece p G k) : gradedPow p G k (-x) = -gradedPow p G k x

π commutes with negation, in every degree and for every p.

@[simp]

theorem TauCeti.gradedPow_smul {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} (c : ZMod p) (x : gradedPiece p G k) : gradedPow p G k (c • x) = c • gradedPow p G k x

π commutes with scalars, in every degree and for every p.

theorem TauCeti.gradedMk_pow_mul {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) (c : ℕ) (h : g ^ (p * c) ∈ pLowerCentralSeries p G 1) : gradedMk p G 1 ⟨g ^ (p * c), h⟩ = c • gradedPow p G 0 (gradedMkZero p G g)

The class of a p-power in gr_1(G): the class of g ^ (p * c) is c times the p-power class π ⟦g⟧.

@[simp]

theorem TauCeti.gradedPow_add_of_one_le {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} (hk : 1 ≤ k) (x y : gradedPiece p G k) : gradedPow p G k (x + y) = gradedPow p G k x + gradedPow p G k y

π is additive above degree zero, for every p: for k ≥ 1 the image of λ_k in G ⧸ λ_{k+2} is abelian, because ⁅λ_k, λ_k⁆ ≤ λ_{2k+1} ≤ λ_{k+2}.

def TauCeti.gradedPowAddMonoidHom (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} (hk : 1 ≤ k) : gradedPiece p G k →+ gradedPiece p G (k + 1)

The p-power operator above degree zero, as an additive map gr_k(G) →+ gr_{k+1}(G), for k ≥ 1, where π is additive (TauCeti.gradedPow_add_of_one_le).

Equations

• TauCeti.gradedPowAddMonoidHom p G hk = AddMonoidHom.mk' (TauCeti.gradedPow p G k) ⋯

@[simp]

theorem TauCeti.gradedPowAddMonoidHom_apply {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} (hk : 1 ≤ k) (x : gradedPiece p G k) : (gradedPowAddMonoidHom p G hk) x = gradedPow p G k x

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

The defect of additivity in degree zero: π (x + y) = π x + π y + (p choose 2) • [y, x] in gr_1(G). This is the binomial formula (x * y) ^ p = x ^ p * y ^ p * ⁅y, x⁆ ^ (p choose 2) of nilpotency class two, read in G ⧸ λ_2, where the image of λ_1 is central.

@[simp]

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

π is additive in degree zero for odd p: the defect (p choose 2) • [y, x] is a multiple of p • [y, x] = 0.

@[simp]

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

The dyadic defect of additivity in degree zero. For p = 2, π (x + y) = π x + π y + [x, y] in gr_1(G): the defect is the binom(2, 2) term of the Hall–Petrescu formula itself. Whenever some bracket [x, y] in degree zero is nonzero, π is therefore not additive on gr_0(G), so gr(G) carries no 𝔽₂[π]-module structure in which π acts by TauCeti.gradedPow.

theorem TauCeti.gradedPow_gradedBracket_left {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {j k : ℕ} (hj : 1 ≤ j) (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)

π against the bracket on the left, away from degree zero: π [x, y] = [π x, y] for x ∈ gr_j(G) with j ≥ 1. The correction term ⁅x, ⁅x, y⁆⁆ has degree 2j + k + 2, which is above j + k + 2 exactly when j ≥ 1.

theorem TauCeti.gradedPow_gradedBracket_right {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {j k : ℕ} (hk : 1 ≤ 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))

π against the bracket on the right, away from degree zero: π [x, y] = [x, π y] for y ∈ gr_k(G) with k ≥ 1.

@[simp]

theorem TauCeti.gradedBracket_gradedPow_self {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} (x : gradedPiece p G k) : ((gradedBracket p G (k + 1) k) (gradedPow p G k x)) x = 0

A class brackets trivially with its own p-power: [π x, x] = 0 in every degree, since x ^ p commutes with x.

@[simp]

theorem TauCeti.gradedBracket_self_gradedPow {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {k : ℕ} (x : gradedPiece p G k) : ((gradedBracket p G k (k + 1)) x) (gradedPow p G k x) = 0

A class brackets trivially with its own p-power: [x, π x] = 0 in every degree, since x commutes with x ^ p.

Functoriality

def TauCeti.gradedMap (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous ⇑f) (k : ℕ) : gradedPiece p G k →+ gradedPiece p H k

The graded map of a continuous homomorphism: f carries λ_k(G) into λ_k(H), so it induces gr_k(G) →+ gr_k(H). Its defining equation is TauCeti.gradedMap_gradedMk.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.gradedMap_gradedMk {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous ⇑f) {k : ℕ} (x : ↥(pLowerCentralSeries p G k)) : (gradedMap p f hf k) (gradedMk p G k x) = gradedMk p H k ⟨f ↑x, ⋯⟩

The graded map on classes: the defining equation of TauCeti.gradedMap.

@[simp]

theorem TauCeti.gradedMap_gradedMkZero {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous ⇑f) (g : G) : (gradedMap p f hf 0) (gradedMkZero p G g) = gradedMkZero p H (f g)

The graded map in degree zero: the class of g goes to the class of f g.

@[simp]

theorem TauCeti.gradedMap_id {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : gradedMap p (MonoidHom.id G) ⋯ k = AddMonoidHom.id (gradedPiece p G k)

The identity of G induces the identity on every graded piece.

@[simp]

theorem TauCeti.gradedMap_comp {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {K : Type w} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] (g : H →* K) (hg : Continuous ⇑g) (f : G →* H) (hf : Continuous ⇑f) (k : ℕ) : gradedMap p (g.comp f) ⋯ k = (gradedMap p g hg k).comp (gradedMap p f hf k)

The graded map induced by a composite is the composite of the graded maps: gr_k is a functor.

@[simp]

theorem TauCeti.gradedMap_symm_gradedMap {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) (k : ℕ) (x : gradedPiece p G k) : (gradedMap p ↑e.symm ⋯ k) ((gradedMap p ↑e ⋯ k) x) = x

The graded map of the inverse of a topological isomorphism inverts the graded map of the isomorphism, in every degree.

theorem TauCeti.gradedMap_surjective {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous ⇑f) (hfc : IsClosedMap ⇑f) (hsurj : Function.Surjective ⇑f) (k : ℕ) : Function.Surjective ⇑(gradedMap p f hf k)

A continuous closed surjection (for instance a continuous surjection from a compact group onto a Hausdorff group, by Continuous.isClosedMap) induces a surjection in every degree.

@[simp]

theorem TauCeti.gradedMap_gradedBracket {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous ⇑f) {j k : ℕ} (x : gradedPiece p G j) (y : gradedPiece p G k) : (gradedMap p f hf (j + k + 1)) (((gradedBracket p G j k) x) y) = ((gradedBracket p H j k) ((gradedMap p f hf j) x)) ((gradedMap p f hf k) y)

Naturality of the bracket.

@[simp]

theorem TauCeti.gradedMap_gradedPow {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous ⇑f) {k : ℕ} (x : gradedPiece p G k) : (gradedMap p f hf (k + 1)) (gradedPow p G k x) = gradedPow p H k ((gradedMap p f hf k) x)

Naturality of the p-power operator.

Iterated p-powers of degree-zero classes

def TauCeti.gradedPowIter (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (j : ℕ) : gradedPiece p G 0 → gradedPiece p G j

The iterated p-power operator π^j : gr_0(G) → gr_j(G), the j-fold composite π ∘ ⋯ ∘ π of TauCeti.gradedPow starting in degree zero. On classes it is induced by g ↦ g ^ (p ^ j) (TauCeti.gradedPowIter_gradedMkZero). It commutes with scalars (TauCeti.gradedPowIter_smul), but for p = 2 it need not be additive: already π^1 = π has the defect [x, y] in degree zero (TauCeti.gradedPow_add_zero_of_two), which is nonzero for the free pro-2 group of rank two (TauCeti.gradedPow_freeProP_two_not_additive).

Equations

• TauCeti.gradedPowIter p G 0 = id
• TauCeti.gradedPowIter p G j.succ = TauCeti.gradedPow p G j ∘ TauCeti.gradedPowIter p G j

@[simp]

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

@[simp]

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

@[simp]

theorem TauCeti.gradedPowIter_gradedMkZero {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (j : ℕ) (g : G) : gradedPowIter p G j (gradedMkZero p G g) = gradedMk p G j ⟨g ^ p ^ j, ⋯⟩

The iterated p-power operator on classes: π^j sends the class of g to the class of g ^ (p ^ j) in gr_j(G).

@[simp]

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

@[simp]

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

The iterated p-power operator commutes with scalars, since π does in every degree.

@[simp]

theorem TauCeti.gradedMap_gradedPowIter {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous ⇑f) (j : ℕ) (x : gradedPiece p G 0) : (gradedMap p f hf j) (gradedPowIter p G j x) = gradedPowIter p H j ((gradedMap p f hf 0) x)

Naturality of the iterated p-power operator.

theorem TauCeti.gradedPow_mem_span_range_gradedPowIter_succ {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {ι : Type u_1} (x : ι → gradedPiece p G 0) {j : ℕ} (hj : 1 ≤ j) {t : gradedPiece p G j} (ht : t ∈ Submodule.span (ZMod p) (Set.range fun (a : ι) => gradedPowIter p G j (x a))) : gradedPow p G j t ∈ Submodule.span (ZMod p) (Set.range fun (a : ι) => gradedPowIter p G (j + 1) (x a))

π carries the span of iterated p-powers to the next degree: above degree zero, π maps the span of the classes π^j x_a of a family x : ι → gr_0(G) into the span of the classes π^{j+1} x_a.

theorem MulEquiv.gradedPowIter_gradedMkZero_ne_zero_multiplicative_zmod_pow {p : ℕ} [Fact (Nat.Prime p)] {H : Type u} [Group H] [TopologicalSpace H] [DiscreteTopology H] {n : ℕ} (e : H ≃* Multiplicative (ZMod (p ^ (n + 1)))) : TauCeti.gradedPowIter p H n (TauCeti.gradedMkZero p H (e.symm (Multiplicative.ofAdd 1))) ≠ 0

In a discrete group isomorphic to ℤ/pⁿ⁺¹, the iterated p-power class π^n of the generator is nonzero in gr_n.

Iterated p-powers of a bracket of degree-zero classes

theorem TauCeti.commutatorElement_pow_pow_mem_pLowerCentralSeries (p : ℕ) {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g h : G) (m : ℕ) : ⁅g, h⁆ ^ p ^ m ∈ pLowerCentralSeries p G (m + 1)

The p ^ m-th power of the commutator of two elements lies in λ_{m+1}(G).

noncomputable def TauCeti.gradedPowIterBracket (p : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : ℕ) (g h : G) : gradedPiece p G (m + 1)

The iterated p-power of the bracket of two degree-zero classes: π^m [ξ_g, ξ_h], the class in gr_{m+1}(G) of ⁅g, h⁆ ^ (p ^ m). For m = 0 it is the bracket of the classes of g and h (TauCeti.gradedPowIterBracket_zero), and π raises m by one (TauCeti.gradedPow_gradedPowIterBracket). At p = 2 these classes are not brackets of iterated p-powers: π [ξ_g, ξ_h] differs from [π ξ_g, ξ_h] by the correction [[ξ_g, ξ_h], ξ_g], the bracket in gr_2(G) of the degree-one class [ξ_g, ξ_h] with ξ_g (TauCeti.gradedPow_gradedBracket_zero_zero), which is why they occur as spanning vectors of their own in the span statements of the dyadic classification.

Equations

• TauCeti.gradedPowIterBracket p G m g h = TauCeti.gradedMk p G (m + 1) ⟨⁅g, h⁆ ^ p ^ m, ⋯⟩

theorem TauCeti.gradedPowIterBracket_def {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : ℕ) (g h : G) : gradedPowIterBracket p G m g h = gradedMk p G (m + 1) ⟨⁅g, h⁆ ^ p ^ m, ⋯⟩

@[simp]

theorem TauCeti.gradedPowIterBracket_zero {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g h : G) : gradedPowIterBracket p G 0 g h = ((gradedBracket p G 0 0) (gradedMkZero p G g)) (gradedMkZero p G h)

For m = 0, that is without any p-power, π^0 [ξ_g, ξ_h] ∈ gr_1(G) is the bracket of the classes of g and h.

@[simp]

theorem TauCeti.gradedPow_gradedPowIterBracket {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : ℕ) (g h : G) : gradedPow p G (m + 1) (gradedPowIterBracket p G m g h) = gradedPowIterBracket p G (m + 1) g h

π raises the iterated p-power of a bracket by one: π (π^m [ξ_g, ξ_h]) = π^{m+1} [ξ_g, ξ_h].

@[simp]

theorem TauCeti.gradedPowIterBracket_self {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : ℕ) (g : G) : gradedPowIterBracket p G m g g = 0

The iterated p-powers of the bracket of a class with itself vanish.

theorem TauCeti.gradedPowIterBracket_swap {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (m : ℕ) (g h : G) : gradedPowIterBracket p G m h g = -gradedPowIterBracket p G m g h

Skew-symmetry of the iterated p-powers of brackets: π^m [ξ_h, ξ_g] = -π^m [ξ_g, ξ_h].