Lower Central Series

This file defines the lower central series of a subgroup.

Main definitions

Recall that if H K : Subgroup G then ⁅H, K⁆ : Subgroup G is the subgroup of G generated by the commutators h * k * h⁻¹ * k⁻¹. Recall also Lean's conventions that ⊤ denotes the subgroup G of G, and ⊥ denotes the trivial subgroup {1}.

• Subgroup.lowerCentralSeries (H : Subgroup G) : ℕ → Subgroup G : the lower central series of H, computed in the ambient group G. These are the iterated commutators H, ⁅H, H⁆, ⁅⁅H, H⁆, H⁆, …. The classical lower central series of G is the case H = ⊤.
• IsDescendingCentralSeries (H : ℕ → Subgroup G) : Prop : Note that in the literature a "central series" for a group is usually defined to be a finite sequence of normal subgroups H 0, H 1, ..., starting at ⊤, finishing at ⊥, and with each H n / H (n + 1) central in G / H (n + 1). In this formalisation it is convenient to have a weaker predicate on an infinite sequence of subgroups H n of G: we say a sequence is a descending central series if it starts at G and ⁅H n, ⊤⁆ ⊆ H (n + 1) for all n. Note that this series may not terminate at ⊥, and the H i need not be normal.

def Subgroup.IsDescendingCentralSeries {G : Type u_1} [Group G] (H : ℕ → Subgroup G) : Prop

A sequence of subgroups of G is a descending central series if H 0 is G and ⁅H n, G⁆ ⊆ H (n + 1) for all n. Note that we do not require that H n = {1} for some n.

Equations

• Subgroup.IsDescendingCentralSeries H = (H 0 = ⊤ ∧ ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1))

def AddSubgroup.IsDescendingCentralSeries {G : Type u_1} [AddGroup G] (H : ℕ → AddSubgroup G) : Prop

A sequence of additive subgroups of G is a descending central series if H 0 is G and ⁅H n, G⁆ ⊆ H (n + 1) for all n. We do not require that H n = {1} for some n.

Equations

• AddSubgroup.IsDescendingCentralSeries H = (H 0 = ⊤ ∧ ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1))

def AddSubgroup.lowerCentralSeries {G : Type u_2} [AddGroup G] (H : AddSubgroup G) : ℕ → AddSubgroup G

The lower central series of an additive subgroup H of G, computed in the ambient additive group G.

Equations

• H.lowerCentralSeries 0 = H
• H.lowerCentralSeries n.succ = ⁅H.lowerCentralSeries n, H⁆

def Subgroup.lowerCentralSeries {G : Type u_1} [Group G] (H : Subgroup G) : ℕ → Subgroup G

The lower central series of a subgroup H of G, computed in the ambient group G. This is the iterated commutator ⁅⁅⋯⁅H, H⁆, H⁆⋯, H⁆, a subgroup of G. The lower central series of G itself is the case H = ⊤.

Equations

• H.lowerCentralSeries 0 = H
• H.lowerCentralSeries n.succ = ⁅H.lowerCentralSeries n, H⁆

@[simp]

theorem Subgroup.lowerCentralSeries_zero {G : Type u_1} [Group G] (H : Subgroup G) : H.lowerCentralSeries 0 = H

@[simp]

theorem AddSubgroup.lowerCentralSeries_zero {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : H.lowerCentralSeries 0 = H

@[simp]

theorem Subgroup.lowerCentralSeries_succ {G : Type u_1} [Group G] (H : Subgroup G) (n : ℕ) : H.lowerCentralSeries (n + 1) = ⁅H.lowerCentralSeries n, H⁆

@[simp]

theorem AddSubgroup.lowerCentralSeries_succ {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (n : ℕ) : H.lowerCentralSeries (n + 1) = ⁅H.lowerCentralSeries n, H⁆

theorem Subgroup.top_lowerCentralSeries_one {G : Type u_1} [Group G] : ⊤.lowerCentralSeries 1 = _root_.commutator G

theorem AddSubgroup.top_lowerCentralSeries_one {G : Type u_1} [AddGroup G] : ⊤.lowerCentralSeries 1 = _root_.addCommutator G

theorem Subgroup.lowerCentralSeries_one_eq_bot_iff {G : Type u_1} [Group G] : ⊤.lowerCentralSeries 1 = ⊥ ↔ IsMulCommutative G

theorem AddSubgroup.lowerCentralSeries_zero_eq_bot_iff {G : Type u_1} [AddGroup G] : ⊤.lowerCentralSeries 1 = ⊥ ↔ IsAddCommutative G

@[deprecated AddSubgroup.top_lowerCentralSeries_one (since := "2026-05-25")]

theorem AddSubgroup.lowerCentralSeries_one {G : Type u_1} [AddGroup G] : ⊤.lowerCentralSeries 1 = _root_.addCommutator G

Alias of AddSubgroup.top_lowerCentralSeries_one.

@[deprecated Subgroup.top_lowerCentralSeries_one (since := "2026-05-25")]

theorem Subgroup.lowerCentralSeries_one {G : Type u_1} [Group G] : ⊤.lowerCentralSeries 1 = _root_.commutator G

Alias of Subgroup.top_lowerCentralSeries_one.

theorem Subgroup.mem_lowerCentralSeries_succ_iff {G : Type u_1} [Group G] (H : Subgroup G) (n : ℕ) (q : G) : q ∈ H.lowerCentralSeries (n + 1) ↔ q ∈ closure {x : G | ∃ p ∈ H.lowerCentralSeries n, ∃ q ∈ H, ⁅p, q⁆ = x}

theorem AddSubgroup.mem_lowerCentralSeries_succ_iff {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (n : ℕ) (q : G) : q ∈ H.lowerCentralSeries (n + 1) ↔ q ∈ closure {x : G | ∃ p ∈ H.lowerCentralSeries n, ∃ q ∈ H, ⁅p, q⁆ = x}

instance Subgroup.lowerCentralSeries_normal {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] (n : ℕ) : (N.lowerCentralSeries n).Normal

instance AddSubgroup.lowerCentralSeries_normal {G : Type u_1} [AddGroup G] (N : AddSubgroup G) [N.Normal] (n : ℕ) : (N.lowerCentralSeries n).Normal

instance Subgroup.lowerCentralSeries_characteristic {G : Type u_1} [Group G] (H : Subgroup G) [H.Characteristic] (n : ℕ) : (H.lowerCentralSeries n).Characteristic

instance AddSubgroup.lowerCentralSeries_characteristic {G : Type u_1} [AddGroup G] (H : AddSubgroup G) [H.Characteristic] (n : ℕ) : (H.lowerCentralSeries n).Characteristic

theorem Subgroup.self_le_normalizer_lowerCentralSeries {G : Type u_1} [Group G] (H : Subgroup G) (n : ℕ) : H ≤ normalizer ↑(H.lowerCentralSeries n)

theorem AddSubgroup.self_le_normalizer_lowerCentralSeries {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (n : ℕ) : H ≤ normalizer ↑(H.lowerCentralSeries n)

theorem Subgroup.lowerCentralSeries_antitone {G : Type u_1} [Group G] (H : Subgroup G) : Antitone H.lowerCentralSeries

theorem AddSubgroup.lowerCentralSeries_antitone {G : Type u_1} [AddGroup G] (H : AddSubgroup G) : Antitone H.lowerCentralSeries

theorem Subgroup.lowerCentralSeries_isDescendingCentralSeries {G : Type u_1} [Group G] : IsDescendingCentralSeries ⊤.lowerCentralSeries

The lower central series of a group is a descending central series.

theorem AddSubgroup.lowerCentralSeries_isDescendingCentralSeries {G : Type u_1} [AddGroup G] : IsDescendingCentralSeries ⊤.lowerCentralSeries

The lower central series of an additive group is a descending central series.

theorem Subgroup.descending_central_series_ge_lower {G : Type u_1} [Group G] (H : ℕ → Subgroup G) (hH : IsDescendingCentralSeries H) (n : ℕ) : ⊤.lowerCentralSeries n ≤ H n

Any descending central series for a group is bounded below by the lower central series.

theorem AddSubgroup.descending_central_series_ge_lower {G : Type u_1} [AddGroup G] (H : ℕ → AddSubgroup G) (hH : IsDescendingCentralSeries H) (n : ℕ) : ⊤.lowerCentralSeries n ≤ H n

Any descending central series for an additive group is bounded below by the lower central series.

theorem Subgroup.map_lowerCentralSeries {G : Type u_1} [Group G] (H : Subgroup G) {G' : Type u_2} [Group G'] (f : G →* G') (n : ℕ) : map f (H.lowerCentralSeries n) = (map f H).lowerCentralSeries n

The lower central series commutes with images under a group homomorphism.

theorem AddSubgroup.map_lowerCentralSeries {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {G' : Type u_2} [AddGroup G'] (f : G →+ G') (n : ℕ) : map f (H.lowerCentralSeries n) = (map f H).lowerCentralSeries n

The lower central series commutes with images under an additive group homomorphism.

@[simp]

theorem Subgroup.top_subtype_lowerCentralSeries {G : Type u_1} [Group G] (H : Subgroup G) (n : ℕ) : map H.subtype (⊤.lowerCentralSeries n) = H.lowerCentralSeries n

The lower central series of H : Subgroup G computed in the ambient group G coincides with the lower central series of H viewed as its own group, mapped back to G.

@[simp]

theorem AddSubgroup.top_subtype_lowerCentralSeries {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (n : ℕ) : map H.subtype (⊤.lowerCentralSeries n) = H.lowerCentralSeries n

The lower central series of H : AddSubgroup G computed in the ambient additive group G coincides with the lower central series of H viewed as its own additive group, mapped back to G.

theorem Subgroup.lowerCentralSeries_le_self {G : Type u_1} [Group G] (H : Subgroup G) (n : ℕ) : H.lowerCentralSeries n ≤ H

theorem AddSubgroup.lowerCentralSeries_le_self {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (n : ℕ) : H.lowerCentralSeries n ≤ H

theorem Subgroup.lowerCentralSeries_mono {G : Type u_1} [Group G] (n : ℕ) : Monotone fun (H : Subgroup G) => H.lowerCentralSeries n

theorem AddSubgroup.lowerCentralSeries_mono {G : Type u_1} [AddGroup G] (n : ℕ) : Monotone fun (H : AddSubgroup G) => H.lowerCentralSeries n

@[deprecated "Use `top_subtype_lowerCentralSeries` and `lowerCentralSeries_mono` instead." (since := "2026-05-27")]

theorem Subgroup.lowerCentralSeries_map_subtype_le {G : Type u_1} [Group G] (H : Subgroup G) (n : ℕ) : map H.subtype (⊤.lowerCentralSeries n) ≤ ⊤.lowerCentralSeries n

@[deprecated "Use `top_subtype_lowerCentralSeries` and `lowerCentralSeries_mono` instead." (since := "2026-05-27")]

theorem AddSubgroup.lowerCentralSeries_map_subtype_le {G : Type u_1} [AddGroup G] (H : AddSubgroup G) (n : ℕ) : map H.subtype (⊤.lowerCentralSeries n) ≤ ⊤.lowerCentralSeries n

@[deprecated "Use `map_lowerCentralSeries` and `lowerCentralSeries_mono` instead." (since := "2026-05-28")]

theorem Subgroup.lowerCentralSeries.map {G : Type u_1} [Group G] {G' : Type u_2} [Group G'] (f : G →* G') (n : ℕ) : Subgroup.map f (⊤.lowerCentralSeries n) ≤ ⊤.lowerCentralSeries n

@[deprecated "Use `map_lowerCentralSeries` and `lowerCentralSeries_mono` instead." (since := "2026-05-28")]

theorem AddSubgroup.lowerCentralSeries.map {G : Type u_1} [AddGroup G] {G' : Type u_2} [AddGroup G'] (f : G →+ G') (n : ℕ) : AddSubgroup.map f (⊤.lowerCentralSeries n) ≤ ⊤.lowerCentralSeries n

theorem Subgroup.lowerCentralSeries_succ_eq_bot {G : Type u_1} [Group G] (H : Subgroup G) {n : ℕ} (h : H.lowerCentralSeries n ≤ center G) : H.lowerCentralSeries (n + 1) = ⊥

theorem AddSubgroup.lowerCentralSeries_succ_eq_bot {G : Type u_1} [AddGroup G] (H : AddSubgroup G) {n : ℕ} (h : H.lowerCentralSeries n ≤ center G) : H.lowerCentralSeries (n + 1) = ⊥

theorem Subgroup.derivedSeries_le_lowerCentralSeries_top {G : Type u_1} [Group G] (n : ℕ) : derivedSeries G n ≤ ⊤.lowerCentralSeries n

theorem AddSubgroup.derivedSeries_le_lowerCentralSeries_top {G : Type u_1} [AddGroup G] (n : ℕ) : derivedSeries G n ≤ ⊤.lowerCentralSeries n

@[deprecated Subgroup.derivedSeries_le_lowerCentralSeries_top (since := "2026-10-19")]

theorem Subgroup.derived_le_lower_central {G : Type u_1} [Group G] (n : ℕ) : derivedSeries G n ≤ ⊤.lowerCentralSeries n

Alias of Subgroup.derivedSeries_le_lowerCentralSeries_top.

theorem Subgroup.lowerCentralSeries_prod {G₁ : Type u_2} {G₂ : Type u_3} [Group G₁] [Group G₂] (H₁ : Subgroup G₁) (H₂ : Subgroup G₂) (n : ℕ) : (H₁.prod H₂).lowerCentralSeries n = (H₁.lowerCentralSeries n).prod (H₂.lowerCentralSeries n)

theorem AddSubgroup.lowerCentralSeries_sum {G₁ : Type u_2} {G₂ : Type u_3} [AddGroup G₁] [AddGroup G₂] (H₁ : AddSubgroup G₁) (H₂ : AddSubgroup G₂) (n : ℕ) : (H₁.prod H₂).lowerCentralSeries n = (H₁.lowerCentralSeries n).prod (H₂.lowerCentralSeries n)

theorem Subgroup.top_lowerCentralSeries_prod {G₁ : Type u_2} {G₂ : Type u_3} [Group G₁] [Group G₂] (n : ℕ) : ⊤.lowerCentralSeries n = (⊤.lowerCentralSeries n).prod (⊤.lowerCentralSeries n)

The ⊤-specialization of lowerCentralSeries_prod.

theorem AddSubgroup.top_lowerCentralSeries_sum {G₁ : Type u_2} {G₂ : Type u_3} [AddGroup G₁] [AddGroup G₂] (n : ℕ) : ⊤.lowerCentralSeries n = (⊤.lowerCentralSeries n).prod (⊤.lowerCentralSeries n)

The ⊤-specialization of lowerCentralSeries_sum.

theorem Subgroup.lowerCentralSeries_pi_le {η : Type u_2} {Gs : η → Type u_3} [(i : η) → Group (Gs i)] (Hs : (i : η) → Subgroup (Gs i)) (n : ℕ) : (pi Set.univ Hs).lowerCentralSeries n ≤ pi Set.univ fun (i : η) => (Hs i).lowerCentralSeries n

theorem AddSubgroup.lowerCentralSeries_pi_le {η : Type u_2} {Gs : η → Type u_3} [(i : η) → AddGroup (Gs i)] (Hs : (i : η) → AddSubgroup (Gs i)) (n : ℕ) : (pi Set.univ Hs).lowerCentralSeries n ≤ pi Set.univ fun (i : η) => (Hs i).lowerCentralSeries n

theorem Subgroup.top_lowerCentralSeries_pi_le {η : Type u_2} {Gs : η → Type u_3} [(i : η) → Group (Gs i)] (n : ℕ) : ⊤.lowerCentralSeries n ≤ pi Set.univ fun (i : η) => ⊤.lowerCentralSeries n

The ⊤-specialization of lowerCentralSeries_pi_le.

theorem AddSubgroup.top_lowerCentralSeries_pi_le {η : Type u_2} {Gs : η → Type u_3} [(i : η) → AddGroup (Gs i)] (n : ℕ) : ⊤.lowerCentralSeries n ≤ pi Set.univ fun (i : η) => ⊤.lowerCentralSeries n

The ⊤-specialization of lowerCentralSeries_pi_le.

theorem Subgroup.lowerCentralSeries_pi_of_finite {η : Type u_2} {Gs : η → Type u_3} [(i : η) → Group (Gs i)] [Finite η] (Hs : (i : η) → Subgroup (Gs i)) (n : ℕ) : (pi Set.univ Hs).lowerCentralSeries n = pi Set.univ fun (i : η) => (Hs i).lowerCentralSeries n

theorem AddSubgroup.lowerCentralSeries_pi_of_finite {η : Type u_2} {Gs : η → Type u_3} [(i : η) → AddGroup (Gs i)] [Finite η] (Hs : (i : η) → AddSubgroup (Gs i)) (n : ℕ) : (pi Set.univ Hs).lowerCentralSeries n = pi Set.univ fun (i : η) => (Hs i).lowerCentralSeries n

theorem Subgroup.top_lowerCentralSeries_pi_of_finite {η : Type u_2} {Gs : η → Type u_3} [(i : η) → Group (Gs i)] [Finite η] (n : ℕ) : ⊤.lowerCentralSeries n = pi Set.univ fun (i : η) => ⊤.lowerCentralSeries n

The ⊤-specialization of lowerCentralSeries_pi_of_finite.

theorem AddSubgroup.top_lowerCentralSeries_pi_of_finite {η : Type u_2} {Gs : η → Type u_3} [(i : η) → AddGroup (Gs i)] [Finite η] (n : ℕ) : ⊤.lowerCentralSeries n = pi Set.univ fun (i : η) => ⊤.lowerCentralSeries n

The ⊤-specialization of lowerCentralSeries_pi_of_finite.