Fitting's Theorem (nilpotent normal subgroups)

If H and K are nilpotent normal subgroups of a group G, then H ⊔ K is nilpotent. Moreover, if H has class h and K has class k, then the class of H ⊔ K is at most h + k.

This file implements the proof via a semiring structure on normal subgroups with addition given by ⊔ and multiplication by the commutator ⁅·, ·⁆, and translates bounds on lower central series into estimates on powers in that semiring.

theorem Ring.foldl_range {α : Type u_1} {n : ℕ} (s t : Finset ℕ) (init : α) (f : α → ℕ → Finset ℕ → α) (h : ∀ i < n, ∀ (a : α), f a i s = f a i t) : List.foldl (fun (tot : α) (i : ℕ) => f tot (i + 1) s) init (List.range (n - 1)) = List.foldl (fun (tot : α) (i : ℕ) => f tot (i + 1) t) init (List.range (n - 1))

A fold-equivalence over List.range (n - 1) when the step function depends only on values < n and the membership predicate agrees on two finite sets.

@[implicit_reducible]

def Ring.instHPowPNat_fittingsTheorem {M : Type u_1} [Mul M] : HPow M ℕ+ M

Power by positive naturals on a (non-unital) semiring-like structure, defined by left multiplication recursion.

We use ℕ+ for the exponent since the ground ring does not necessarily contain a unit.

Equations

• Ring.instHPowPNat_fittingsTheorem = { hPow := fun (m : M) (n : ℕ+) => Nat.leRec m (fun ⦃x : ℕ⦄ (x_1 : 1 ≤ x) (m' : M) => m * m') ⋯ }

@[simp]

theorem Ring.pow_one {M : Type u_1} [Mul M] (a : M) : a ^ 1 = a

theorem Ring.pow_succ {M : Type u_1} [Mul M] (n : ℕ+) (a : M) : a ^ (n + 1) = a * a ^ n

Successor step for positive power.

def Ring.factor {M : Type u_1} [Mul M] (H K : M) (n : ℕ) (s : Finset ℕ) : M

Form the product of n factors, where the i-th one is H, if i ∈ s and it is K otherwise.

Equations

• Ring.factor H K n s = List.foldl (fun (tot : M) (i : ℕ) => tot * if i + 1 ∈ s then H else K) (if 0 ∈ s then H else K) (List.range (n - 1))

theorem Ring.factor_succ {M : Type u_1} [Mul M] {H K : M} {n : ℕ} (hn : n ≠ 0) (s : Finset ℕ) : factor H K (n + 1) s = factor H K n s * if n ∈ s then H else K

One-step recursion for factor.

@[simp]

theorem Ring.factor_zero {M : Type u_1} [Mul M] {H K : M} (s : Finset ℕ) : factor H K 0 s = if 0 ∈ s then H else K

theorem Ring.factor_eq_factor_of {M : Type u_1} [Mul M] {H K : M} {n : ℕ} (hn : n ≠ 0) (s t : Finset ℕ) (h : ∀ i < n, i ∈ s ↔ i ∈ t) : factor H K n s = factor H K n t

If membership in s and t agrees below n, then the corresponding factors agree.

@[reducible, inline]

abbrev Ring.castRangeSucc (n : ℕ) : ↥(Finset.range n) → ↥(Finset.range (n + 1))

The canonical embedding range n ↪ range (n+1).

Equations

• Ring.castRangeSucc n ⟨a, ha⟩ = ⟨a, ⋯⟩

theorem Ring.sum_factor_filter_eq {R : Type u_1} [NonUnitalNonAssocCommSemiring R] {H K : R} (n : ℕ+) (p : Finset ↥(Finset.range (↑n + 1)) → Prop) [DecidablePred p] (hp : (∀ (i : Finset ↥(Finset.range (↑n + 1))), p i ↔ ⟨↑n, ⋯⟩ ∈ i) ∨ ∀ (i : Finset ↥(Finset.range (↑n + 1))), p i ↔ ⟨↑n, ⋯⟩ ∉ i) : ∑ x : Finset ↥(Finset.range (↑n + 1)) with p x, factor H K (↑n) (Finset.image Subtype.val x) = ∑ s : Finset ↥(Finset.range ↑n), factor H K (↑n) (Finset.image Subtype.val s)

Reindexing a sum over subsets of range (n+1) depending on whether n is selected.

theorem Ring.pow_add_eq_sum_factor {R : Type u_1} [NonUnitalNonAssocCommSemiring R] {H K : R} (n : ℕ+) : (H + K) ^ n = ∑ s : Finset ↥(Finset.range ↑n), factor H K (↑n) (Finset.image Subtype.val s)

A nonassociative binomial-style expansion: (H + K) ^ n is the sum over subsets s ⊆ {0,…,n-1} of the corresponding factor.

theorem Ring.factor_eq_factor_compl {R : Type u_1} [NonUnitalNonAssocCommSemiring R] {H K : R} {n : ℕ} (hn : n ≠ 0) (s : Finset ℕ) : factor H K n s = factor K H n (Finset.range n \ s)

factor is invariant under complement in range n after swapping H and K.

theorem Ring.pow_antitone {R : Type u_1} [NonUnitalNonAssocCommSemiring R] [PartialOrder R] (H : R) (hmul : ∀ (J K : R), J * K ≤ K) : Antitone fun (n : ℕ+) => H ^ n

If J * K ≤ K holds for all J, K, then the power map n ↦ H ^ n is antitone in ℕ+.

theorem Ring.factor_le_left {R : Type u_1} [NonUnitalNonAssocCommSemiring R] [PartialOrder R] [MulPosMono R] {H : R} (K : R) (H0 : 0 ≤ H) (n : ℕ) (s : Finset ℕ) (hs : {x ∈ s | x < n}.Nonempty) (hmul : ∀ (J K : R), J * K ≤ K) : factor H K n s ≤ H ^ ⟨{x ∈ s | x < n}.card, ⋯⟩

Upper bound in terms of powers of H when at least one index < n chooses H.

theorem Ring.factor_nonneg_of_nonneg {R : Type u_1} [NonUnitalNonAssocCommSemiring R] [PartialOrder R] [MulPosMono R] {H K : R} (H0 : 0 ≤ H) (K0 : 0 ≤ K) (n : ℕ+) (s : Finset ℕ) : 0 ≤ factor H K (↑n) s

Nonnegativity of factor when H, K ≥ 0.

theorem Ring.factor_le_right {R : Type u_1} [NonUnitalNonAssocCommSemiring R] [PartialOrder R] [MulPosMono R] (H : R) {K : R} (K0 : 0 ≤ K) (n : ℕ) (s : Finset ℕ) (hs : {x ∈ Finset.range n \ s | x < n}.Nonempty) (hmul : ∀ (J K : R), J * K ≤ K) : factor H K n s ≤ K ^ ⟨{x ∈ Finset.range n \ s | x < n}.card, ⋯⟩

Upper bound in terms of powers of K when at least one index < n chooses K.

theorem Ring.factor_eq_zero_of_le {R : Type u_1} [NonUnitalNonAssocCommSemiring R] [PartialOrder R] [MulPosMono R] {H K : R} (H0 : 0 ≤ H) (K0 : 0 ≤ K) (hmul : ∀ (J K : R), J * K ≤ K) (nh nk : ℕ+) (s : Finset ℕ) (hH : H ^ nh = 0) (hK : K ^ nk = 0) : factor H K (↑nh + ↑nk - 1) s = 0

Vanishing of a factor when enough H-steps or K-steps vanish.

theorem Ring.pow_add_eq_zero_of_le {R : Type u_1} [NonUnitalNonAssocCommSemiring R] [PartialOrder R] [MulPosMono R] {H K : R} (H0 : 0 ≤ H) (K0 : 0 ≤ K) (hmul : ∀ (J K : R), J * K ≤ K) (nh nk : ℕ+) (hH : H ^ nh = 0) (hK : K ^ nk = 0) : (H + K) ^ (nh + nk - 1) = 0

The vanishing of the power of a binomial, assuming enough vanishing and inequalities.

theorem Subgroup.map_subtype_top {G : Type u_1} [Group G] (H : Subgroup G) : map H.subtype ⊤ = H

The image of ⊤ under the inclusion H ↪ G is H itself.

@[simp]

theorem Subgroup.mem_sup_iff_mem_mul_of_normal_left {G : Type u_1} [Group G] {H K : Subgroup G} (g : G) [H.Normal] : g ∈ H ⊔ K ↔ g ∈ ↑H * ↑K

Membership in H ⊔ K equals membership in the product set when H is normal.

theorem Subgroup.commutator_sup_le_sup_commutator_of_normal_left {G : Type u_1} [Group G] (H K L : Subgroup G) (HNorm : H.Normal) (LK : ⁅L, K⁆.Normal) : ⁅L, H ⊔ K⁆ ≤ ⁅L, H⁆ ⊔ ⁅L, K⁆

⁅L, ·⁆ is subadditive over ⊔ on the right when the left factor is normal.

theorem Subgroup.commutator_sup_le_sup_commutator_of_normal_left_other {G : Type u_1} [Group G] (H K L : Subgroup G) : ⁅L, H⁆ ⊔ ⁅L, K⁆ ≤ ⁅L, H ⊔ K⁆

⁅L, ·⁆ is superadditive over ⊔ on the right when the left factor is normal.

theorem Subgroup.commutator_sup_distrib_left_of_normal {G : Type u_1} [Group G] (H K L : Subgroup G) (HNorm : H.Normal) (LNorm : L.Normal) (KNorm : K.Normal) : ⁅L, H ⊔ K⁆ = ⁅L, H⁆ ⊔ ⁅L, K⁆

Commutator distributes over ⊔ on the right when all three subgroups are normal.

See commutator_sup_le_sup_commutator_of_normal_left and commutator_sup_le_sup_commutator_of_normal_left_other for the separate inclusions, with weaker assumptions.

def Subgroup.NormalSubgroups (G : Type u_1) [Group G] : Type u_1

The type of normal subgroups of G.

We endow this type with the semiring structure:

• H + K := H ⊔ K,
• H * K := ⁅H, K⁆.

Equations

• Subgroup.NormalSubgroups G = { H : Subgroup G // H.Normal }

@[implicit_reducible]

instance Subgroup.NormalSubgroups.instNonUnitalNonAssocCommSemiring {G : Type u_1} [Group G] : NonUnitalNonAssocCommSemiring (NormalSubgroups G)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Subgroup.NormalSubgroups.ext_iff {G : Type u_1} [Group G] (H K : NormalSubgroups G) : H = K ↔ ↑H = ↑K

theorem Subgroup.NormalSubgroups.ext {G : Type u_1} [Group G] (H K : NormalSubgroups G) (h : ↑H = ↑K) : H = K

@[simp]

theorem Subgroup.NormalSubgroups.zero_eq_bot {G : Type u_1} [Group G] : ↑0 = ⊥

theorem Subgroup.NormalSubgroups.add_eq_sup {G : Type u_1} [Group G] (H K : NormalSubgroups G) : ↑(H + K) = ↑H ⊔ ↑K

theorem Subgroup.NormalSubgroups.mul_eq_comm {G : Type u_1} [Group G] (H K : NormalSubgroups G) : ↑(H * K) = ⁅↑H, ↑K⁆

@[implicit_reducible]

instance Subgroup.NormalSubgroups.instPartialOrder {G : Type u_1} [Group G] : PartialOrder (NormalSubgroups G)

Order structure induced from inclusion of the underlying subgroups.

Equations

• Subgroup.NormalSubgroups.instPartialOrder = PartialOrder.lift Subtype.val ⋯

@[implicit_reducible]

instance Subgroup.NormalSubgroups.instOrderBot {G : Type u_1} [Group G] : OrderBot (NormalSubgroups G)

Equations

• Subgroup.NormalSubgroups.instOrderBot = { bot := 0, bot_le := ⋯ }

theorem Subgroup.NormalSubgroups.le_iff {G : Type u_1} [Group G] (H K : NormalSubgroups G) : H ≤ K ↔ ↑H ≤ ↑K

instance Subgroup.NormalSubgroups.instAddLeftMono {G : Type u_1} [Group G] : AddLeftMono (NormalSubgroups G)

H ≤ K implies the inequality (C ⊔ H) ≤ (C ⊔ K).

instance Subgroup.NormalSubgroups.instMulRightMono {G : Type u_1} [Group G] : MulRightMono (NormalSubgroups G)

Monotonicity in the right commutator slot.

instance Subgroup.NormalSubgroups.instMulLeftMono {G : Type u_1} [Group G] : MulLeftMono (NormalSubgroups G)

Monotonicity in the left commutator position.

theorem Subgroup.NormalSubgroups.zero_le {G : Type u_1} [Group G] (H : NormalSubgroups G) : 0 ≤ H

theorem Subgroup.NormalSubgroups.pow_eq_lowerCentralSeries_pred {G : Type u_1} [Group G] (k : ℕ+) (H : NormalSubgroups G) : ↑(H ^ k) = (↑H).lowerCentralSeries (↑k - 1)

The k‑th power of a normal subgroup H : NormalSubgroups G is the (k - 1)‑st term of the lower central series of H, computed in the ambient group G.

theorem Subgroup.lowerCentralSeries_eq_zero_of_add {G : Type u_1} [Group G] {nH nK : ℕ} {H K : Subgroup G} [HN : H.Normal] (hH : H.lowerCentralSeries nH = ⊥) [KN : K.Normal] (hK : K.lowerCentralSeries nK = ⊥) : (H ⊔ K).lowerCentralSeries (nH + nK) = ⊥

If the lower central series of H is trivial after nH steps and the lower central series of K is trivial after nK steps, then the lower central series of H ⊔ K is trivial after nH + nK steps.

Assumes that H and K are normal (and would not necessarily be true otherwise).

theorem Subgroup.isNilpotent_sup_of_normal {G : Type u_1} [Group G] (H K : Subgroup G) [HN : H.Normal] [hH : Group.IsNilpotent ↥H] [KN : K.Normal] [hK : Group.IsNilpotent ↥K] : Group.IsNilpotent ↥(H ⊔ K)

Fitting's Theorem: If H and K are nilpotent normal subgroups of G, then H ⊔ K is nilpotent.

theorem Subgroup.nilpotencyClass_sup_le_of_normal {G : Type u_1} [Group G] (H K : Subgroup G) [H.Normal] [Group.IsNilpotent ↥H] [K.Normal] [Group.IsNilpotent ↥K] : have this := ⋯; Group.nilpotencyClass ↥(H ⊔ K) ≤ Group.nilpotencyClass ↥H + Group.nilpotencyClass ↥K

Fitting's Theorem, quantitative form: if H and K are nilpotent normal subgroups of G, then the nilpotency class of H ⊔ K is at most the sum of the nilpotency classes of H and K.

This is the second half of Fitting's theorem; isNilpotent_sup_of_normal is the first half.