## Stream: general

### Topic: 2nd isomorphism theorem for groups

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

#### Johan Commelin (Feb 10 2021 at 18:15):

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

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

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

#### Johan Commelin (Feb 10 2021 at 18:22):

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

#### Floris van Doorn (Feb 10 2021 at 18:22):

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

#### 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?

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

#### Floris van Doorn (Feb 10 2021 at 18:23):

That sounds right.

#### 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

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

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

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

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

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

#### 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?

#### 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)

#### 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

#### Scott Kovach (Feb 11 2021 at 01:55):

right, but that takes me to the has_sup class

#### 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!

#### 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

#### 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

#### 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?

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

#### 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

#### 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".

#### Eric Wieser (Feb 11 2021 at 11:17):

What is the purpose of the "tag"s?

#### 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