Zulip Chat Archive

Stream: general

Topic: 2nd isomorphism theorem for groups


view this post on Zulip Adrián Doña Mateo (Feb 10 2021 at 17:35):

I needed the 2nd isomorphism theorem for groups (the one that says HN/N ≃* H/(H ∩ N)) to formalise the classical proof of Jordan–Hölder. I couldn't find this (or even a definition of HN) in mathlib so I wrote one up. The main results look like this:

import group_theory.subgroup
import group_theory.quotient_group

variables {G : Type*} [group G]

-- To go in group_theory.subgroup
namespace subgroup

/- The internal product `HN` of a subgroup `H` and a normal subgroup `N` is a subgroup. -/
def prod_normal (H N : subgroup G) [hN : N.normal] : subgroup G :=
{ carrier := { g |  (h  H) (n  N), g = h * n }, ... }

end subgroup

-- To go in group_theory.quotient_group
namespace quotient_group

/- The second isomorphism theorem: given two subgroups `H` and `N` of a group `G`, where `N`
is normal, defines an isomorphism between `H/(H ∩ N)` and `(HN)/N`. -/
noncomputable def quotient_inf_equiv_prod_normal_quotient (H N : subgroup G) [N.normal] :
  quotient ((H  N).comap H.subtype) ≃* quotient (N.comap (H.prod_normal N).subtype) :=
mul_equiv.trans (equiv_quotient_of_eq ker_φ.symm)
  (quotient_ker_equiv_of_surjective (φ H N) φ_surjective)

end quotient_group

I was wondering if this is in the right form for mathlib and whether I should make a pull request.

view this post on Zulip Johan Commelin (Feb 10 2021 at 18:15):

I can believe that this is missing. The code looks right for mathlib.

view this post on Zulip Johan Commelin (Feb 10 2021 at 18:21):

I haven't thought this through, but one idea would be to replace the defn of prod_normal by the subgroup generated by elements of the form h * n. You can then drop the [N.normal] condition. Afterwards, you can write a lemma that says that in case N is normal, the resulting subgroup has the "special" form that is currently your definition.

view this post on Zulip Floris van Doorn (Feb 10 2021 at 18:21):

One remark: { g | ∃ (h ∈ H) (n ∈ N), g = h * n } can be written as H * N if you import data.set.pointwise. See docs#set.has_mul. That might be useful.

view this post on Zulip Johan Commelin (Feb 10 2021 at 18:22):

But you need to cast H and N to sets to do that.

view this post on Zulip Floris van Doorn (Feb 10 2021 at 18:22):

Oh yes, you're right. So maybe that's not so nice.

view this post on Zulip Johan Commelin (Feb 10 2021 at 18:23):

I didn't think this through, but is subgroup.closure ((H : set G) * N) an associative multiplication on subgroup G?

view this post on Zulip Johan Commelin (Feb 10 2021 at 18:23):

If so, that would turn subgroup G into a monoid, which seems like a useful thing to have.

view this post on Zulip Floris van Doorn (Feb 10 2021 at 18:23):

That sounds right.

view this post on Zulip Mario Carneiro (Feb 10 2021 at 18:24):

We could add a has_mul on subgroup to do this, as long as it doesn't have any conflicting meaning in the literature

view this post on Zulip Johan Commelin (Feb 10 2021 at 18:29):

I think has_mul is certainly fine. But I'm wondering if we can get more out of this.

view this post on Zulip Adrián Doña Mateo (Feb 10 2021 at 18:41):

The problem with has_mul would be that H * N is only a subgroup when at least one of the two is normal. Nevermind, I see that taking the closure would fix this.

view this post on Zulip Adrián Doña Mateo (Feb 10 2021 at 18:45):

I'll have a go at defining has_mul and changing the results accordingly.

view this post on Zulip Kevin Buzzard (Feb 10 2021 at 19:25):

The only issue I guess is that I've seen HK to mean both the subset of products, and the subgroup they generate. But here this is perfect because if people want a subset and then multiply there.

view this post on Zulip Adrián Doña Mateo (Feb 10 2021 at 21:59):

I'm managed to prove the monoid structure and have some lemmas that show that H * N is just HN when N is normal. They look like this:

import group_theory.subgroup
import algebra.pointwise

open subgroup

variables {G : Type*} [group G]

/-- Two subgroups `H` and `K` can be multiplied to form another one. The result
is the smallest subgroup that contains `{ h * k | h ∈ H, k ∈ K }`. -/
instance subgroup_mul : has_mul (subgroup G) := λ H K, closure (H * K)⟩

/-- The carrier of `H * N` is just `↑H * ↑N` when `N` is normal. -/
lemma mul_normal (H N : subgroup G) [N.normal] : ((H * N) : set G) = H * N := sorry

/-- The carrier of `N * H` is just `↑N * ↑H` when `N` is normal. -/
lemma normal_mul (N H : subgroup G) [N.normal] : ((N * H) : set G) = N * H := sorry

/-- Subgroups form a monoid under multiplication. -/
instance : monoid (subgroup G) := sorry

I'll first make a pull request for this.

view this post on Zulip Eric Wieser (Feb 11 2021 at 00:56):

Isn't the proposed has_mul precisely the current sup operator on submodules, based on the statement of docs#subgroup.mem_sup?

view this post on Zulip Scott Kovach (Feb 11 2021 at 01:51):

as somebody new to lean, locating the definition of sup for subgroups starting from that lemma was a bit of an exercise, but after opening 6 of the proof widgets in vscode I got a link to subgroup.complete_lattice, which uses complete_lattice_of_Inf, which defines

sup := λ a b, Inf {x | a  x  b  x},

which I believe is the closure of the product.

(I may have misunderstood what you meant, but the mem_sup theorem is specific to comm_group, where every subgroup is normal)

view this post on Zulip Yakov Pechersky (Feb 11 2021 at 01:52):

If you're in vscode, you can also F12 (or right-click Go To Definition) to go to the file

view this post on Zulip Scott Kovach (Feb 11 2021 at 01:55):

right, but that takes me to the has_sup class

view this post on Zulip Eric Wieser (Feb 11 2021 at 01:55):

You did better than me, I just guessed what the definition was based on what was proved for comm_group!

view this post on Zulip Scott Kovach (Feb 11 2021 at 02:14):

oh right, I guess it would be surprising to have any other definition of sup, especially in light of that lemma

view this post on Zulip Johan Commelin (Feb 11 2021 at 05:37):

Eric Wieser said:

Isn't the proposed has_mul precisely the current sup operator on submodules, based on the statement of docs#subgroup.mem_sup?

Yup, that seems right. Good catch

view this post on Zulip Oliver Nash (Feb 11 2021 at 10:25):

Don't lattice theory people regard the 2nd iso theorem as a special case of the diamond isomorphism theorem for modular lattices?

view this post on Zulip Oliver Nash (Feb 11 2021 at 10:27):

I guess in this case it's not strictly a special case since subgroups don't form a modular lattice but I wonder if we could / should use a normal closure or something to factor this through the diamond isomorphism theorem for the modular lattice of normal subgroups.

view this post on Zulip Oliver Nash (Feb 11 2021 at 10:34):

Thinking about it a bit more, it probably just complicates things to try and use the DIT but looking now, I'm impressed that we do actually have this in Mathlib here

view this post on Zulip Oliver Nash (Feb 11 2021 at 10:37):

I wonder if someone should add a Tag in the docstring for modular_lattice.lean saying "second isomorphism theorem".

view this post on Zulip Eric Wieser (Feb 11 2021 at 11:17):

What is the purpose of the "tag"s?

view this post on Zulip Oliver Nash (Feb 11 2021 at 11:43):

I don't know if they have a well-defined purpose. I see them a place for strings that I think will help somebody doing a free text search for something (and which deserve to have a file-level scope). I think modular_lattice.lean deserves to show up if someone searches for "second isomorphism theorem".


Last updated: May 15 2021 at 02:11 UTC