The quotient of a product group is isomorphic to the product

Stream: mathlib4

[张守信(Shouxin Zhang)]

I am trying to prove (G₁ × G₂) ⧸ (H₁ × H₂) ≃* G₁ ⧸ H₁ × G₂ ⧸ H₂. Since I couldn't find a library theorem, I spent some time trying to prove this simple result. However, I believe that theoretically, this result should be in the Mathlib4 library because it seems too classic. I suspect I haven't found the right library API. Does anyone know about this result?

import Mathlib

open Subgroup BigOperators

@[simp]
lemma quotient_group_prod_proj_eq_left
  {A₁ A₂ : Type*} [Group A₁] [Group A₂]
  {B₁ : Subgroup A₁} {B₂ : Subgroup A₂} [B₁.Normal] [B₂.Normal]
  (a : A₁ × A₂) :
  QuotientGroup.mk (s := B₁) (Quotient.out' (QuotientGroup.mk (s := B₁.prod B₂) a)).1 = a.1 := by
  let ha' := Quotient.out_eq' (QuotientGroup.mk (s := B₁.prod B₂) a)
  set a' := Quotient.out' (QuotientGroup.mk (s := B₁.prod B₂) a)
  rw [QuotientGroup.eq, mem_prod, Prod.fst_mul] at ha'
  exact QuotientGroup.eq.mpr ha'.1

@[simp]
lemma quotient_group_prod_proj_eq_right
  {A₁ A₂ : Type*} [Group A₁] [Group A₂]
  {B₁ : Subgroup A₁} {B₂ : Subgroup A₂} [B₁.Normal] [B₂.Normal]
  (a : A₁ × A₂) :
  QuotientGroup.mk (s := B₂) (Quotient.out' (QuotientGroup.mk (s := B₁.prod B₂) a)).2 = a.2 := by
  let ha' := Quotient.out_eq' (QuotientGroup.mk (s := B₁.prod B₂) a)
  set a' := Quotient.out' (QuotientGroup.mk (s := B₁.prod B₂) a)
  rw [QuotientGroup.eq, mem_prod, Prod.fst_mul] at ha'
  exact QuotientGroup.eq.mpr ha'.2


/-- (G₁ × G₂) ⧸ (H₁ × H₂) ≃* G₁ ⧸ H₁ × G₂ ⧸ H₂ -/
noncomputable def prodQuotientEquiv
  {A₁ A₂ : Type*} [Group A₁] [Group A₂]
  {B₁ : Subgroup A₁} {B₂ : Subgroup A₂}
  (hB₁ : B₁.Normal) (hB₂ : B₂.Normal) :
  (A₁ × A₂) ⧸ (B₁.prod B₂) ≃* (A₁ ⧸ B₁) × (A₂ ⧸ B₂) where
  toFun x := by
    obtain ⟨x₁, x₂⟩ := Quotient.out' x
    exact (QuotientGroup.mk x₁, QuotientGroup.mk x₂)
  invFun y := by
    obtain ⟨y₁, y₂⟩ := (Quotient.out' y.1, Quotient.out' y.2)
    exact @QuotientGroup.mk (A₁ × A₂) Prod.instGroup (B₁.prod B₂) (y₁, y₂)
  left_inv x := by
    simp only
    nth_rw 3 [← Quotient.out_eq x]
    simp only [QuotientGroup.eq, Prod.inv_mk, mem_prod]
    simp [Prod.fst_mul, Prod.snd_mul, ← QuotientGroup.eq, Quotient.out_eq']
    exact Prod.mk.inj_iff.mp rfl
  right_inv _ := by
    simp only [quotient_group_prod_proj_eq_left, Quotient.out_eq',
      quotient_group_prod_proj_eq_right, Prod.mk.eta]
  map_mul' := by
    intro x y; dsimp only
    set x₁ := (Quotient.out' x).1
    set x₂ := (Quotient.out' x).2
    set y₁ := (Quotient.out' y).1
    set y₂ := (Quotient.out' y).2
    set xy₁ := (Quotient.out' (x * y)).1
    set xy₂ := (Quotient.out' (x * y)).2
    simp only [Prod.mk_mul_mk, ← QuotientGroup.mk_mul]
    set z := @QuotientGroup.mk (A₁ × A₂) Prod.instGroup (B₁.prod B₂) ((x₁ * y₁), (x₂ * y₂)) with hz
    set z' := (QuotientGroup.mk (s := B₁) (Quotient.out' z).1, QuotientGroup.mk (s := B₂) (Quotient.out' z).2) with hz'
    have : (QuotientGroup.mk xy₁, QuotientGroup.mk xy₂) = z' := by
      have : z = (@QuotientGroup.mk (A₁ × A₂) Prod.instGroup (B₁.prod B₂) (x₁, x₂)) * (@QuotientGroup.mk (A₁ × A₂) Prod.instGroup (B₁.prod B₂) (y₁, y₂)) := by
        simp only [hz, ← QuotientGroup.mk_mul, Prod.mk_mul_mk]
      simp only [hz', this, Quotient.out_eq' x, Quotient.out_eq' y]
    simp only [this, hz', hz, Prod.mk.injEq]
    exact ⟨by apply quotient_group_prod_proj_eq_left,
      by apply quotient_group_prod_proj_eq_right⟩

[Andrew Yang]

An easy way is docs#MonoidHom.ker_prodMap docs#Prod.map_surjective docs#QuotientGroup.quotientKerEquivOfSurjective docs#QuotientGroup.quotientMulEquivOfEq

[张守信(Shouxin Zhang)]

Andrew Yang said:

An easy way is docs#MonoidHom.ker_prodMap docs#Prod.map_surjective docs#QuotientGroup.quotientKerEquivOfSurjective docs#QuotientGroup.quotientMulEquivOfEq

Although I can roughly guess the proofs corresponding to these documents, there is no doubt that this is beyond my capabilities... Moreover, is it not included in the Mathlib4 library because this example can be concisely proven using these documents? I find that unreasonable. (thinking...

[Andrew Yang]

We definitely want this in mathlib. Feel free to PR it!

[Andrew Yang]

But we should probably have a computable inverse.

[Yury G. Kudryashov]

@Joseph Myers added leftRel_prod in #17585

[Yury G. Kudryashov]

... and some relevant Equivs in #15947

[Yury G. Kudryashov]

Joseph, are you going to add MulEquiv versions?

[Joseph Myers]

I'm not planning MulEquiv versions - my goal with those equivs was simply to show the types have equal cardinality, which doesn't need any further structure.