# Zulip Chat Archive

## Stream: maths

### Topic: bundling normal subgroups

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

#### Kevin Buzzard (Aug 06 2019 at 13:41):

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

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

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

#### Chris Hughes (Aug 06 2019 at 13:48):

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

#### Kevin Buzzard (Aug 06 2019 at 13:48):

I guess `ideal R`

is bundled ideals and `Spec R`

is bundled prime ideals.

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

#### Kevin Buzzard (Aug 06 2019 at 13:49):

Is that another way of doing normal subgroups?

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

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

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

#### Mario Carneiro (Aug 06 2019 at 15:00):

it's not a group though

#### Kevin Buzzard (Aug 06 2019 at 15:01):

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

#### Mario Carneiro (Aug 06 2019 at 15:01):

right

#### Mario Carneiro (Aug 06 2019 at 15:01):

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

#### Mario Carneiro (Aug 06 2019 at 15:02):

when do you need normality anyway?

#### Kevin Buzzard (Aug 06 2019 at 15:02):

When you're teaching undergraduates group theory

#### Mario Carneiro (Aug 06 2019 at 15:02):

a predicate is preferable for teaching undergrads

#### Mario Carneiro (Aug 06 2019 at 15:02):

typeclass inference is confusing

#### Kevin Buzzard (Aug 06 2019 at 15:04):

Fair point

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

#### Reid Barton (Apr 18 2020 at 15:20):

You should randomly choose (1)

#### Reid Barton (Apr 18 2020 at 15:21):

But it sounds like this is what you have already?

#### Reid Barton (Apr 18 2020 at 15:21):

Oh wait, no I misread.

#### Reid Barton (Apr 18 2020 at 15:25):

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

#### Kevin Buzzard (Apr 18 2020 at 15:26):

Yes

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