The closed lower central series of a topological group

The closed lower central series of a topological group G is the sequence of closed normal subgroups

γ₀ = G,   γ_{n+1} = closure [γ_n, G],

the case p = 0 of the lower p-series TauCeti.pLowerCentralSeries: at p = 0 the power term λ_nᵖ of the step closure (λ_nᵖ ⬝ [λ_n, G]) is trivial. It is defined as that case, so the closedness, normality, antitonicity, degree-raising law ⁅γ_j, γ_k⁆ ≤ γ_{j+k+1} and functoriality proved for the lower p-series apply to it, and are recorded here in the notation of the closed series. The degree-raising law is what makes the commutator induce a graded bracket on the successive quotients γ_n ⧸ γ_{n+1}, which are TauCeti.gradedPiece 0 G n.

Each γ_n is the topological closure of the term Subgroup.lowerCentralSeries ⊤ n of the lower central series of the underlying abstract group, because the commutator map is continuous. It is topologically characteristic, and it is contained in every lower p-series term λ_n. In a pro-p group the closed lower central series therefore has trivial intersection (TauCeti.IsProP.iInf_closedLowerCentralSeries_eq_bot).

The terms γ_n are not open in general, unlike the λ_n of a topologically finitely generated pro-p group: for the free pro-p group of rank two, G ⧸ γ_1 is ℤ_p ^ 2.

Main definitions

• TauCeti.closedLowerCentralSeries: the closed lower central series γ_n.

Main results

• TauCeti.closedLowerCentralSeries_succ: γ_{n+1} = closure ⁅γ_n, G⁆.
• TauCeti.commutator_closedLowerCentralSeries_le: the degree-raising law ⁅γ_j, γ_k⁆ ≤ γ_{j+k+1}.
• MonoidHom.map_closedLowerCentralSeries_le, MonoidHom.map_closedLowerCentralSeries_eq_of_surjective, ContinuousMulEquiv.map_closedLowerCentralSeries_eq: functoriality of the series.
• TauCeti.isTopCharacteristic_closedLowerCentralSeries: every term is topologically characteristic.
• TauCeti.closedLowerCentralSeries_eq_topologicalClosure: γ_n is the closure of the n-th term of the abstract lower central series.
• TauCeti.closedLowerCentralSeries_le_pLowerCentralSeries: γ_n ≤ λ_n for every p.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Section 2.8.
• J. D. Dixon, M. P. F. du Sautoy, A. Mann and D. Segal, Analytic pro-p groups, Section 1.2.

def TauCeti.closedLowerCentralSeries (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) : Subgroup G

The closed lower central series of a topological group, 0-based to match Mathlib's Subgroup.lowerCentralSeries: γ₀ = G and γ_{n+1} = closure ⁅γ_n, G⁆ (TauCeti.closedLowerCentralSeries_succ). It is the case p = 0 of the lower p-series (TauCeti.closedLowerCentralSeries_def), and each term is the topological closure of the corresponding term of the lower central series of the underlying group (TauCeti.closedLowerCentralSeries_eq_topologicalClosure).

Equations

• TauCeti.closedLowerCentralSeries G n = TauCeti.pLowerCentralSeries 0 G n

theorem TauCeti.closedLowerCentralSeries_def (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) : closedLowerCentralSeries G n = pLowerCentralSeries 0 G n

The closed lower central series is the lower p-series at p = 0.

@[simp]

theorem TauCeti.closedLowerCentralSeries_zero (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : closedLowerCentralSeries G 0 = ⊤

The zeroth term of the closed lower central series is the whole group.

@[simp]

theorem TauCeti.closedLowerCentralSeries_succ (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) : closedLowerCentralSeries G (n + 1) = ⁅closedLowerCentralSeries G n, ⊤⁆.topologicalClosure

The recursion of the closed lower central series: γ_{n+1} = closure ⁅γ_n, G⁆.

theorem TauCeti.closedLowerCentralSeries_one (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : closedLowerCentralSeries G 1 = (commutator G).topologicalClosure

The first term of the closed lower central series is the closure of the commutator subgroup, the subgroup by which Mathlib's TopologicalAbelianization is the quotient.

instance TauCeti.closedLowerCentralSeries_normal {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) : (closedLowerCentralSeries G n).Normal

Every term of the closed lower central series is a normal subgroup.

theorem TauCeti.isClosed_closedLowerCentralSeries {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) : IsClosed ↑(closedLowerCentralSeries G n)

Every term of the closed lower central series is closed.

theorem TauCeti.closedLowerCentralSeries_antitone {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Antitone (closedLowerCentralSeries G)

The closed lower central series is antitone.

theorem TauCeti.commutator_closedLowerCentralSeries_le {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (j k : ℕ) : ⁅closedLowerCentralSeries G j, closedLowerCentralSeries G k⁆ ≤ closedLowerCentralSeries G (j + k + 1)

The degree-raising law. Commutators of γ_j with γ_k lie in γ_{j+k+1}.

theorem TauCeti.closedLowerCentralSeries_eq_topologicalClosure {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) : closedLowerCentralSeries G n = (⊤.lowerCentralSeries n).topologicalClosure

Comparison with the abstract lower central series. Every term of the closed lower central series is the topological closure of the corresponding term of the lower central series of the underlying group.

theorem TauCeti.closedLowerCentralSeries_le_pLowerCentralSeries {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (p n : ℕ) : closedLowerCentralSeries G n ≤ pLowerCentralSeries p G n

Comparison with the lower p-series. For every p, each term of the closed lower central series is contained in the corresponding term of the lower p-series.

Functoriality

theorem MonoidHom.map_closedLowerCentralSeries_le {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous ⇑f) (n : ℕ) : Subgroup.map f (TauCeti.closedLowerCentralSeries G n) ≤ TauCeti.closedLowerCentralSeries H n

A continuous homomorphism carries γ_n into γ_n.

theorem MonoidHom.map_closedLowerCentralSeries_eq_of_surjective {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous ⇑f) (hfc : IsClosedMap ⇑f) (hsurj : Function.Surjective ⇑f) (n : ℕ) : Subgroup.map f (TauCeti.closedLowerCentralSeries G n) = TauCeti.closedLowerCentralSeries H n

A continuous closed surjection (for instance a continuous surjection from a compact group onto a Hausdorff group, by Continuous.isClosedMap) carries γ_n onto γ_n.

theorem ContinuousMulEquiv.map_closedLowerCentralSeries_eq {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) (n : ℕ) : Subgroup.map e.toMonoidHom (TauCeti.closedLowerCentralSeries G n) = TauCeti.closedLowerCentralSeries H n

A topological group isomorphism matches the closed lower central series of its source and target term by term.

theorem TauCeti.isTopCharacteristic_closedLowerCentralSeries (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) : IsTopCharacteristic G (closedLowerCentralSeries G n)

Every term of the closed lower central series is topologically characteristic.