Fitting subgroup and Frattini subgroup of a finite group

Stream: Is there code for X?

[Ryan Smith]

Are either of these subgroups defined in our group theory library? Moogle doesn't come up with anything. Assuming neither exist, what are conventions about what belongs in a separate file for something like this? In addition to defining both I was thinking of proving some basic results about each which would be useful later on.

[Kim Morrison]

Typing frattini into the search box in VSCode immediately finds the Frattini subgroup?

[Ryan Smith]

You are correct of course :man_facepalming: I'm not sure why it still doesn't show up in Moogle. Even with advanced file search technology I still don't see any sign of the Fitting subgroup?

[Kim Morrison]

Moogle has not been updated in some time, and I think is not really being maintained. LeanSearch is generally better.

[Kim Morrison]

https://leansearch.net/?q=frattini+subgroup

[Thomas Browning]

Yeah, we don't have the fitting subgroup, just the frattini subgroup (docs#frattini).

[Chris Henson]

Kim Morrison said:

Moogle has not been updated in some time, and I think is not really being maintained. LeanSearch is generally better.

Or remember that loogle can search for strings and types together...

[Chris Henson]

@loogle Group, "frattini"

[loogle]

:search: frattini, frattini_characteristic, and 5 more

[Kim Morrison]

I couldn't resist feeding Claude "The Theory of Nilpotent Groups", and seeing what it could do. It's certainly not complete, but a decent start in the fitting branch of kim-em/mathlib4:

/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kim Morrison
-/
import Mathlib.GroupTheory.Nilpotent

/-!
# Fitting's theorem

This file proves Fitting's theorem about nilpotent normal subgroups.

## Main results
* `Subgroup.lowerCentralSeries_sup_eq_bot`: The key technical lemma stating that if
  `lowerCentralSeries M m = ⊥` and `lowerCentralSeries N n = ⊥`, then
  `lowerCentralSeries (M ⊔ N) (m + n) = ⊥`.
* `Subgroup.isNilpotent_sup`: If `M` and `N` are nilpotent normal subgroups of `G`,
  then their supremum `M ⊔ N` is also nilpotent.
* `Subgroup.nilpotencyClass_sup_le`: If `M` has nilpotency class `m` and `N` has
  nilpotency class `n`, then `M ⊔ N` has nilpotency class at most `m + n`.

## References
* [Wikipedia, Fitting's theorem](https://en.wikipedia.org/wiki/Fitting%27s_theorem)
-/

open Subgroup Group

variable {G : Type*} [Group G]

namespace Subgroup

/-- **Fitting's theorem** (explicit bound): If `lowerCentralSeries M m = ⊥` and
`lowerCentralSeries N n = ⊥`, then `lowerCentralSeries (M ⊔ N) (m + n) = ⊥`.

This is the key technical lemma from which both `isNilpotent_sup` and `nilpotencyClass_sup_le`
follow as immediate corollaries.

## Proof Sketch
**Step 1**: By hypothesis, `lowerCentralSeries M m = ⊥` and `lowerCentralSeries N n = ⊥`.
**Step 2**: We need to show `lowerCentralSeries (M ⊔ N) (m + n) = ⊥`. This means showing
every element in this subgroup is the identity.
**Step 3**: Expand `lowerCentralSeries (M ⊔ N) (m + n)` as an (m+n)-fold nested commutator
`⁅M ⊔ N, ⁅M ⊔ N, ⁅..., ⊤⁆...⁆⁆`. Using distributivity of commutators over suprema (since M and N
are normal), this can be written as a supremum of (m+n)-fold commutators where each position
is occupied by either `M` or `N`.
**Step 4**: For any such commutator, by pigeonhole principle, either `M` appears at least `m`
times or `N` appears at least `n` times.
**Step 5**: Key lemma needed: If `lowerCentralSeries M k = ⊥` and `H` is any subgroup, then
iterated commutators `⁅M, ⁅M, ⁅..., ⁅M, H⁆...⁆⁆⁆` (with M appearing k times) equals `⊥`.
This follows from the fact that `lowerCentralSeries M` is preserved under commutators with
normal subgroups.
**Step 6**: Applying Step 5, any commutator with M appearing ≥m times or N appearing ≥n
times must equal `⊥`.
**Step 7**: Since all commutators in the expansion are `⊥`, the entire supremum is `⊥`. -/
theorem lowerCentralSeries_sup_eq_bot (M N : Subgroup G) [M.Normal] [N.Normal]
    (m n : ℕ) (hM : lowerCentralSeries M m = ⊥) (hN : lowerCentralSeries N n = ⊥) :
    lowerCentralSeries (M ⊔ N : Subgroup G) (m + n) = ⊥ := by
  sorry

/-- **Fitting's theorem**: The supremum of two nilpotent normal subgroups is nilpotent.

In group theory, when `M` and `N` are normal subgroups, their supremum `M ⊔ N` equals their
product `{mn | m ∈ M, n ∈ N}`, which is also a normal subgroup. This theorem states that
if both `M` and `N` are nilpotent, then so is their product.

## Proof Sketch

By the definition of `IsNilpotent`, there exist `m` and `n` such that
`lowerCentralSeries M m = ⊥` and `lowerCentralSeries N n = ⊥`. We can take
`m = nilpotencyClass M` and `n = nilpotencyClass N` by `lowerCentralSeries_nilpotencyClass`.
Then `lowerCentralSeries_sup_eq_bot` gives us that
`lowerCentralSeries (M ⊔ N) (nilpotencyClass M + nilpotencyClass N) = ⊥`, which by
`nilpotent_iff_lowerCentralSeries` shows that `M ⊔ N` is nilpotent. -/
instance isNilpotent_sup (M N : Subgroup G) [M.Normal] [N.Normal]
    [IsNilpotent M] [IsNilpotent N] : IsNilpotent (M ⊔ N : Subgroup G) := by
  rw [nilpotent_iff_lowerCentralSeries]
  use nilpotencyClass M + nilpotencyClass N
  apply lowerCentralSeries_sup_eq_bot
  · rw [lowerCentralSeries_eq_bot_iff_nilpotencyClass_le]
  · rw [lowerCentralSeries_eq_bot_iff_nilpotencyClass_le]

/-- **Fitting's theorem** with nilpotency class bound: If `M` has nilpotency class `m` and `N`
has nilpotency class `n`, then `M ⊔ N` has nilpotency class at most `m + n`.

## Proof Sketch

This follows directly from `lowerCentralSeries_sup_eq_bot`:
- Let `m = nilpotencyClass M` and `n = nilpotencyClass N`.
- By `lowerCentralSeries_nilpotencyClass`, we have
  `lowerCentralSeries M m = ⊥` and `lowerCentralSeries N n = ⊥`.
- By `lowerCentralSeries_sup_eq_bot`, we have `lowerCentralSeries (M ⊔ N) (m + n) = ⊥`.
- Therefore, by `lowerCentralSeries_eq_bot_iff_nilpotencyClass_le`, we have
  `Group.nilpotencyClass (M ⊔ N) ≤ m + n`.

Note: The bound is sharp in many cases. For example, when `M` and `N` generate a direct
product, the nilpotency class of `M ⊔ N` is exactly `max(m, n)` by `nilpotencyClass_prod`,
but in general the class can be as large as `m + n`. -/
theorem nilpotencyClass_sup_le (M N : Subgroup G) [M.Normal] [N.Normal]
    [IsNilpotent M] [IsNilpotent N] :
    nilpotencyClass (M ⊔ N : Subgroup G) ≤
      nilpotencyClass M + nilpotencyClass N := by
  rw [← lowerCentralSeries_eq_bot_iff_nilpotencyClass_le]
  have h := lowerCentralSeries_sup_eq_bot M N (nilpotencyClass M) (nilpotencyClass N)
  simp only [lowerCentralSeries_eq_bot_iff_nilpotencyClass_le] at h
  have h' := h (by omega) (by omega)
  exact lowerCentralSeries_eq_bot_iff_nilpotencyClass_le.mpr h'

end Subgroup

Feel free to use or ignore as you please!

[Kim Morrison]

I wonder how Aristotle would perform with that file as input?

[Markus Himmel]

Kim Morrison said:

I wonder how Aristotle would perform with that file as input?

I tried and it didn't manage to fill the sorry.

[Ryan Smith]

I didn't realize that moogle was abandoned, thanks. I've had trouble finding results which people said they were going to merge into mathlib, I thought it was just that their PRs were stuck in purgatory.

[Ryan Smith]

@Kim Morrison Sort of related question: do we have mathlib reviewers focused on specific areas of math / the library? Any approved reviewer could check if a PR passes basic correctness, but it might take deeper knowledge of both lean and the subject area to know if we're formalizing new definitions well for the future. I remember as a particularly thorny example of this Kevin Buzzard had a blog post about going through three iterations of the definition of a scheme to find the right one for use in lean.

[Ruben Van de Velde]

May I point at the section of the readme that lists the maintainers and their areas of interest? https://github.com/leanprover-community/mathlib4?tab=readme-ov-file#maintainers

[Ryan Smith]

Yes!

[Kevin Buzzard]

One thing about the first two definitions of a scheme is that they were not even PRed to mathlib, because along the way it became clear why they were deficient.

One of the roles FLT plays here is that it has a more liberal idea of an acceptable definition (because I am doing the reviewing and I am nowhere near as talented as the pool of all mathlib maintainers/reviewers) and then we play with the definition and see if it works in practice. Ones that do may well get upstreamed to mathlib.

[Kim Morrison]

Fortunately for the topic at hand, getting the definitions for e.g. Fitting subgroups right is much easier than for schemes. While I don't know that we have anyone who is a particular specialist in finite group theory on the reviewer team, I think there is still a long runway of results that we could competently review before there's a problem. And hopefully by that stage we have some Lean-expert finite group theorists who we can appoint as reviewers!

And moreover --- everyone can and should review! Being an "official reviewer" really just means that you have access to some bots that send notifications, and being an official maintainer just means you can tell the bot to merge things, but anyone can say "this looks good" (or otherwise!), and this is both super helpful, and essential for the library to grow in new directions.