Continuity of the graded commutator

The commutator on a topological group descends to a jointly continuous bracket on the graded pieces of its lower p-series. In the closed lower central series (p = 0), this permits closed-subgroup arguments with brackets even when the graded pieces are not discrete.

theorem TauCeti.continuous_gradedMk {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : Continuous (gradedMk p G k)

The quotient map from a lower-series term to its graded piece is continuous.

theorem TauCeti.isOpenQuotientMap_gradedMk {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (k : ℕ) : IsOpenQuotientMap (gradedMk p G k)

The quotient map from a lower-series term to its graded piece is open.

theorem TauCeti.continuous_gradedBracket {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (j k : ℕ) : Continuous fun (xy : gradedPiece p G j × gradedPiece p G k) => ((gradedBracket p G j k) xy.1) xy.2

The graded commutator is jointly continuous in its two arguments.