Zulip Chat Archive

Stream: maths

Topic: bundling normal subgroups


view this post on Zulip Kevin Buzzard (Aug 06 2019 at 11:01):

Should normal subgroups be bundled? I am a bit confused about this.

Subsets of a group G are bundled -- they're set G. The general concensus amongst the community is that subgroups of G should also be bundled -- they can be subgroup G. There's a local project at Imperial with bundled subgroups and they're working fine.

But we're venturing into quotients so we need the notion of a normal subgroup. If we also bundle these as normal_subgroup' G then we have the issue that a normal subgroup of G is now not a subgroup. We can put a coercion to subgroups, but then there's sometimes a coercion from subgroups to subsets, and we are ending up with double coercions and things just don't look good.

Thinking about how to solve this made me realise that I don't really understand what's going on. Are we bundling subgroups because they just seem to work better? Is the idea that we bundled submodules and they worked really well? Is there an argument for making normal subgroups a typeclass on subgroups? This feels similar to making subgroups a typeclass on subsets -- which is what the community decided to move away from. What are the disadvantages of letting normal subgroups be a typeclass on bundled subgroups?

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 13:41):

@Chris Hughes do you have an opinion about this? Sorry to bother you.

view this post on Zulip Chris Hughes (Aug 06 2019 at 13:46):

I think that probably bundling normal subgroups will be best. There'll be type class inference problems otherwise with quotient groups. A lot of these decisions depend on what happens in Lean4. Hopefully we'll have unification hints that work nicely.

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 13:46):

Then should there be coercions from normal subgroups to subgroups, and from subgroups to subsets, and from normal subgroups to subsets?

view this post on Zulip Chris Hughes (Aug 06 2019 at 13:48):

Yes, but then there should probably be mem on all of this stuff as well.

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 13:48):

I guess ideal R is bundled ideals and Spec R is bundled prime ideals.

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 13:49):

Oh wow Amelia just pointed out

@[class] def is_prime (I : ideal α) : Prop :=
I     {x y : α}, x * y  I  x  I  y  I

What's going on there? I don't even understand how a definition which isn't a structure can be tagged as a class.

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 13:49):

Is that another way of doing normal subgroups?

view this post on Zulip Chris Hughes (Aug 06 2019 at 13:50):

It's possible but a bad idea, but I can't remember why. Something to do with it being semireducible.

view this post on Zulip Mario Carneiro (Aug 06 2019 at 14:59):

I think normal should be a predicate on subgroups, and quotient groups should be defined relative to arbitrary sets or arbitrary subgroups (not sure which) by taking the normal closure

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 15:00):

You can make a quotient by a non-normal subgroup, it's just a set with an action of the big group

view this post on Zulip Mario Carneiro (Aug 06 2019 at 15:00):

it's not a group though

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 15:01):

No. What do you mean by predicate? No type class inference at all?

view this post on Zulip Mario Carneiro (Aug 06 2019 at 15:01):

right

view this post on Zulip Mario Carneiro (Aug 06 2019 at 15:01):

I'm not positive, it depends on how this predicate is used

view this post on Zulip Mario Carneiro (Aug 06 2019 at 15:02):

when do you need normality anyway?

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 15:02):

When you're teaching undergraduates group theory

view this post on Zulip Mario Carneiro (Aug 06 2019 at 15:02):

a predicate is preferable for teaching undergrads

view this post on Zulip Mario Carneiro (Aug 06 2019 at 15:02):

typeclass inference is confusing

view this post on Zulip Kevin Buzzard (Aug 06 2019 at 15:04):

Fair point

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 15:19):

OK, now #2140 is close to hitting mathlib (hopefully -- any reviews welcome) we need to make a decision on normal subgroups. There are two possibilities: (1) bundling (i.e. a new type normal_subgroup G) (2) a predicate is_normal on subgroup G which isn't a class (3) a predicate is_normal on subgroup G` which is a class.

Mario asked "when do you need normality anyway?" and my initial answer was "teaching" but now it's "research" -- we use quotient groups in the perfectoid project, and currently we're quotienting out by an unbundled normal subgroup. I'd like to get started on this but I don't know what to do. Mario suggested quotienting out by general subsets (defined to be quotienting out by the normal closure) and because I don't actually need normal subgroups per se, but rather quotient groups, this would also be good for me.

I am completely happy if the answer is "make a random choice and see how it works out" but what I want to avoid is me refactoring group_theory/quotient_group.lean and then in the PR process someone saying "you should have done it another way".

In fact maybe this is not even the right question! I don't even care about normal subgroups. I care about quotient groups. Currently the set-up is

quotient_group.quotient : Π {α : Type u_1} [_inst_1 : group α] (s : set α) [_inst_2 : is_subgroup s], Type u_1

(this is just the type of cosets) and then an instance of type

Π {G : Type u_1} [_inst_1 : group G] (N : set G) [_inst_2 : normal_subgroup N], group (quotient N)

My question is simple: should I PR some more lemmas about quotient groups, or should I take the opportunity to refactor quotient groups in some way? If so, how? I would like to come to a firm decision before starting the PR.

view this post on Zulip Reid Barton (Apr 18 2020 at 15:20):

You should randomly choose (1)

view this post on Zulip Reid Barton (Apr 18 2020 at 15:21):

But it sounds like this is what you have already?

view this post on Zulip Reid Barton (Apr 18 2020 at 15:21):

Oh wait, no I misread.

view this post on Zulip Reid Barton (Apr 18 2020 at 15:25):

In perfectoid spaces, are you taking quotients of abelian groups?

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 15:26):

Yes

view this post on Zulip Kevin Buzzard (Apr 18 2020 at 15:27):

but I decided not to mention this because I thought it would muddy the water.


Last updated: May 18 2021 at 07:19 UTC