The graded bracket of the closed lower central series

The successive quotients of the closed lower central series are the case p = 0 of Tau Ceti's graded pieces for the lower p-series. This file gives that specialization its consumer-facing names; its commutator formula is lcsBracket_lcsGradedMk. The ℤ_p-module structure and bilinearity results for a pro-p group are the case q = 0 of the results in TauCeti.Topology.Algebra.Group.LowerCentralSeries.Graded.PadicModule.

Main definitions

• TauCeti.lcsGradedPiece: the successive quotient γ_n(G) / γ_{n+1}(G), written additively.
• TauCeti.lcsGradedMk: the class of an element of γ_n(G).
• TauCeti.lcsBracket: the bracket induced by the group commutator.

Main results

• TauCeti.lcsGradedMk_conj: conjugation is trivial on each graded piece.
• TauCeti.lcsGradedMk_surjective: every graded class has a closed-series representative.
• TauCeti.lcsBracket_lcsGradedMk: the bracket of two classes is the class of the commutator.

References

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

@[reducible, inline]

abbrev TauCeti.lcsGradedPiece (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) : Type u

The n-th graded piece of the closed lower central series, written additively. It is a profinite abelian group when G is profinite.

@[reducible, inline]

abbrev TauCeti.lcsGradedMk (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) (x : ↥(closedLowerCentralSeries G n)) : lcsGradedPiece G n

The class in γ_n(G) / γ_{n+1}(G) of an element of γ_n(G).

theorem TauCeti.lcsGradedMk_surjective {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) : Function.Surjective (lcsGradedMk G n)

Every class in a closed lower-central-series graded piece has a representative in that term of the closed lower central series.

@[simp]

theorem TauCeti.lcsGradedMk_conj {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) (g : G) (x : ↥(closedLowerCentralSeries G n)) : lcsGradedMk G n ⟨g * ↑x * g⁻¹, ⋯⟩ = lcsGradedMk G n x

Conjugation acts trivially on every graded piece of the closed lower central series.

@[reducible, inline]

abbrev TauCeti.lcsBracket (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (j k : ℕ) : lcsGradedPiece G j →+ lcsGradedPiece G k →+ lcsGradedPiece G (j + k + 1)

The bracket on the graded pieces of the closed lower central series. Its degree is j + k + 1 because the series is indexed from zero.

theorem TauCeti.lcsBracket_lcsGradedMk {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {j k : ℕ} (x : ↥(closedLowerCentralSeries G j)) (y : ↥(closedLowerCentralSeries G k)) : ((lcsBracket G j k) (lcsGradedMk G j x)) (lcsGradedMk G k y) = lcsGradedMk G (j + k + 1) ⟨⁅↑x, ↑y⁆, ⋯⟩

The closed-series bracket on classes is represented by the group commutator.