2nd isomorphism theorem for groups

Stream: general

[Adrián Doña Mateo]

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]

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

[Johan Commelin]

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]

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]

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

[Floris van Doorn]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Floris van Doorn]

That sounds right.

[Mario Carneiro]

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]

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

[Adrián Doña Mateo]

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]

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

[Kevin Buzzard]

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]

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]

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

[Scott Kovach]

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]

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

[Scott Kovach]

right, but that takes me to the has_sup class

[Eric Wieser]

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

[Scott Kovach]

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

[Johan Commelin]

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]

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

[Oliver Nash]

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]

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]

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

[Eric Wieser]

What is the purpose of the "tag"s?

[Oliver Nash]

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