bundling normal subgroups

Stream: maths

[Kevin Buzzard]

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]

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

[Chris Hughes]

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]

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

[Chris Hughes]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

Is that another way of doing normal subgroups?

[Chris Hughes]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

it's not a group though

[Kevin Buzzard]

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

[Mario Carneiro]

right

[Mario Carneiro]

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

[Mario Carneiro]

when do you need normality anyway?

[Kevin Buzzard]

When you're teaching undergraduates group theory

[Mario Carneiro]

a predicate is preferable for teaching undergrads

[Mario Carneiro]

typeclass inference is confusing

[Kevin Buzzard]

Fair point

[Kevin Buzzard]

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]

You should randomly choose (1)

[Reid Barton]

But it sounds like this is what you have already?

[Reid Barton]

Oh wait, no I misread.

[Reid Barton]

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

[Kevin Buzzard]

Yes

[Kevin Buzzard]

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