# mathlib3documentation

group_theory.nilpotent

# Nilpotent groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 .

## 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
Instances for upper_central_series_step
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_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
Instances for upper_central_series
@[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] :
@[simp]
theorem upper_central_series_one (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

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

Instances of this typeclass
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] :

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))

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) =
Instances for lower_central_series
@[simp]
theorem lower_central_series_zero {G : Type u_1} [group G] :
@[simp]
theorem lower_central_series_one {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
@[simp]

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.

@[simp]
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] :

A subgroup of a nilpotent group is nilpotent

theorem subgroup.nilpotency_class_le {G : Type u_1} [group G] (H : subgroup G) [hG : group.is_nilpotent G] :

A the nilpotency class of a subgroup is less or equal the the nilpotency class of the group

@[protected, instance]
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) :

The preimage of a nilpotent group is nilpotent if the kernel of the homomorphism is contained in the center

theorem nilpotency_class_le_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 nilpotent_of_surjective {G : Type u_1} [group G] {G' : Type u_2} [group G'] [h : group.is_nilpotent G] (f : G →* G') (hf : function.surjective f) :

The range of a surjective homomorphism from a nilpotent group is nilpotent

theorem nilpotency_class_le_of_surjective {G : Type u_1} [group G] {G' : Type u_2} [group G'] (f : G →* G') (hf : function.surjective f) [h : group.is_nilpotent G] :

The nilpotency class of the range of a surejctive homomorphism from a nilpotent group is less or equal the nilpotency class of the domain

theorem nilpotent_of_mul_equiv {G : Type u_1} [group G] {G' : Type u_2} [group G'] [h : group.is_nilpotent G] (f : G ≃* G') :

Nilpotency respects isomorphisms

@[protected, instance]

A quotient of a nilpotent group is nilpotent

theorem nilpotency_class_quotient_le {G : Type u_1} [group G] (H : subgroup G) [H.normal] [h : group.is_nilpotent G] :

The nilpotency class of a quotient of G is less or equal the nilpotency class of G

Quotienting the center G reduces the nilpotency class by 1

The nilpotency class of a non-trivial group is one more than its quotient by the center

theorem of_quotient_center_nilpotent {G : Type u_1} [group G] (h : group.is_nilpotent (G ) :

If the quotient by center G is nilpotent, then so is G.

theorem nilpotent_center_quotient_ind {P : Π (G : Type u_1) [_inst_3 : group G] [_inst_4 : , Prop} (G : Type u_1) [group G] (hbase : (G : Type u_1) [_inst_6 : group G] [_inst_7 : , P G) (hstep : (G : Type u_1) [_inst_8 : group G] [_inst_9 : , P (G P G) :
P G

A custom induction principle for nilpotent groups. The base case is a trivial group (subsingleton G), and in the induction step, one can assume the hypothesis for the group quotiented by its center.

theorem derived_le_lower_central {G : Type u_1} [group G] (n : ) :
@[protected, instance]
def comm_group.is_nilpotent {G : Type u_1} [comm_group G] :

Abelian groups are nilpotent

Abelian groups have nilpotency class at most one

def comm_group_of_nilpotency_class {G : Type u_1} [group G] (h : 1) :

Groups with nilpotency class at most one are abelian

Equations
theorem lower_central_series_prod {G₁ : Type u_2} {G₂ : Type u_3} [group G₁] [group G₂] (n : ) :
lower_central_series (G₁ × G₂) n = n).prod n)
@[protected, instance]
def is_nilpotent_prod {G₁ : Type u_2} {G₂ : Type u_3} [group G₁] [group G₂]  :

Products of nilpotent groups are nilpotent

theorem nilpotency_class_prod {G₁ : Type u_2} {G₂ : Type u_3} [group G₁] [group G₂]  :

The nilpotency class of a product is the max of the nilpotency classes of the factors

theorem lower_central_series_pi_le {η : Type u_2} {Gs : η Type u_3} [Π (i : η), group (Gs i)] (n : ) :
lower_central_series (Π (i : η), Gs i) n (λ (i : η), lower_central_series (Gs i) n)
theorem is_nilpotent_pi_of_bounded_class {η : Type u_2} {Gs : η Type u_3} [Π (i : η), group (Gs i)] [ (i : η), group.is_nilpotent (Gs i)] (n : ) (h : (i : η), group.nilpotency_class (Gs i) n) :
group.is_nilpotent (Π (i : η), Gs i)

products of nilpotent groups are nilpotent if their nipotency class is bounded

theorem lower_central_series_pi_of_finite {η : Type u_2} {Gs : η Type u_3} [Π (i : η), group (Gs i)] [finite η] (n : ) :
lower_central_series (Π (i : η), Gs i) n = (λ (i : η), lower_central_series (Gs i) n)
@[protected, instance]
def is_nilpotent_pi {η : Type u_2} {Gs : η Type u_3} [Π (i : η), group (Gs i)] [finite η] [ (i : η), group.is_nilpotent (Gs i)] :
group.is_nilpotent (Π (i : η), Gs i)

n-ary products of nilpotent groups are nilpotent

theorem nilpotency_class_pi {η : Type u_2} {Gs : η Type u_3} [Π (i : η), group (Gs i)] [fintype η] [ (i : η), group.is_nilpotent (Gs i)] :
group.nilpotency_class (Π (i : η), Gs i) = finset.univ.sup (λ (i : η), group.nilpotency_class (Gs i))

The nilpotency class of an n-ary product is the sup of the nilpotency classes of the factors

@[protected, instance]

A nilpotent subgroup is solvable

theorem is_p_group.is_nilpotent {G : Type u_1} [hG : group G] [finite G] {p : } [hp : fact (nat.prime p)] (h : G) :

A p-group is nilpotent

theorem is_nilpotent_of_product_of_sylow_group {G : Type u_1} [hG : group G] [fintype G] (e : (Π (p : .support)) (P : G), P) ≃* G) :

If a finite group is the direct product of its Sylow groups, it is nilpotent

theorem is_nilpotent_of_finite_tfae {G : Type u_1} [hG : group G] [fintype G] :
[, , (H : subgroup G), H.normal, (p : ), fact (nat.prime p) (P : G), P.normal, nonempty ((Π (p : .support)) (P : G), P) ≃* G)].tfae

A finite group is nilpotent iff the normalizer condition holds, and iff all maximal groups are normal and iff all sylow groups are normal and iff the group is the direct product of its sylow groups.