stabilizers and maximal subgroups

Stream: new members

[Jireh Loreaux]

Note though, we already have pointwise stabilizers by group actions: docs#MulAction.Stabilizer.submonoid

[Jireh Loreaux]

As for Subgroup.IsMaximal, can you just use docs#IsCoatom ?

[Peiran Wu]

Jireh Loreaux said:

Note though, we already have pointwise stabilizers by group actions: docs#MulAction.Stabilizer.submonoid

I believe that is the stabilizer of a single point. A pointwise stabilizer is the intersection of point stabilizers.

[Peiran Wu]

Jireh Loreaux said:

As for Subgroup.IsMaximal, can you just use docs#IsCoatom ?

Ideal.IsMaximal is precisely a wrapper of IsCoatom. Is that not the way to go?

[Peiran Wu]

(deleted)

[Jireh Loreaux]

Peiran Wu said:

Jireh Loreaux said:

Note though, we already have pointwise stabilizers by group actions: docs#MulAction.Stabilizer.submonoid

I believe that is the stabilizer of a single point. A pointwise stabilizer is the intersection of point stabilizers.

That's ⨅ a : G, MulAction.Stabilizer.submonoid G a. (Oh and sorry, I think docs#MulAction.Stabilizer is actually the subgroup)

[Jireh Loreaux]

Peiran Wu said:

Jireh Loreaux said:

As for Subgroup.IsMaximal, can you just use docs#IsCoatom ?

Ideal.IsMaximal is precisely a wrapper of IsCoatom. Is that not the way to go?

I would say it's only the way to go if it's worth developing a separate API. In the case of Ideal, it's worth it because we want it to be a class so that we can have type class inference.

[Notification Bot]

7 messages were moved here from #new members > permission to push to GitHub by Jireh Loreaux.

[Peiran Wu]

Jireh Loreaux said:

That's ⨅ a : G, MulAction.Stabilizer.submonoid G a. (Oh and sorry, I think docs#MulAction.Stabilizer is actually the subgroup)

Yes, that's the definition I have as well, along with several simp lemmas. I'm just laying some ground work so that I won't have to keep writing down the indexed infimum

[Peiran Wu]

Jireh Loreaux said:

I would say it's only the way to go if it's worth developing a separate API. In the case of Ideal, it's worth it because we want it to be a class so that we can have type class inference.

I see. I do have plan to use the maximality of subgroups and minimality of normal subgroups extensively, with a distant goal of formalizing the O'Nan-Scott theorem on the classification of permtutation groups. But I'm happy to hold off doing this bit and see if we actually need it.

[Peiran Wu]

Just accepted the invitation. Thanks! @Jireh Loreaux

[Jireh Loreaux]

Great! Sorry, I wasn't trying to deter you from doing useful things, I just wanted to make sure you were sufficiently familiar with the library to know these things existed. If you feel these things are necessary, feel free to PR them. As for maximality, I would say the key question to ask is this: "do we need to be able to use type class inference to conclude a subgroup is maximal"? If not, then I suspect docs#IsCoatom is the preferred way to go about this.

[Anatole Dedecker]

As for maximality, I would say the key question to ask is this: "do we need to be able to use type class inference to conclude a subgroup is maximal"? If not, then I suspect docs#IsCoatom is the preferred way to go about this.

To expand on this, the typical example is docs#Ideal.Quotient.field where the typeclass systems needs the maximality. I'm not sure this would be particularly useful for subgroups, but maybe it could be for maximal normal subgroups, in which case one gets a docs#IsSimpleGroup. Even then, I'm no group theorist so I can't tell how often this is used.

[Peiran Wu]

That's all understood Jireh; no worries. I didn't realise the subtlety surrounding the necessity of type class inference.

[Peiran Wu]

Anatole Dedecker said:

I'm not sure this would be particularly useful for subgroups, but maybe it could be for maximal normal subgroups, in which case one gets a docs#IsSimpleGroup.

Thanks for the elaboration. In fact, given your example, this will be particularly useful for subgroups, since a transitive group action is primitive iff the point stabilizer is a maximal subgroup! Primitive permutation groups are the "simple groups" of permutation group theory.

[Peiran Wu]

And primitivity was my original motivation for adding Subgroup.IsMaximal

[Anatole Dedecker]

The fact that the world "primitive" pops up makes me realize that you should absolutely talk to @Antoine Chambert-Loir about all of the work he's done (outside of mathlib for now) around group actions and permutation groups.

[Anatole Dedecker]

Peiran Wu said:

Anatole Dedecker said:

I'm not sure this would be particularly useful for subgroups, but maybe it could be for maximal normal subgroups, in which case one gets a docs#IsSimpleGroup.

Thanks for the elaboration. In fact, given your example, this will be particularly useful for subgroups, since a transitive group action is primitive iff the point stabilizer is a maximal subgroup! Primitive permutation groups are the "simple groups" of permutation group theory.

I think that's a bit different, because you probably wouldn't want the typeclass system to do that for you, right? Or do you have a potential instance in mind?

[Peiran Wu]

Anatole Dedecker said:

I think that's a bit different, because you probably wouldn't want the typeclass system to do that for you, right? Or do you have a potential instance in mind?

Well my current research involves particular families of maximal subgroups of the symmetric/alternating groups, and the corresponding primitive actions. But I'm not going to be formalising my research yet. I'll need to think more about this.

[Peiran Wu]

Anatole Dedecker said:

The fact that the world "primitive" pops up makes me realize that you should absolutely talk to Antoine Chambert-Loir about all of the work he's done (outside of mathlib for now) around group actions and permutation groups.

That's very interesting. He seems quite active here on Zulip; it'd be great to find out more about what he's done.

[Antoine Chambert-Loir]

Indeed, I have formalized a great deal of primitive group actions, Jordan's theorem, the intransitive maximal subgroups of An and Sn, Iwasawa's primitivity criterion... I now need to translate this to lean4...

[Peiran Wu]

Antoine Chambert-Loir said:

Indeed, I have formalized a great deal of primitive group actions, Jordan's theorem, the intransitive maximal subgroups of An and Sn, Iwasawa's primitivity criterion... I now need to translate this to lean4...

Oh that's great. Are you looking to add some of this into mathlib after porting it to Lean 4? I would be interested in contributing to the porting and merging as well. It would be nice to have it in mathlib, so I and potentially some of the other permutation group theorists here at St Andrews can expand on the work.

[Peiran Wu]

(deleted)