## Stream: new members

### Topic: Composition series for finite groups

#### Hanting Zhang (Jan 04 2021 at 19:00):

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: )

#### Aaron Anderson (Jan 04 2021 at 19:01):

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 (Jan 04 2021 at 19:02):

@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 (Jan 04 2021 at 19:04):

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 (Jan 04 2021 at 19:06):

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

#### Kevin Buzzard (Jan 04 2021 at 19:06):

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

yeah

#### Patrick Lutz (Jan 04 2021 at 19:10):

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 (Jan 04 2021 at 19:19):

@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 (Jan 04 2021 at 19:19):

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 (Jan 04 2021 at 19:21):

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 (Jan 04 2021 at 19:21):

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 (Jan 04 2021 at 19:21):

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

#### Patrick Lutz (Jan 04 2021 at 19:27):

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 (Jan 04 2021 at 19:28):

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

#### Patrick Lutz (Jan 04 2021 at 19:30):

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 (Jan 04 2021 at 19:30):

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

#### Hanting Zhang (Jan 04 2021 at 19:31):

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

#### Patrick Lutz (Jan 04 2021 at 19:31):

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

#### Patrick Lutz (Jan 04 2021 at 19:31):

or (G : Type*) [group G]

#### Jason KY. (Jan 04 2021 at 19:49):

Kevin Buzzard said:

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 (Jan 04 2021 at 19:54):

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 (Jan 04 2021 at 19:55):

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 (Jan 04 2021 at 19:55):

@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 (Jan 04 2021 at 19:58):

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

#### Patrick Lutz (Jan 04 2021 at 19:58):

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

#### Patrick Lutz (Jan 04 2021 at 19:59):

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

#### Jason KY. (Jan 04 2021 at 19:59):

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 (Jan 04 2021 at 20:01):

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

#### Kevin Buzzard (Jan 04 2021 at 20:07):

I am not sure that using category theory will help here

Last updated: May 14 2021 at 00:42 UTC