mathlib documentation

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}.

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) :
x upper_central_series_step H ∀ (y : G), x * y * x⁻¹ * y⁻¹ H

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]
@[simp]
theorem upper_central_series_zero (G : Type u_1) [group G] :
@[simp]
theorem mem_upper_central_series_succ_iff (G : Type u_1) [group G] (n : ) (x : G) :
x upper_central_series G (n + 1) ∀ (y : G), x * y * x⁻¹ * y⁻¹ upper_central_series G n

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 : subgroup G) :
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 : 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 requre that H n = {1} for some n.

Equations
theorem ascending_central_series_le_upper {G : Type u_1} [group G] (H : subgroup G) (hH : is_ascending_central_series 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.

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 : subgroup G} {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 : subgroup G} {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
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 lower_central_series G (n + 1) q subgroup.closure {x : G | ∃ (p : G) (H : p lower_central_series G n) (q : G) (H : q ), p * q * p⁻¹ * q⁻¹ = x}
theorem lower_central_series_succ {G : Type u_1} [group G] (n : ) :
lower_central_series G (n + 1) = subgroup.closure {x : G | ∃ (p : G) (H : p lower_central_series G n) (q : G) (H : q ), p * q * p⁻¹ * q⁻¹ = x}
@[protected, instance]

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 : subgroup G) (hH : is_descending_central_series H) (n : ) :

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

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.

@[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

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 is_nilpotent_of_ker_le_center {G : Type u_1} [group G] {H : Type u_2} [group H] (f : G →* H) (hf1 : f.ker subgroup.center G) (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 subgroup.center G) (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]
def nilpotent_quotient_of_nilpotent {G : Type u_1} [group G] (H : subgroup G) [H.normal] [h : group.is_nilpotent G] :

A quotient of a nilpotent group is nilpotent

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

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 : group.is_nilpotent G], Prop} (G : Type u_1) [group G] [group.is_nilpotent G] (hbase : ∀ (G : Type u_1) [_inst_6 : group G] [_inst_7 : subsingleton G], P G) (hstep : ∀ (G : Type u_1) [_inst_8 : group G] [_inst_9 : group.is_nilpotent G], P (G subgroup.center 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]

Abelian groups are nilpotent

Abelian groups have nilpotency class at most one

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 : ) :
@[protected, instance]
def is_nilpotent_prod {G₁ : Type u_2} {G₂ : Type u_3} [group G₁] [group G₂] [group.is_nilpotent G₁] [group.is_nilpotent G₂] :

Products of nilpotent groups are nilpotent

theorem nilpotency_class_prod {G₁ : Type u_2} {G₂ : Type u_3} [group G₁] [group G₂] [group.is_nilpotent G₁] [group.is_nilpotent 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 subgroup.pi set.univ (λ (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_fintype {η : Type u_2} [fintype η] {Gs : η → Type u_3} [Π (i : η), group (Gs i)] (n : ) :
lower_central_series (Π (i : η), Gs i) n = subgroup.pi set.univ (λ (i : η), lower_central_series (Gs i) n)
@[protected, instance]
def is_nilpotent_pi {η : Type u_2} [fintype η] {Gs : η → Type u_3} [Π (i : η), group (Gs i)] [∀ (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} [fintype η] {Gs : η → Type u_3} [Π (i : η), group (Gs i)] [∀ (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]
def is_nilpotent.to_is_solvable {G : Type u_1} [group G] [h : group.is_nilpotent G] :

A nilpotent subgroup is solvable

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

A p-group is nilpotent

theorem is_nilpotent_of_product_of_sylow_group {G : Type u_1} [hG : group G] [hf : fintype G] (e : (Π (p : ((fintype.card G).factorization.support)) (P : sylow 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] [hf : fintype G] :
[group.is_nilpotent G, normalizer_condition G, ∀ (H : subgroup G), is_coatom H → H.normal, ∀ (p : ), fact (nat.prime p)∀ (P : sylow p G), P.normal, nonempty ((Π (p : ((fintype.card G).factorization.support)) (P : sylow 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.