# Zulip Chat Archive

## 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 ~~ Nevermind, I see that taking the closure would fix this.`has_mul`

would be that `H * N`

is only a subgroup when at least one of the two is normal.

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