Subgroup.nilpotencyClass_le
theorem Subgroup.nilpotencyClass_le :
∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [hG : Group.IsNilpotent G],
Group.nilpotencyClass ↥H ≤ Group.nilpotencyClass G
This theorem states that the nilpotency class of a subgroup is always less than or equal to the nilpotency class of the entire group. In other words, for any type `G` with a group structure and a subgroup `H` of `G`, if `G` is nilpotent, then the smallest natural number `n` such that the `n`th term of the upper central series of `H` is `H` is less than or equal to the smallest natural number `m` such that the `m`th term of the upper central series of `G` is `G`.
More concisely: If `G` is a nilpotent group and `H` is a subgroup of `G`, then the nilpotency class of `H` is less than or equal to the nilpotency class of `G`.
|
descending_central_series_ge_lower
theorem descending_central_series_ge_lower :
∀ {G : Type u_1} [inst : Group G] (H : ℕ → Subgroup G),
IsDescendingCentralSeries H → ∀ (n : ℕ), lowerCentralSeries G n ≤ H n
The theorem `descending_central_series_ge_lower` states that for any group `G`, any descending central series `H` is always bounded below by the lower central series. In other words, for every natural number `n`, the `n`-th term of the lower central series of the group `G` is a subgroup of the `n`-th term of the descending central series `H`. This means the lower central series provides a lower bound for any descending central series in the group.
More concisely: For any group G and any descending central series H, the lower central series of G is a refinement of H.
|
least_ascending_central_series_length_eq_nilpotencyClass
theorem least_ascending_central_series_length_eq_nilpotencyClass :
∀ {G : Type u_1} [inst : Group G] [hG : Group.IsNilpotent G], Nat.find ⋯ = Group.nilpotencyClass G
The theorem `least_ascending_central_series_length_eq_nilpotencyClass` states that for any given nilpotent group `G`, the nilpotency class of `G` (defined as the smallest natural number `n` such that the `n`th term of the upper central series is `G`) is equivalent to the smallest `n` such that an ascending central series reaches `G` in its `n`th term. This establishes a link between the concept of nilpotency class and the structure of ascending central series in a nilpotent group.
More concisely: The nilpotency class of a nilpotent group equals the length of the shortest ascending central series that reaches the group itself.
|
isNilpotent_of_ker_le_center
theorem isNilpotent_of_ker_le_center :
∀ {G : Type u_1} [inst : Group G] {H : Type u_2} [inst_1 : Group H] (f : G →* H),
f.ker ≤ Subgroup.center G → Group.IsNilpotent H → Group.IsNilpotent G
The theorem `isNilpotent_of_ker_le_center` states that for any two groups `G` and `H` and a group homomorphism `f` from `G` to `H`, if the kernel of `f` is contained within the center of group `G` and if group `H` is nilpotent, then group `G` is also nilpotent. Here, the center of a group is the set of elements that commute with all elements of the group, and a nilpotent group is a group that has an upper-bound on the order of its elements when generated under group operation.
More concisely: If a group homomorphism from a group with a kernel contained in its center maps to a nilpotent group, then the initial group is nilpotent.
|
lowerCentralSeries_length_eq_nilpotencyClass
theorem lowerCentralSeries_length_eq_nilpotencyClass :
∀ {G : Type u_1} [inst : Group G] [hG : Group.IsNilpotent G], Nat.find ⋯ = Group.nilpotencyClass G
The theorem states that for any nilpotent group `G`, the nilpotency class of `G` is equal to the length of the lower central series. In other words, the number of steps in the lower central series until reaching the whole group `G` is the same as the smallest natural number `n` for which the `n`-th term of the upper central series is `G` (the nilpotency class of `G`).
More concisely: The nilpotency class of a nilpotent group equals the length of its lower central series.
|
CommGroup.nilpotencyClass_le_one
theorem CommGroup.nilpotencyClass_le_one : ∀ {G : Type u_2} [inst : CommGroup G], Group.nilpotencyClass G ≤ 1 := by
sorry
The theorem `CommGroup.nilpotencyClass_le_one` states that for any Abelian group `G`, the nilpotency class of `G` is less than or equal to one. In other words, in the context of Abelian groups, the smallest natural number `n` such that the `n`'th term of the upper central series is `G` is always one or less.
More concisely: In any Abelian group, the nilpotency class is at most 1.
|
nilpotent_of_surjective
theorem nilpotent_of_surjective :
∀ {G : Type u_1} [inst : Group G] {G' : Type u_2} [inst_1 : Group G'] [h : Group.IsNilpotent G] (f : G →* G'),
Function.Surjective ⇑f → Group.IsNilpotent G'
The theorem `nilpotent_of_surjective` states that for any given groups `G` and `G'` and a group homomorphism `f` from `G` to `G'`, if `G` is nilpotent and `f` is surjective, then `G'` is also nilpotent. In other words, the property of being nilpotent is preserved under surjective group homomorphisms.
More concisely: If `G` is a nilpotent group and `f` is a surjective group homomorphism from `G` to `G'`, then `G'` is also a nilpotent group.
|
nilpotencyClass_quotient_le
theorem nilpotencyClass_quotient_le :
∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [inst_1 : H.Normal] [_h : Group.IsNilpotent G],
Group.nilpotencyClass (G ⧸ H) ≤ Group.nilpotencyClass G
The theorem `nilpotencyClass_quotient_le` states that for any group `G` which is nilpotent, and any subgroup `H` of `G`, the nilpotency class of the quotient group `G ⧸ H` is less than or equal to the nilpotency class of `G`. Here, the nilpotency class is defined as the smallest natural number `n` such that the `n`-th term of the upper central series is `G`. This result is fundamental in the theory of nilpotent groups.
More concisely: For any nilpotent group `G` and subgroup `H`, the nilpotency class of the quotient group `G / H` is less than or equal to the nilpotency class of `G`.
|
nilpotencyClass_pi
theorem nilpotencyClass_pi :
∀ {η : Type u_2} {Gs : η → Type u_3} [inst : (i : η) → Group (Gs i)] [inst_1 : Fintype η]
[inst_2 : ∀ (i : η), Group.IsNilpotent (Gs i)],
Group.nilpotencyClass ((i : η) → Gs i) = Finset.univ.sup fun i => Group.nilpotencyClass (Gs i)
The theorem `nilpotencyClass_pi` states that for a product group, composed of a finite set of nilpotent groups, the nilpotency class of the entire product group is equal to the supremum (i.e., the maximum) of the nilpotency classes of the individual factor groups. In other words, the degree of nilpotence of the product group is determined by the group factor that has the highest degree of nilpotency.
More concisely: The nilpotency class of a product of finite nilpotent groups is equal to the maximum nilpotency class of its factors.
|
of_quotient_center_nilpotent
theorem of_quotient_center_nilpotent :
∀ {G : Type u_1} [inst : Group G], Group.IsNilpotent (G ⧸ Subgroup.center G) → Group.IsNilpotent G
This theorem states that for any group `G`, if the quotient of `G` by its center (i.e., the set of elements that commute with all elements in `G`) is a nilpotent group, then `G` itself is a nilpotent group. In other words, if we can form a sequence of normal subgroups for the quotient group `G`/`center(G)` starting from the whole group down to the trivial group, where each subgroup is normal in the previous one, then such a sequence also exists for the original group `G`.
More concisely: If the quotient of a group `G` by its center is a nilpotent group, then `G` is also a nilpotent group.
|
upperCentralSeriesStep_eq_comap_center
theorem upperCentralSeriesStep_eq_comap_center :
∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [inst_1 : H.Normal],
upperCentralSeriesStep H = Subgroup.comap (QuotientGroup.mk' H) (Subgroup.center (G ⧸ H))
This theorem establishes that in a group `G` with a normal subgroup `H`, the `upperCentralSeriesStep H` is the preimage of the center of the quotient group `G/H` under the canonical surjection. In other words, it verifies that the set of elements in `G` that commute with `H` when conjugated (denoted as `upperCentralSeriesStep H`) is exactly the set of elements in `G` that get mapped to the center of `G/H` by the quotient map.
More concisely: The upper central series step of a normal subgroup in a group is the preimage of the center of the quotient group under the canonical surjection.
|
nilpotencyClass_quotient_center
theorem nilpotencyClass_quotient_center :
∀ {G : Type u_1} [inst : Group G] [hH : Group.IsNilpotent G],
Group.nilpotencyClass (G ⧸ Subgroup.center G) = Group.nilpotencyClass G - 1
This theorem states that for any given group `G` that is nilpotent, the nilpotency class of the quotient group formed by taking the group `G` and quotienting by its center is equal to the nilpotency class of the original group `G` minus one. In other words, reducing the group `G` by its center - the set of elements that commute with all elements in `G` - decreases the nilpotency class, a measure of the 'degree' of nilpotence, by one.
More concisely: For any nilpotent group `G`, the nilpotency class of `G/Z(G)` (quotient group of `G` by its center `Z(G)`) is equal to the nilpotency class of `G` minus one.
|
least_descending_central_series_length_eq_nilpotencyClass
theorem least_descending_central_series_length_eq_nilpotencyClass :
∀ {G : Type u_1} [inst : Group G] [hG : Group.IsNilpotent G], Nat.find ⋯ = Group.nilpotencyClass G
This theorem states that the nilpotency class of a nilpotent group `G` is equal to the smallest natural number `n` such that the `n`'th term of the descending central series reaches the bottom element. In other words, it equates the concept of nilpotency class, defined through the upper central series, with the length of the descending central series until it reaches the bottom.
More concisely: The nilpotency class of a nilpotent group equals the length of the descending central series that reaches the identity element.
|
lowerCentralSeries_isDescendingCentralSeries
theorem lowerCentralSeries_isDescendingCentralSeries :
∀ {G : Type u_1} [inst : Group G], IsDescendingCentralSeries (lowerCentralSeries G)
The theorem states that for any group `G`, the lower central series of that group is a descending central series. In mathematical terms, it says that if `H n` represents the `n`th subgroup in the lower central series of `G`, then `H 0` is the entire group `G` and for every element `x` in `H n` and every `g` in `G`, the element `x * g * x⁻¹ * g⁻¹` is in `H (n + 1)`. This reflects the defining properties of a descending central series.
More concisely: The lower central series of any group is a descending central series, that is, for all `n`, `H n+1` is the subnormal subgroup of `H n` generated by commutators `[x, g]` for all `x` in `H n` and `g` in the group.
|
nilpotent_iff_finite_ascending_central_series
theorem nilpotent_iff_finite_ascending_central_series :
∀ (G : Type u_1) [inst : Group G], Group.IsNilpotent G ↔ ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤
A group `G` is described as nilpotent if and only if there exists an ascending central series that reaches `G` in a finite number of steps. In this context, an ascending central series is a sequence of subgroups of `G` where the initial subgroup is trivial and every subsequent subgroup is contained in the commutator of the preceding subgroup and `G`. The condition `H n = ⊤` signifies that the ascending central series reaches the whole group `G` at the `n`-th step.
More concisely: A group G is nilpotent if and only if it has a finite-length ascending central series.
|
upperCentralSeries_isAscendingCentralSeries
theorem upperCentralSeries_isAscendingCentralSeries :
∀ (G : Type u_1) [inst : Group G], IsAscendingCentralSeries (upperCentralSeries G)
This theorem states that the upper central series of a group is an ascending central series. In other words, for any group `G`, the upper central series, which is a sequence of subgroups of `G`, satisfies two properties: first, the subgroup at index 0 is trivial (consists only of the identity element); second, for every element `x` in the subgroup at index `(n + 1)` and for any element `g` of the group, the commutator of `x` and `g` (given by `x * g * x⁻¹ * g⁻¹`) is in the subgroup at index `n`.
More concisely: The upper central series of a group is a filtration where each subgroup is the normal closure of the commutators of the previous subgroup with the group. (This is equivalent to the given properties in Lean 4.)
|
lowerCentralSeries_eq_bot_iff_nilpotencyClass_le
theorem lowerCentralSeries_eq_bot_iff_nilpotencyClass_le :
∀ {G : Type u_1} [inst : Group G] [hG : Group.IsNilpotent G] {n : ℕ},
lowerCentralSeries G n = ⊥ ↔ Group.nilpotencyClass G ≤ n
The theorem `lowerCentralSeries_eq_bot_iff_nilpotencyClass_le` states that for any group `G` that is nilpotent, the `n`th term of its lower central series is the trivial subgroup if and only if the nilpotency class of `G` is less than or equal to `n`. In other words, if we reach the bottom of the lower central series at step `n`, then the nilpotency class of the group (the minimum natural number at which the upper central series reaches the entire group) must be at most `n`.
More concisely: For any nilpotent group G, the n-th term of its lower central series is the trivial subgroup if and only if the nilpotency class of G is less than or equal to n.
|
isNilpotent_of_finite_tFAE
theorem isNilpotent_of_finite_tFAE :
∀ {G : Type u_1} [hG : Group G] [inst : Fintype G],
[Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → H.Normal,
∀ (p : ℕ), Fact p.Prime → ∀ (P : Sylow p G), P.Normal,
Nonempty (((p : { x // x ∈ (Fintype.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G)].TFAE
This theorem states that for any finite group `G`, the following five conditions are all equivalent:
1. `G` is nilpotent,
2. Every proper subgroup `H` of `G` is a proper normal subgroup of the normalizer of `H` in `G` (the normalizer condition),
3. Every maximal subgroup `H` of `G` is a normal subgroup,
4. For every prime number `p`, every Sylow `p`-subgroup of `G` is normal,
5. `G` is the direct product of its Sylow subgroups.
Therefore, if any one of these conditions holds for a finite group `G`, then all the others do as well. This theorem essentially provides multiple characterizations of nilpotent groups, so different properties might be easier to verify in different contexts.
More concisely: A finite group `G` is nilpotent if and only if every proper subgroup is normal in its normalizer, every maximal subgroup is normal, every Sylow subgroup is normal, and `G` is the direct product of its Sylow subgroups.
|
mem_upperCentralSeries_succ_iff
theorem mem_upperCentralSeries_succ_iff :
∀ (G : Type u_1) [inst : Group G] (n : ℕ) (x : G),
x ∈ upperCentralSeries G (n + 1) ↔ ∀ (y : G), x * y * x⁻¹ * y⁻¹ ∈ upperCentralSeries G n
The theorem `mem_upperCentralSeries_succ_iff` states that for any group `G` and natural number `n`, an element `x` of the group `G` belongs to the `(n+1)`st term of the upper central series of `G` if and only if for every `y` in `G`, the commutator of `x` and `y`, defined as `x * y * x⁻¹ * y⁻¹`, belongs to the `n`th term of the upper central series of `G`. That is, the elements of the `(n+1)`st term of the upper central series are precisely those elements that commute with every element of the group into the `n`th term of the upper central series.
More concisely: An element x in a group G belongs to the (n+1)st term of the upper central series if and only if for all y in G, the commutator x * y * x⁻¹ * y⁻¹ is in the nth term of the upper central series.
|
nilpotent_of_mulEquiv
theorem nilpotent_of_mulEquiv :
∀ {G : Type u_1} [inst : Group G] {G' : Type u_2} [inst_1 : Group G'] [_h : Group.IsNilpotent G],
G ≃* G' → Group.IsNilpotent G'
This theorem states that nilpotency respects isomorphisms. Specifically, for any given types `G` and `G'` which are groups, if `G` is nilpotent and there exists a group isomorphism between `G` and `G'`, then `G'` must also be nilpotent. Here, `G ≃* G'` represents a group isomorphism between `G` and `G'`, and `Group.IsNilpotent G` and `Group.IsNilpotent G'` represent the nilpotency of groups `G` and `G'` respectively.
More concisely: If `G` is a nilpotent group and there exists a group isomorphism `G ≃* G'`, then `G'` is also nilpotent.
|
nilpotencyClass_prod
theorem nilpotencyClass_prod :
∀ {G₁ : Type u_2} {G₂ : Type u_3} [inst : Group G₁] [inst_1 : Group G₂] [inst_2 : Group.IsNilpotent G₁]
[inst_3 : Group.IsNilpotent G₂],
Group.nilpotencyClass (G₁ × G₂) = max (Group.nilpotencyClass G₁) (Group.nilpotencyClass G₂)
The theorem `nilpotencyClass_prod` states that for any two nilpotent groups `G₁` and `G₂`, the nilpotency class of their direct product `G₁ × G₂` is equal to the maximum of the nilpotency classes of `G₁` and `G₂`. Here, the nilpotency class of a nilpotent group is defined as the smallest natural number `n` such that the `n`-th term of the upper central series of the group is the group itself.
More concisely: The nilpotency class of the direct product of two nilpotent groups is equal to the maximum of their nilpotency classes.
|
isNilpotent_pi_of_bounded_class
theorem isNilpotent_pi_of_bounded_class :
∀ {η : Type u_2} {Gs : η → Type u_3} [inst : (i : η) → Group (Gs i)] [inst_1 : ∀ (i : η), Group.IsNilpotent (Gs i)]
(n : ℕ), (∀ (i : η), Group.nilpotencyClass (Gs i) ≤ n) → Group.IsNilpotent ((i : η) → Gs i)
The theorem `isNilpotent_pi_of_bounded_class` states that if we have a collection of nilpotent groups indexed by some type `η`, where each group is nilpotent and has a nilpotency class less than or equal to a certain natural number `n`, then the product of these groups (considered as a group where the group operation is performed component-wise) is also a nilpotent group. Here, the nilpotency class of a group is the smallest natural number such that the `n`-th term of the group's upper central series is the group itself.
More concisely: If every group in a collection indexed by type `η` is nilpotent with nilpotency class less than or equal to `n`, then their component-wise product is also a nilpotent group with nilpotency class less than or equal to `n`.
|
ascending_central_series_le_upper
theorem ascending_central_series_le_upper :
∀ {G : Type u_1} [inst : Group G] (H : ℕ → Subgroup G),
IsAscendingCentralSeries H → ∀ (n : ℕ), H n ≤ upperCentralSeries G n
This theorem states that for any group `G`, if a sequence of subgroups `H` forms an ascending central series, then each term in this sequence is a subgroup of (or equal to) the corresponding term in the upper central series of `G`. In other words, any ascending central series for a group `G` is elementwise contained in or equal to the upper central series of `G`.
More concisely: For any group `G`, every term in an ascending central series of `G` is contained in or equal to the corresponding term in the upper central series of `G`.
|
isNilpotent_of_product_of_sylow_group
theorem isNilpotent_of_product_of_sylow_group :
∀ {G : Type u_1} [hG : Group G] [inst : Fintype G],
((p : { x // x ∈ (Fintype.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G → Group.IsNilpotent G
The theorem `isNilpotent_of_product_of_sylow_group` states that for any given finite group `G`, if there is a group isomorphism between `G` and the direct product of its Sylow subgroups, then `G` is a nilpotent group. The Sylow subgroups are denoted by `P` and are parametrized by the prime factors of the cardinality of `G`. Each prime factor is represented as a subtype `{ x // x ∈ (Fintype.card G).primeFactors }`, and the isomorphism is denoted by the equivalence relation `≃*`.
More concisely: If a finite group `G` is isomorphic to the direct product of its Sylow subgroups, then `G` is nilpotent.
|
nilpotencyClass_eq_quotient_center_plus_one
theorem nilpotencyClass_eq_quotient_center_plus_one :
∀ {G : Type u_1} [inst : Group G] [hH : Group.IsNilpotent G] [inst_1 : Nontrivial G],
Group.nilpotencyClass G = Group.nilpotencyClass (G ⧸ Subgroup.center G) + 1
The theorem `nilpotencyClass_eq_quotient_center_plus_one` states that for any nontrivial group `G`, which is also nilpotent, the nilpotency class of `G` is equal to one more than the nilpotency class of the quotient group `G / Subgroup.center G`. Here, the quotient group `G / Subgroup.center G` is formed by taking the group `G` and partitioning it into cosets with respect to the center of `G`. The center of a group `G` being the set of all elements that commute with every other element in `G`. The nilpotency class of a nilpotent group is defined as the smallest natural number `n` such that the `n`th term of the upper central series is `G`.
More concisely: In a nontrivial nilpotent group G, the nilpotency class equals one more than that of the quotient group G by its center.
|
nilpotencyClass_le_of_surjective
theorem nilpotencyClass_le_of_surjective :
∀ {G : Type u_1} [inst : Group G] {G' : Type u_2} [inst_1 : Group G'] (f : G →* G') (hf : Function.Surjective ⇑f)
[h : Group.IsNilpotent G], Group.nilpotencyClass G' ≤ Group.nilpotencyClass G
The theorem `nilpotencyClass_le_of_surjective` states that for any surjective homomorphism from a nilpotent group to another group, the nilpotency class of the range (the second group) is less than or equal to the nilpotency class of the domain (the first group). Here, a homomorphism is a function that preserves the group structure, a group is said to be nilpotent if its upper central series terminates in the whole group, and the nilpotency class of such a group is the smallest natural number `n` such that the `n`th term of the upper central series is the group itself. A function is surjective if every element in the target set (second group) is mapped to by at least one element in the domain (first group).
More concisely: For any surjective homomorphism between nilpotent groups, the nilpotency class of the image group is less than or equal to that of the domain group.
|
upperCentralSeries_eq_top_iff_nilpotencyClass_le
theorem upperCentralSeries_eq_top_iff_nilpotencyClass_le :
∀ {G : Type u_1} [inst : Group G] [hG : Group.IsNilpotent G] {n : ℕ},
upperCentralSeries G n = ⊤ ↔ Group.nilpotencyClass G ≤ n
The theorem `upperCentralSeries_eq_top_iff_nilpotencyClass_le` states that for any nilpotent group `G` and natural number `n`, the `n`th term of the upper central series of `G` being the whole group `G` is equivalent to the nilpotency class of `G` being less than or equal to `n`. Here, the upper central series of a group is a sequence of subgroups, and the nilpotency class of a group is the smallest `n` such that the `n`th term of the upper central series is `G`.
More concisely: For any nilpotent group G and natural number n, the upper central series of G reaches G if and only if the nilpotency class of G is less than or equal to n.
|
IsPGroup.isNilpotent
theorem IsPGroup.isNilpotent :
∀ {G : Type u_1} [hG : Group G] [inst : Finite G] {p : ℕ} [hp : Fact p.Prime], IsPGroup p G → Group.IsNilpotent G
This theorem states that any p-group is nilpotent. In other words, for any group `G` that is finite and for any natural number `p` that is prime, if `G` is a p-group (meaning that every element in `G` has an order that is a power of `p`), then `G` is also a nilpotent group. In the context of group theory, a nilpotent group is a group that has an ascending series of normal subgroups where each factor group is abelian.
More concisely: Any finite p-group is nilpotent, meaning it has a normal series with abelian factor groups.
|
nilpotent_iff_finite_descending_central_series
theorem nilpotent_iff_finite_descending_central_series :
∀ (G : Type u_1) [inst : Group G], Group.IsNilpotent G ↔ ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥
A group `G` is defined as nilpotent if and only if there exists a descending central series that reaches the trivial group within a finite amount of steps. In more specific terms, there exists a sequence of subgroups of `G` satisfying two conditions: firstly, the subgroup containing all elements of `G` is the start of the sequence; and secondly, for any element of the nth subgroup and any element of `G`, their associated commutator belongs to the (n+1)th subgroup, and this sequence eventually reduces to the subgroup containing only the identity element of the group.
More concisely: A group is nilpotent if and only if it has a descending central series that finitely terminates at the identity element.
|
Group.IsNilpotent.nilpotent
theorem Group.IsNilpotent.nilpotent :
∀ (G : Type u_2) [inst : Group G] [inst_1 : Group.IsNilpotent G], ∃ n, upperCentralSeries G n = ⊤
This theorem states that for any group 'G' that is nilpotent (as indicated by `Group.IsNilpotent G`), there exists a natural number 'n' such that the 'n'th term of the upper central series of 'G' is equal to the entire group 'G'. The upper central series of a group is a sequence of normal subgroups, where each subgroup is central in the quotient by the subgroup before it. The theorem is essentially asserting a property of nilpotent groups: they have an upper central series that eventually covers the entire group.
More concisely: A nilpotent group 'G' has a finite upper central series that equals the whole group.
|
nilpotent_iff_lowerCentralSeries
theorem nilpotent_iff_lowerCentralSeries :
∀ {G : Type u_1} [inst : Group G], Group.IsNilpotent G ↔ ∃ n, lowerCentralSeries G n = ⊥
The theorem `nilpotent_iff_lowerCentralSeries` states that a group is nilpotent if and only if its lower central series eventually reaches the trivial subgroup. In other words, a group `G` is considered nilpotent when there exists a natural number `n` such that the `n`th term of its lower central series - a sequence of subgroups starting from the whole group `G` and iteratively taking the commutator of the current term and `G` - is the trivial subgroup (denoted as `⊥`).
More concisely: A group is nilpotent if and only if its lower central series reaches the trivial subgroup.
|
upperCentralSeries_one
theorem upperCentralSeries_one : ∀ (G : Type u_1) [inst : Group G], upperCentralSeries G 1 = Subgroup.center G := by
sorry
This theorem states that for any group `G`, the first term in the upper central series of `G` is equal to the center of `G`. In other words, for any group, the set of elements that commute with everything in the group is the same as the first term in the upper central series of the group.
More concisely: The first term of the upper central series of a group equals its center.
|
nilpotent_center_quotient_ind
theorem nilpotent_center_quotient_ind :
∀ {P : (G : Type u_2) → [inst : Group G] → [inst : Group.IsNilpotent G] → Prop} (G : Type u_2) [inst : Group G]
[inst_1 : Group.IsNilpotent G],
(∀ (G : Type u_2) [inst : Group G] [inst_2 : Subsingleton G], P G) →
(∀ (G : Type u_2) [inst : Group G] [inst_2 : Group.IsNilpotent G], P (G ⧸ Subgroup.center G) → P G) → P G
This theorem is a custom induction principle for nilpotent groups. The base case is a group that is trivial, or a subsingleton. In the induction step, if we assume the inductive hypothesis for the quotient of a group by its center, it follows that the hypothesis holds for the group itself. This induction principle is useful in proving properties that are preserved under quotienting by the center of a group.
More concisely: The theorem is an induction principle stating that if a property holds for the quotient of a nilpotent group by its center, then it holds for the group itself.
|