Zulip Chat Archive

Stream: new members

Topic: Composition series for finite groups


view this post on Zulip 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: )

view this post on Zulip Kevin Buzzard (Jan 04 2021 at 19:01):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 04 2021 at 19:04):

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

view this post on Zulip Patrick Lutz (Jan 04 2021 at 19:06):

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

view this post on Zulip Kevin Buzzard (Jan 04 2021 at 19:06):

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

view this post on Zulip Patrick Lutz (Jan 04 2021 at 19:07):

yeah

view this post on Zulip 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

view this post on Zulip 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)?

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Lutz (Jan 04 2021 at 19:21):

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

view this post on Zulip 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 N\mathbb{N} to some set), instead they are elements of some inductive type. But you could extract a sequence from them if you wanted.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Hanting Zhang (Jan 04 2021 at 19:31):

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

view this post on Zulip Patrick Lutz (Jan 04 2021 at 19:31):

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

view this post on Zulip Patrick Lutz (Jan 04 2021 at 19:31):

or (G : Type*) [group G]

view this post on Zulip 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 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.

view this post on Zulip 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

view this post on Zulip 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 :-) )

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Lutz (Jan 04 2021 at 19:59):

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

view this post on Zulip 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

view this post on Zulip Patrick Lutz (Jan 04 2021 at 20:01):

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

view this post on Zulip 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