Cleanly defining the Fitting subgroup

Stream: new members

[Ryan Smith]

That's maybe not a great title for a post but I'm trying to give the general purpose definition of the Fitting subgroup of an arbitrary group G without assumption of it being finite. So in general this is the subgroup generated by all of the normal nilpotent subgroups of G.

import Mathlib
import Mathlib.GroupTheory.Nilpotent
open Subgroup Group
namespace Subgroup

def nn_subgroups (G : Type*) [Group G] := { K : Subgroup G | K.Normal ∧ IsNilpotent K }

Checking the type of our interim definition shows Set (Subgroup G) like we would expect. We don't have an index for this set of subgroups (presumably there is a result which can axiom of choice this into being for us?), but assuming we could solve that problem we have elements of type Subgroup G and not type Set G. Our endgame would be if we had a Set (Set G) we could define the subgroup we want as ⨆ i, s i.

Is this making things too hard? Can we do this concisely in a single definition rather than employing a temporary definition just to define the set of subgroups we want to close? Is the right approach to coerce from Subgroup G to Set G somehow when we form this union?

[Kevin Buzzard]

sSup (nn_subgroups G) is what you're after.

[Ryan Smith]

That's really interesting, so even though sSup is a set operation it understands that we are talking about the closure in a group theory sense? How does it know about that?

[Kevin Buzzard]

Lean knows that Subgroup G is a complete lattice, so it's a partial order with a meet and a join operator. This structure is all defined in the file Mathlib/Algebra/Group/Subgroup/Lattice.lean if you want to poke around in there. The join of two subgroups is the intersection of all the subgroups containing them both etc etc.

[Kevin Buzzard]

One crazy thing about Lean which took me a while to learn is that it doesn't do magic -- any question you ask of this nature can be answered by reading the code, although it takes some time to get the hang of how to read the code; you can't just look at it on e.g. github, you really need VS Code or equivalent to interact with it. But the bottom line is that it's all just maths, and you can find your way to it by jumping around in the code.

You can start the journey with

variable (G : Type*) [Group G]

#synth CompleteLattice (Subgroup G)

and then click on #synth and you'll see instCompleteLattice in the infoview, then you can ctrl-click on this and jump to the place where the term of type CompleteLattice (Subgroup G) is defined, and read what's going on there.

[Kevin Buzzard]

Ryan Smith said:

even though sSup is a set operation

Aah no no no, sSup is a lattice operation, or even a partially ordered set operation. It's "supremum of a subset of your poset".

[Aaron Liu]

You may be thinking of docs#Set.sUnion, which is a set operation (you can tell because it says Set in the name)

[Matt Diamond]

to be clear, Set.sUnion literally is sSup, just in the specific context of the lattice structure of sets

[Aaron Liu]

Yeah it's just defined as sSup

[Aaron Liu]

But I guess this way you can't accidentally pass in something else