Composition series for finite groups

Stream: new members

[Hanting Zhang]

What would be the best way to define composition series on finite groups? I'm thinking of this:

def composition_series [fintype G] : ℕ → subgroup G
| 0 := ⊤
| (n + 1) := maximal_normal_subgroup (composition_series n)

It should be possible to define maximal_normal_subgroup by creating a maximal element of { N : subgroup G // N.normal }, but I'm not sure how to do that. Presumably there's something in the order theory files, but I haven't been able to find anything. (I don't really know what I'm looking for. :grimacing: )

[Kevin Buzzard]

At least two other people have been thinking about this recently. @Thomas Browning @Jason KY. ?

[Aaron Anderson]

You probably want to use is_coatom somewhere. I'm not sure how much API we have on the lattice of normal subgroups, though.

[Thomas Browning]

@Patrick Lutz and I haven't done composition series specifically. However, @Brendan Seamas Murphy did composition series a long time ago: https://github.com/Shamrock-Frost/jordan-holder/blob/master/src/composition_series.lean

[Kevin Buzzard]

In my mind this is not a completely straightforward problem. If $1\subset G_1\subset G_2\subset G_3\subset\cdots\subset G_n=G$ then it's very natural for the $G_i$ to be subgroups of $G$ but you also want $G_i$ to be a subgroup of $G_j$ too.

[Patrick Lutz]

@Kevin Buzzard Maybe just specify embeddings rather than require the $G_i$ to be subgroups?

[Kevin Buzzard]

So you can go "full type" and have $G_i$ all being types and there being maps between them

[Patrick Lutz]

yeah

[Patrick Lutz]

Thomas Browning said:

Patrick Lutz and I haven't done composition series specifically. However, Brendan Seamas Murphy did composition series a long time ago: https://github.com/Shamrock-Frost/jordan-holder/blob/master/src/composition_series.lean

To give a little more detail: we've proved some stuff about solvable groups (along with Jordan Brown), but it seemed easier to us to define solvable in terms of the derived series of a group rather than in terms of composition series. The definition of derived series should be merged into mathlib soon though

[Patrick Lutz]

@Hanting Zhang Your definition of composition_series seems to be trying to define a unique sequence associated to a finite group. But can't a group have multiple different composition series (because there is not always a unique maximal normal subgroup)?

[Patrick Lutz]

So maybe instead you should define a type of composition series and prove that it's nonempty (it looks like the repository that Thomas linked to takes a similar approach)

[Hanting Zhang]

I can't really understand what @Brendan Seamas Murphy has done at first glance. The category theory is getting lost on me. Would the type be list subgroup G? I don't really understand what "full type" means either.

[Patrick Lutz]

Also, not sure if this is the type of lemma you are asking about, but mathlib does have finset.exists_maximal which shows that any finite subset of a preorder has a maximal element

[Patrick Lutz]

https://leanprover-community.github.io/mathlib_docs/data/fintype/basic.html#finset.exists_maximal

[Patrick Lutz]

Hanting Zhang said:

I can't really understand what Brendan Seamas Murphy has done at first glance. The category theory is getting lost on me. Would the type be list subgroup G? I don't really understand what "full type" means either.

Here's what's going on I think. First, he defines a type consisting of all "normal series" of a group

inductive normal_series (T : Group.{u}): Group.{u} → Type (u+1)
| initial {} : ∀ {T'}, (T' ≅ T) → normal_series T'
| step : ∀ {H G K : Group.{u}},
       SES H G K
       → normal_series H
       → normal_series G

Basically this is saying that if G is a group then

1. Any group isomorphic to G can count as a normal series for G (think of it as the trivial normal series of length 1)
2. If H embeds into G and its image is a normal subgroup then if you have a normal series on H you also have a normal series on G which you get by appending H to the beginning

One slightly tricky thing here is that the elements of this type are not sequences in the usual sense (i.e. they are not functions from $\mathbb{N}$ to some set), instead they are elements of some inductive type. But you could extract a sequence from them if you wanted.

[Patrick Lutz]

Next, he defines a predicate on the normal_series type that says if the given normal series is a composition series

[Patrick Lutz]

def is_composition_series
  {G : Group} (σ : normal_series 1 G)
  := list.foldr (∧) true
     $ list.map (λ K : Group, simple_group K ∧ ¬ subsingleton K)
     $ factors σ

Basically this is just saying that if σ is a normal series for G it is a composition series if at every step in the formation of σ, if you quotient by the subgroup that was used, you get a simple group

[Hanting Zhang]

What is the analog of Group.{u} in Lean currently? I'm guessing it means the Type of all groups in u.

[Hanting Zhang]

Also, thanks for all the explanations, they're very helpful.

[Patrick Lutz]

I would normally write (G : Type u) [group G]

[Patrick Lutz]

or (G : Type*) [group G]

[Jason KY.]

Kevin Buzzard said:

At least two other people have been thinking about this recently. Thomas Browning Jason KY. ?

I messed around with derived series a while back and I defined it in a way similar to what Zhang has

def derived_subgroup (G : Type*) [group G] : ℕ → subgroup G
| 0       := ⊤
| (n + 1) := (commutator $ derived_subgroup n).map (derived_subgroup n).inclusion

where inclusionis the following homomorphism

def subgroup.inclusion {G : Type*} [group G] (H : subgroup G) : H →* G :=
  ⟨λ h, h.1, rfl, λ _ _, rfl⟩

I couldn't find a nice way of extending this to composition series however.

[Hanting Zhang]

I think I'm getting somewhere, although the definition isn't done:

inductive normal_series (T : Type u) [group T] : Type u → Type (u + 1)
| init {} : ∀ T' [group T'], T' ≃* T → normal_series T'
| step : ∀ {H G K : Type u} [group H] [group G] [group K],
  (∃ f : H →* G, function.injective f ∧ /- H identifies as a normal subgroup of G -/ )
  normal_series H → normal_series G

[Kevin Buzzard]

Hanting Zhang said:

What is the analog of Group.{u} in Lean currently? I'm guessing it means the Type of all groups in u.

In Lean, Group would be the category of all groups (in universe u) (assuming they made this category by now :-) )

[Patrick Lutz]

@Jason KY. FYI, there is currently a PR underway to mathlib to add derived series (#5565). Also there will probably soon be a PR coming to add something like your inclusion

[Hanting Zhang]

Oh no, is it better to work with Group then? This is getting much harder than I thought it would be.

[Patrick Lutz]

@Jason KY. Actually I got a little confused. Your inclusion is just subgroup.subtype which is already in mathlib

[Patrick Lutz]

but soon there will be a map from subgroup H to subgroup G (see here)

[Jason KY.]

I was just messing around in lean since I was learning the material myself so its not surprising that I missed that definition :p

[Patrick Lutz]

Yeah, I think I only discovered it by accident (using library_search or something)

[Kevin Buzzard]

I am not sure that using category theory will help here