Zulip Chat Archive

Stream: Is there code for X?

Topic: normal subgroups


view this post on Zulip 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.

view this post on Zulip 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]

view this post on Zulip Thomas Browning (Nov 11 2020 at 20:41):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 21:49):

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

view this post on Zulip Adam Topaz (Nov 11 2020 at 21:58):

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

view this post on Zulip 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)

view this post on Zulip Adam Topaz (Nov 11 2020 at 21:59):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Nov 11 2020 at 23:00):

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

view this post on Zulip Patrick Lutz (Nov 11 2020 at 23:01):

I meant the problem that subgroup.normal is Prop valued

view this post on Zulip Patrick Lutz (Nov 11 2020 at 23:02):

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

view this post on Zulip Alex J. Best (Nov 11 2020 at 23:31):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Lutz (Nov 11 2020 at 23:46):

Adam Topaz said:

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.

view this post on Zulip Adam Topaz (Nov 11 2020 at 23:46):

Oh, I see.

view this post on Zulip 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

view this post on Zulip 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".

view this post on Zulip Adam Topaz (Nov 11 2020 at 23:49):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Adam Topaz (Nov 12 2020 at 00:27):

Or maybe I'm missing an import?

view this post on Zulip 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

view this post on Zulip Alex J. Best (Nov 12 2020 at 00:52):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Nov 12 2020 at 07:16):

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

view this post on Zulip Kevin Buzzard (Nov 12 2020 at 07:17):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Jason KY. (Nov 12 2020 at 07:43):

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

view this post on Zulip Patrick Lutz (Nov 12 2020 at 07:44):

yeah, that would be great

view this post on Zulip 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

view this post on Zulip 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".

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Patrick Lutz (Nov 23 2020 at 07:14):

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

view this post on Zulip Patrick Lutz (Nov 23 2020 at 07:14):

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

view this post on Zulip 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