# Zulip Chat Archive

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

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

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

#### 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

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

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

- Any group isomorphic to
`G`

can count as a normal series for`G`

(think of it as the trivial normal series of length 1) - 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:

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 `inclusion`

is 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