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

• 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.
• If G is nilpotent, then so are its subgroups, images, quotients and preimages. Binary and finite products of nilpotent groups are nilpotent. Infinite products are nilpotent if their nilpotent class is bounded. Corresponding lemmas about the nilpotency_class are provided.
• The nilpotency_class of G ⧸ center G is given explicitly, and an induction principle is derived from that.
• 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.