normal subgroups

Stream: Is there code for X?

[Adam Topaz]

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]

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]

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

[Adam Topaz]

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

[Adam Topaz]

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

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

[Adam Topaz]

Similar to

import ring_theory.ideal.basic

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

#check I.quotient

[Kevin Buzzard]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Kevin Buzzard]

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]

Well.... this is discouraging:

variables (G : Type*) [group G]

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

[Patrick Lutz]

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]

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

[Patrick Lutz]

I meant the problem that subgroup.normal is Prop valued

[Patrick Lutz]

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

[Alex J. Best]

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

[Adam Topaz]

@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]

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]

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]

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.

[Adam Topaz]

Oh, I see.

[Patrick Lutz]

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]

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]

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

[Alex J. Best]

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]

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]

Or maybe I'm missing an import?

[Alex J. Best]

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]

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

[Kevin Buzzard]

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

[Jason KY.]

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]

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]

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

[Kevin Buzzard]

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

[Johan Commelin]

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]

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]

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

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

[Patrick Lutz]

yeah, that would be great

[Patrick Lutz]

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

[Thomas Browning]

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

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

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]

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]

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]

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

[Patrick Lutz]

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

[Patrick Lutz]

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