## Stream: Is there code for X?

### Topic: normal subgroups

#### Adam Topaz (Nov 11 2020 at 20:38):

What's the idiomatic way to speak about the type of all normal subgroups of a group? We have subgroup G for the type of (bundled) subgroups of G, and subgroup.normal which is a Prop-valued class. There is also a deprecated normal_subgroup. It's unclear to me what the best way to speak about the type of all normal subgroups should be.

#### Adam Topaz (Nov 11 2020 at 20:41):

I guess what I'm looking for is something similar to the following structure:

variables (G : Type*) [group G]

structure normal_subgroup :=
(to_subgroup : subgroup G)
[is_normal : subgroup.normal to_subgroup]


#### Thomas Browning (Nov 11 2020 at 20:41):

maybe subtype (subgroup.normal) (or something like that)?

#### Adam Topaz (Nov 11 2020 at 20:48):

Sure, that subtype would work, but I want something that plays well with the group theory API

#### Adam Topaz (Nov 11 2020 at 20:49):

I guess it doesn't exist? I want to be able to write

variable (H : normal_subgroup G)
#check H.quotient


#### Adam Topaz (Nov 11 2020 at 20:50):

Similar to

import ring_theory.ideal.basic

variables (A : Type*) [comm_ring A] (I : ideal A)

#check I.quotient


#### Kevin Buzzard (Nov 11 2020 at 21:49):

Can't you just make H a subgroup with a [normal] hypothesis?

#### Adam Topaz (Nov 11 2020 at 21:58):

@Kevin Buzzard I'd like to construct the profinite completion of a group.

#### Adam Topaz (Nov 11 2020 at 21:58):

So I need the full diagram of finite quotients of a group (and take its limit to be the profinite completion)

#### Adam Topaz (Nov 11 2020 at 21:59):

And I need some way to write down the indexing set of this limit

#### Kevin Buzzard (Nov 11 2020 at 22:14):

I guess I'd just with the subtype. Somehow the typeclass system gets you into these situations. Someone somewhere decreed that semiring and ring and integral_domain were somehow "basic" and everything else like DVR is Prop-valued and goes on top. Similarly subsets and subgroups have been deemed basic and are bundled, and normal subgroups are a prop on top. It's not clear that there's a good answer for all this.

#### Adam Topaz (Nov 11 2020 at 22:31):

Well.... this is discouraging:

variables (G : Type*) [group G]

example : subgroup.normal (⊤ : subgroup G) := by apply_instance -- FAILS


#### Patrick Lutz (Nov 11 2020 at 22:57):

I had this same problem recently trying to show that subgroup.normal_closure forms a galois insertion together with the forgetful functor from normal subgroups to subsets.

#### Adam Topaz (Nov 11 2020 at 23:00):

I mean... by tidy solves this, so it's not a big deal.

#### Patrick Lutz (Nov 11 2020 at 23:01):

I meant the problem that subgroup.normal is Prop valued

#### Patrick Lutz (Nov 11 2020 at 23:02):

and I wasn't sure how I should state what I wanted to prove given that

#### Alex J. Best (Nov 11 2020 at 23:31):

This is just a missing instance right, what's discouraging about it? I made #4982

#### Adam Topaz (Nov 11 2020 at 23:41):

@Alex J. Best Like I said, it's not a big deal. @Patrick Lutz It's not so much a problem that normalis Prop valued, but rather that mathlib doesn't currently have "the type of normal subgroups". And if you want to define the normal_closure, that's certainly the natural target for that.

#### Alex J. Best (Nov 11 2020 at 23:44):

Yeah it seems this just got lost in the transition to bundled subgroups, there is a lemma univ_subgroup in deprecated/subgroup.lean anyways

#### Adam Topaz (Nov 11 2020 at 23:45):

The following is slightly more serious :)

import group_theory.quotient_group

variables (G : Type*) [group G]

instance : subgroup.normal (⊤ : subgroup G) := ⟨by tauto⟩

instance blah : fintype (quotient_group.quotient (⊤ : subgroup G)) := sorry


#### Patrick Lutz (Nov 11 2020 at 23:46):

Alex J. Best Like I said, it's not a big deal. Patrick Lutz It's not so much a problem that normalis Prop valued, but rather that mathlib doesn't currently have "the type of normal subgroups". And if you want to define the normal_closure, that's certainly the natural target for that.

mathlib already has a normal closure but it takes values in subgroup G. I wanted to prove some basic properties about it which would follow immediately from the galois_insertion fact. Instead I just proved those properties directly.

Oh, I see.

#### Patrick Lutz (Nov 11 2020 at 23:47):

but I don't fully understand why bundled normal subgroups are bad. Kevin said that he tried it a while ago and his students told him it made things harder so idk

#### Adam Topaz (Nov 11 2020 at 23:49):

Hmmm.... I can't see immediately why bundled normal subgroups would be bad. It seems perfectly natural to have this, or alternatively "the type of all quotients of a group G".

#### Adam Topaz (Nov 11 2020 at 23:49):

Maybe @Kevin Buzzard can tell us what the issues were?

#### Alex J. Best (Nov 12 2020 at 00:21):

import group_theory.quotient_group
import algebra.punit_instances
open quotient_group
noncomputable theory
lemma quotient_top_equiv_unit : quotient (⊤ : subgroup G) ≃* unit := begin
have phi : G →* unit := ⟨λ g, 1, rfl, by simp⟩,
have : phi.ker = ⊤ := by {ext, simp [mem_ker]},
convert quotient_ker_equiv_of_surjective phi _,
all_goals {try {rw this}},
intro,
simp at *,
end
instance blah : fintype (quotient (⊤ : subgroup G)) := fintype.of_equiv _ quotient_top_equiv_unit.to_equiv.symm


#### Adam Topaz (Nov 12 2020 at 00:27):

Nice! I was going this way:

import group_theory.quotient_group

variables (G : Type*) [group G]

instance : subgroup.normal (⊤ : subgroup G) := ⟨by tauto⟩

instance : subsingleton (quotient_group.quotient (⊤ : subgroup G)) :=
begin
constructor,
rintros ⟨⟩ ⟨⟩,
apply quot.sound,
tauto,
end

instance blah : fintype (quotient_group.quotient (⊤ : subgroup G)) := by apply_instance -- FAILS for some reason...


but it looks like there might be another missing instance?

#### Adam Topaz (Nov 12 2020 at 00:27):

Or maybe I'm missing an import?

#### Alex J. Best (Nov 12 2020 at 00:52):

Hmm fintype.of_subsingleton requires a term of that type, so you can do

instance blaha : fintype (quotient_group.quotient (⊤ : subgroup G)) := fintype.of_subsingleton 1


note its a def not an instance

#### Alex J. Best (Nov 12 2020 at 00:52):

If you prove unique (quotient... instead of subsingleton it should work as an instance.

#### Kevin Buzzard (Nov 12 2020 at 06:26):

@Jason KY. Why did you unbundle bundled normal subgroups in our independent from-scratch implementation of group theory?

#### Jason KY. (Nov 12 2020 at 06:59):

I did not do that in the end after playing around with prop valued normal subgroups. I originally had problems with normal subgroups because I had to rewrite a lot of code but the prop valued version was even more difficult to work with I had found.

#### Kevin Buzzard (Nov 12 2020 at 07:12):

Jason, Guilia Carfora and I redeveloped all of group theory in Lean starting from a new definition of group and I regard Jason as one of the experts in the area. If he thinks bundling normal subgroups is better than not bundling them then I don't have any objections to bundling them. I don't think it would be a big refactor. There's a ton of stuff one could do with solvable groups which is not in Lean yet but easily could be, but we should make a decision about normal subgroups before launching in.

#### Johan Commelin (Nov 12 2020 at 07:16):

I'm inclined to say, yes, let's bundle

#### Kevin Buzzard (Nov 12 2020 at 07:17):

Also profinite groups will be useful for all sorts of things eg Galois theory

#### Johan Commelin (Nov 12 2020 at 07:17):

Because we're not only interested in a normal subgroup on its own, but also in the lattice of all normal subgroups. There are (interesting) things to be said about it: Adam mentioned using it as indexing diagram, and of course there is Galois theory

#### Thomas Browning (Nov 12 2020 at 07:38):

Kevin Buzzard said:

Jason, Guilia Carfora and I redeveloped all of group theory in Lean starting from a new definition of group and I regard Jason as one of the experts in the area. If he thinks bundling normal subgroups is better than not bundling them then I don't have any objections to bundling them. I don't think it would be a big refactor. There's a ton of stuff one could do with solvable groups which is not in Lean yet but easily could be, but we should make a decision about normal subgroups before launching in.

@Patrick Lutz @Jordan Brown We'll need to discuss this at Friday's meeting

#### Patrick Lutz (Nov 12 2020 at 07:43):

Kevin Buzzard said:

Jason, Guilia Carfora and I redeveloped all of group theory in Lean starting from a new definition of group and I regard Jason as one of the experts in the area. If he thinks bundling normal subgroups is better than not bundling them then I don't have any objections to bundling them. I don't think it would be a big refactor. There's a ton of stuff one could do with solvable groups which is not in Lean yet but easily could be, but we should make a decision about normal subgroups before launching in.

@Thomas Browning, @Jordan Brown and I have been proving some stuff about commutators and solvable groups recently, which we will eventually need for the abel-ruffini theorem

#### Jason KY. (Nov 12 2020 at 07:43):

I would love to help with the refactor if you guys end up deciding with bundling

#### Patrick Lutz (Nov 12 2020 at 07:44):

yeah, that would be great

#### Patrick Lutz (Nov 12 2020 at 07:44):

As Thomas said, we'll probably talk about it a bit more at our weekly meeting on Friday

#### Thomas Browning (Nov 12 2020 at 07:53):

Also, would it make sense to keep a is_normal_subgroup sort of thing (from which you could construct a bundled normal subgroup)? There are some things that might be better to phrase in terms of is_normal_subgroup. For example in the Galois correspondence you have "this extension is Galois if and only if this subgroup is normal".

#### Jason KY. (Nov 12 2020 at 09:37):

I think thats a great idea. When I worked with bundled normal subgroups I often found myself needing the normal statement as a proposition. I worked around it by simply not writing iff statements and instead make everything into functions but I think having the prop version around is a good idea.

#### Jason KY. (Nov 19 2020 at 13:52):

Hi, is there any update on the normal subgroups? I'm experimenting a bit with composition series right now which works much better with bundled normals subgroups. (Sorry if there exists another Zulip thread on this that I missed)

#### Adam Topaz (Nov 19 2020 at 15:37):

I certainly haven't done anything, and I'm too busy right now to do anything serious in lean for the near future. But if I recall correctly some Berkeley people were planning to take this on? :smiley:

#### Patrick Lutz (Nov 23 2020 at 07:14):

Jason KY. said:

Hi, is there any update on the normal subgroups? I'm experimenting a bit with composition series right now which works much better with bundled normals subgroups. (Sorry if there exists another Zulip thread on this that I missed)

I'm interested in doing this. I've started a mathlib branch (normal_subgroup) to work on this. So far I've defined a bundled version of normal_subgroup and proven some basic stuff about it (mostly copied from other bundled things in mathlib). I haven't yet even fixed all the problems in subgroup.lean that the new definition causes though.

#### Patrick Lutz (Nov 23 2020 at 07:14):

I don't really know what I'm doing btw

#### Patrick Lutz (Nov 23 2020 at 07:14):

but it would be great if you also make changes to this mathlib branch

#### Patrick Lutz (Nov 23 2020 at 07:16):

https://github.com/leanprover-community/mathlib/blob/441ab212216e1956f38ea1594ce1fcfbf1078337/src/group_theory/subgroup.lean#L752

Last updated: May 16 2021 at 05:21 UTC