# mathlibdocumentation

group_theory.nilpotent

# Nilpotent groups #

An API for nilpotent groups, that is, groups for which the upper central series reaches ⊤.

## Main definitions #

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

• upper_central_series G : ℕ → subgroup G : the upper central series of a group G. This is an increasing sequence of normal subgroups H n of G with H 0 = ⊥ and H (n + 1) / H n is the centre of G / H n.
• lower_central_series G : ℕ → subgroup G : the lower central series of a group G. This is a decreasing sequence of normal subgroups H n of G with H 0 = ⊤ and H (n + 1) = ⁅H n, G⁆.
• is_nilpotent : A group G is nilpotent if its upper central series reaches ⊤, or equivalently if its lower central series reaches ⊥.
• nilpotency_class : the length of the upper central series of a nilpotent group.
• is_ascending_central_series (H : ℕ → subgroup G) : Prop and
• is_descending_central_series (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 two weaker predicates 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. Similarly a sequence is an ascending central series if H 0 = ⊥ and ⁅H (n + 1), ⊤⁆ ⊆ H n for all n, again with no requirement that the series reaches ⊤ or that the H i are normal.

## Main theorems #

G is defined to be nilpotent if the upper central series reaches ⊤.

• nilpotent_iff_finite_ascending_central_series : G is nilpotent iff some ascending central series reaches ⊤.
• nilpotent_iff_finite_descending_central_series : G is nilpotent iff some descending central series reaches ⊥.
• nilpotent_iff_lower : G is nilpotent iff the lower central series reaches ⊥.
• The nilpotency_class can likeways be obtained from these equivalent definitions, see least_ascending_central_series_length_eq_nilpotency_class, least_descending_central_series_length_eq_nilpotency_class and lower_central_series_length_eq_nilpotency_class.
• is_nilpotent.to_is_solvable: If G is nilpotent, it is solvable.

## Warning #

A "central series" is usually defined to be a finite sequence of normal subgroups going from ⊥ to ⊤ with the property that each subquotient is contained within the centre of the associated quotient of G. This means that if G is not nilpotent, then none of what we have called upper_central_series G, lower_central_series G or the sequences satisfying is_ascending_central_series or is_descending_central_series are actually central series. Note that the fact that the upper and lower central series are not central series if G is not nilpotent is a standard abuse of notation.

def upper_central_series_step {G : Type u_1} [group G] (H : subgroup G) [H.normal] :

If H is a normal subgroup of G, then the set {x : G | ∀ y : G, x*y*x⁻¹*y⁻¹ ∈ H} is a subgroup of G (because it is the preimage in G of the centre of the quotient group G/H.)

Equations
theorem mem_upper_central_series_step {G : Type u_1} [group G] (H : subgroup G) [H.normal] (x : G) :
∀ (y : G), ((x * y) * x⁻¹) * y⁻¹ H
theorem upper_central_series_step_eq_comap_center {G : Type u_1} [group G] (H : subgroup G) [H.normal] :

The proof that upper_central_series_step H is the preimage of the centre of G/H under the canonical surjection.

@[protected, instance]
def upper_central_series_step.subgroup.normal {G : Type u_1} [group G] (H : subgroup G) [H.normal] :
def upper_central_series_aux (G : Type u_1) [group G] :
(Σ' (H : subgroup G), H.normal)

An auxiliary type-theoretic definition defining both the upper central series of a group, and a proof that it is normal, all in one go.

Equations
def upper_central_series (G : Type u_1) [group G] (n : ) :

upper_central_series G n is the nth term in the upper central series of G.

Equations
@[protected, instance]
def upper_central_series.subgroup.normal (G : Type u_1) [group G] (n : ) :
n).normal
@[simp]
theorem upper_central_series_zero (G : Type u_1) [group G] :
theorem mem_upper_central_series_succ_iff (G : Type u_1) [group G] (n : ) (x : G) :
x (n + 1) ∀ (y : G), ((x * y) * x⁻¹) * y⁻¹

The n+1st term of the upper central series H i has underlying set equal to the x such that ⁅x,G⁆ ⊆ H n

@[class]
structure group.is_nilpotent (G : Type u_2) [group G] :
Prop
• nilpotent : ∃ (n : ),

A group G is nilpotent if its upper central series is eventually G.

Instances
def is_ascending_central_series {G : Type u_1} [group G] (H : ) :
Prop

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

Equations
def is_descending_central_series {G : Type u_1} [group G] (H : ) :
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 requre that H n = {1} for some n.

Equations
theorem ascending_central_series_le_upper {G : Type u_1} [group G] (H : ) (hH : is_ascending_central_series H) (n : ) :
H n

Any ascending central series for a group is bounded above by the upper central series.

The upper central series of a group is an ascending central series.

theorem upper_central_series_mono (G : Type u_1) [group G] :
theorem nilpotent_iff_finite_ascending_central_series (G : Type u_1) [group G] :
∃ (n : ) (H : subgroup G),

A group G is nilpotent iff there exists an ascending central series which reaches G in finitely many steps.

theorem is_decending_rev_series_of_is_ascending (G : Type u_1) [group G] {H : } {n : } (hn : H n = ) (hasc : is_ascending_central_series H) :
is_descending_central_series (λ (m : ), H (n - m))
theorem is_ascending_rev_series_of_is_descending (G : Type u_1) [group G] {H : } {n : } (hn : H n = ) (hdesc : is_descending_central_series H) :
is_ascending_central_series (λ (m : ), H (n - m))
theorem nilpotent_iff_finite_descending_central_series (G : Type u_1) [group G] :
∃ (n : ) (H : subgroup G),

A group G is nilpotent iff there exists a descending central series which reaches the trivial group in a finite time.

def lower_central_series (G : Type u_1) [group G] :

The lower central series of a group G is a sequence H n of subgroups of G, defined by H 0 is all of G and for n≥1, H (n + 1) = ⁅H n, G⁆

Equations
• (n + 1) =
@[simp]
theorem lower_central_series_zero {G : Type u_1} [group G] :
theorem mem_lower_central_series_succ_iff {G : Type u_1} [group G] (n : ) (q : G) :
q (n + 1) q subgroup.closure {x : G | ∃ (p : G) (H : p (q : G) (H : q ), ((p * q) * p⁻¹) * q⁻¹ = x}
theorem lower_central_series_succ {G : Type u_1} [group G] (n : ) :
(n + 1) = subgroup.closure {x : G | ∃ (p : G) (H : p (q : G) (H : q ), ((p * q) * p⁻¹) * q⁻¹ = x}
@[protected, instance]
def lower_central_series.subgroup.normal {G : Type u_1} [group G] (n : ) :
n).normal
theorem lower_central_series_antitone {G : Type u_1} [group G] :

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

theorem descending_central_series_ge_lower {G : Type u_1} [group G] (H : ) (hH : is_descending_central_series H) (n : ) :
H n

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

theorem nilpotent_iff_lower_central_series {G : Type u_1} [group G] :
∃ (n : ),

A group is nilpotent if and only if its lower central series eventually reaches the trivial subgroup.

noncomputable def group.nilpotency_class (G : Type u_1) [group G] [hG : group.is_nilpotent G] :

The nilpotency class of a nilpotent group is the smallest natural n such that the n'th term of the upper central series is G.

Equations

The nilpotency class of a nilpotent G is equal to the smallest n for which an ascending central series reaches G in its n'th term.

The nilpotency class of a nilpotent G is equal to the smallest n for which the descending central series reaches ⊥ in its n'th term.

The nilpotency class of a nilpotent G is equal to the length of the lower central series.

theorem lower_central_series_map_subtype_le {G : Type u_1} [group G] (H : subgroup G) (n : ) :
@[protected, instance]
def subgroup.is_nilpotent {G : Type u_1} [group G] (H : subgroup G) [hG : group.is_nilpotent G] :
@[protected, instance]
def is_nilpotent_of_subsingleton {G : Type u_1} [group G] [subsingleton G] :
theorem upper_central_series.map {G : Type u_1} [group G] {H : Type u_2} [group H] {f : G →* H} (h : function.surjective f) (n : ) :
theorem lower_central_series.map {G : Type u_1} [group G] {H : Type u_2} [group H] (f : G →* H) (n : ) :
theorem lower_central_series_succ_eq_bot {G : Type u_1} [group G] {n : } (h : ) :
(n + 1) =
theorem is_nilpotent_of_ker_le_center {G : Type u_1} [group G] {H : Type u_2} [group H] {f : G →* H} (hf1 : f.ker ) (hH : group.is_nilpotent H) :
theorem derived_le_lower_central {G : Type u_1} [group G] (n : ) :
@[protected, instance]
def is_nilpotent.to_is_solvable {G : Type u_1} [group G] [h : group.is_nilpotent G] :