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

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
@[instance]
@[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 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
def group.nilpotency_class (G : Type u_1) [group G] [group.is_nilpotent G] :

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

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

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

@[instance]
def subgroup.is_nilpotent {G : Type u_1} [group G] (H : subgroup G) [hG : group.is_nilpotent G] :
@[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) :