Generation of the graded pieces of the closed lower central series

The brackets of a topological generating set with a graded piece topologically generate the next piece. If the source graded piece is compact and the generating set finite, their sums fill the next piece. The distinction matters because the closed lower central series terms need not be open.

theorem TauCeti.gradedBracket_gradedMkZero_mem_of_isClosed {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) {S : Set G} (hS : (Subgroup.closure S).topologicalClosure = ⊤) {W : AddSubgroup (gradedPiece 0 G (0 + n + 1))} (hWclosed : IsClosed ↑W) (hgen : ∀ s ∈ S, ∀ (y : gradedPiece 0 G n), ((gradedBracket 0 G 0 n) (gradedMkZero 0 G s)) y ∈ W) (g : G) (y : gradedPiece 0 G n) : ((gradedBracket 0 G 0 n) (gradedMkZero 0 G g)) y ∈ W

A closed additive subgroup of the next graded piece that contains the brackets of a topological generating set with the graded piece n contains all brackets of G with it.

theorem TauCeti.eq_top_of_isClosed_of_gradedBracket_mem {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) {W : AddSubgroup (gradedPiece 0 G (0 + n + 1))} (hWclosed : IsClosed ↑W) (hbracket : ∀ (g : G) (y : gradedPiece 0 G n), ((gradedBracket 0 G 0 n) (gradedMkZero 0 G g)) y ∈ W) : W = ⊤

A closed additive subgroup of the next graded piece that contains every bracket of G with the graded piece n is the whole piece. The closed commutator step of the closed lower central series is what makes the brackets span.

theorem TauCeti.topologicalClosure_closure_gradedBracket_eq_top {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) {S : Set G} (hS : (Subgroup.closure S).topologicalClosure = ⊤) : (AddSubgroup.closure (Set.range fun (sy : ↑S × gradedPiece 0 G n) => ((gradedBracket 0 G 0 n) (gradedMkZero 0 G ↑sy.1)) sy.2)).topologicalClosure = ⊤

The brackets with a topological generating set generate the next closed-series graded piece after taking closure.

theorem TauCeti.exists_sum_gradedBracket_eq_of_range {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {ι : Type u_2} [Fintype ι] (n : ℕ) [CompactSpace (gradedPiece 0 G n)] (s : ι → G) (hs : (Subgroup.closure (Set.range s)).topologicalClosure = ⊤) (z : gradedPiece 0 G (0 + n + 1)) : ∃ (y : ι → gradedPiece 0 G n), ∑ i : ι, ((gradedBracket 0 G 0 n) (gradedMkZero 0 G (s i))) (y i) = z

If a finite indexed family topologically generates the group and the source graded piece is compact, every class in the next graded piece is a sum of one bracket with each member of the family. The indexing keeps separate coefficients even when two generators coincide.