Subgroup of quotient

Stream: new members

[Sophia Rodriguez]

Suppose I have a group G, and its subgroups H and V, where V is normal. Is there a way of interpreting(↥(H ⊔ V) ⧸ V.subgroupOf (H ⊔ V))as subgroup of (↥(⊤ : Subgroup G) ⧸ V.subgroupOf ⊤), or even better G ⧸ V?

[Aaron Liu]

Try using some docs#Subgroup.map and docs#Subgroup.comap maybe

[Sophia Rodriguez]

I noticed that QuotientGroup.quotientMapSubgroupOfOfLe produces a map from (↥(H ⊔ V) ⧸ V.subgroupOf (H ⊔ V)) to (↥(⊤ : Subgroup G) ⧸ V.subgroupOf ⊤), but didnt specify whether it is injective or something

[Aaron Liu]

You don't need injective (I think)

[Aaron Liu]

Just comap along the docs#QuotientGroup.mk', then map along docs#Subgroup.subtype, then map along docs#QuotientGroup.mk' and you get a subgroup of G ⧸ V.

[Sophia Rodriguez]

Ah it works! thanks!

[Sophia Rodriguez]

sorry, one more question :smiling_face_with_tear: , how should I prove the resulted subgroup is equivalent with the original one? Like,

  set stage1 := Subgroup.comap (QuotientGroup.mk' (V.subgroupOf (H ⊔ V))) ⊤ with def1
  set stage2 := Subgroup.map (Subgroup.subtype (H ⊔ V)) stage1 with def2
  set stage3 := Subgroup.map (QuotientGroup.mk' V) stage2 with def3
  let equiv : stage3 ≃* ↥(H ⊔ V) ⧸ V.subgroupOf (H ⊔ V) := by sorry

[Aaron Liu]

Explicit homomorphism with explicit inverse, using docs#QuotientGroup.lift

[Sophia Rodriguez]

hummm... could you enlighten me a bit more? I reduced the situation into:

def equiv {G : Type*} [Group G] (H V : Subgroup G) [V.Normal] :
    Subgroup.map (QuotientGroup.mk' V) H ≃* (H ⧸ V.subgroupOf H) := by sorry

and tried QuotientGroup.lift:

def equiv {G : Type*} [Group G] (H V : Subgroup G) [V.Normal] :
    Subgroup.map (QuotientGroup.mk' V) H ≃* (H ⧸ V.subgroupOf H) := by
  let φ : H →* (Subgroup.map (QuotientGroup.mk' V) H) := {
  toFun := by
    intro h
    use ⟦h⟧, h, h.2
    simp only [QuotientGroup.mk'_apply]
  map_one' := rfl
  map_mul' x y := by
    simp only [Subgroup.coe_mul, QuotientGroup.mk_mul]
    rfl
  }
  have le_ker : V.subgroupOf H ≤ φ.ker := by
    rw [← Subgroup.map_eq_bot_iff]
    refine Subgroup.ext ?_
    intro x
    simp only [Subgroup.mem_map, Subtype.exists, Subgroup.mem_bot]
    constructor
    · intro ⟨hx₁, ⟨b, hx₂⟩⟩
      simp only [← hx₂.2, MonoidHom.coe_mk, OneHom.coe_mk, φ]
      apply Subtype.val_inj.1
      simp only [OneMemClass.coe_one, QuotientGroup.eq_one_iff, φ]
      exact hx₂.1
    · intro hx
      rw [hx]
      use 1, (Subgroup.one_mem H)
      constructor
      · exact (Subgroup.one_mem V)
      · simp only [MonoidHom.coe_mk, OneHom.coe_mk, QuotientGroup.mk_one, Subgroup.mk_eq_one, φ]
  let invFun := QuotientGroup.lift (V.subgroupOf H) φ le_ker
  sorry

is this the right approach?

[Kevin Buzzard]

Just use the first isomorphism theorem? Isn't this the second isomorphism theorem, which is in mathlib so you could look for inspiration there

[Sophia Rodriguez]

yes the second isomorphism can yield

↥H ⧸ V.subgroupOf H ≃* ↥(H ⊔ V) ⧸ V.subgroupOf (H ⊔ V)

in the origin question, but I still want it to be a Subgroup (G ⧸ V).
(Cause I am actually analyzing the cardinality of ↥(H ⊔ V) ⧸ V.subgroupOf (H ⊔ V), and now I only have the cardinality of G ⧸ V)

[Sophia Rodriguez]

Sophia Rodriguez said:

hummm... could you enlighten me a bit more? I reduced the situation into:

def equiv {G : Type*} [Group G] (H V : Subgroup G) [V.Normal] :
    Subgroup.map (QuotientGroup.mk' V) H ≃* (H ⧸ V.subgroupOf H) := by sorry

and tried QuotientGroup.lift:
...
is this the right approach?

sorry, it should be Subgroup.map (QuotientGroup.mk' V) (H ⊔ V) ≃* (↥(H ⊔ V) ⧸ V.subgroupOf (H ⊔ V))

[Kevin Buzzard]

Yes I see: H is a term but you are promoting it to a type, indeed you're promoting several terms to types, which makes this kind of thing very thorny. This kind of question really shows you the difference between set theory (how we are all taught to think about these questions) and type theory (where a subgroup isn't a group, because a group is a type and a subgroup is a term). I agree that this is annoying to do in Lean, for non-mathematical reasons.

[Kevin Buzzard]

Here is my proposed approach:

import Mathlib

variable {G : Type*} [Group G] (H V : Subgroup G) [V.Normal]

def lift_inv_fun : H →* Subgroup.map (QuotientGroup.mk' V) H := (QuotientGroup.mk' V).subgroupMap H

def inv_fun {G : Type*} [Group G] (H V : Subgroup G) [V.Normal] :
    (H ⧸ V.subgroupOf H) →* Subgroup.map (QuotientGroup.mk' V) H :=
  QuotientGroup.lift (V.subgroupOf H) (lift_inv_fun H V) <| by
    sorry

noncomputable def equiv_symm {G : Type*} [Group G] (H V : Subgroup G) [V.Normal] :
    (H ⧸ V.subgroupOf H) ≃* Subgroup.map (QuotientGroup.mk' V) H :=
  MulEquiv.ofBijective (inv_fun H V) <| by
    sorry

noncomputable def equiv {G : Type*} [Group G] (H V : Subgroup G) [V.Normal] :
    Subgroup.map (QuotientGroup.mk' V) H ≃* (H ⧸ V.subgroupOf H) := (equiv_symm H V).symm

All the data is defined in term mode, there are two sorrys, hopefully neither of them are hard, but the second one might be a fair bit of work. Hopefully you have seen the questions before though?

[Kevin Buzzard]

I tried this but there seems to be no lemma saying what the kernel of 'subgroupMap' is:

def inv_fun {G : Type*} [Group G] (H V : Subgroup G) [V.Normal] :
    (H ⧸ V.subgroupOf H) →* Subgroup.map (QuotientGroup.mk' V) H :=
  QuotientGroup.lift (V.subgroupOf H) (lift_inv_fun H V) <| by
    rintro ⟨g, hg1⟩ hg2
    simp only [Subgroup.mem_subgroupOf] at hg2
    ext
    simp [lift_inv_fun, hg2]

noncomputable def equiv_symm {G : Type*} [Group G] (H V : Subgroup G) [V.Normal] :
    (H ⧸ V.subgroupOf H) ≃* Subgroup.map (QuotientGroup.mk' V) H :=
  MulEquiv.ofBijective (inv_fun H V) <| by
    refine ⟨?_, ?_⟩
    · rw [← MonoidHom.ker_eq_bot_iff, ← le_bot_iff]
      rintro x
      simp only [inv_fun, lift_inv_fun, Subgroup.mem_bot]
      induction x using QuotientGroup.induction_on
      rename_i z
      obtain ⟨h, hh⟩ := z
      simp
      -- need a lemma about the kernel of subgroupMap
      sorry
    . rintro ⟨_, g, hg, rfl⟩
      use QuotientGroup.mk ⟨g, hg⟩
      simp [inv_fun, lift_inv_fun]
      rfl

[Kevin Buzzard]

-- I couldn't find this API, should be in mathlib
lemma ker_subgroupMap {G G' : Type*} [Group G] [Group G'] (f : G →* G')
    (H : Subgroup G) : (f.subgroupMap H).ker = f.ker.subgroupOf H := by
  ext ⟨x, hx⟩
  simp only [MonoidHom.subgroupMap, MonoidHom.submonoidMap, Subgroup.mem_subgroupOf]
  change ⟨f x, _⟩ = (⟨1, _⟩ : ↥(Subgroup.map f H)) ↔ _
  simp

noncomputable def equiv_symm {G : Type*} [Group G] (H V : Subgroup G) [V.Normal] :
    (H ⧸ V.subgroupOf H) ≃* Subgroup.map (QuotientGroup.mk' V) H :=
  MulEquiv.ofBijective (inv_fun H V) <| by
    refine ⟨?_, ?_⟩
    · rw [← MonoidHom.ker_eq_bot_iff, ← le_bot_iff]
      rintro x
      simp only [inv_fun, lift_inv_fun, Subgroup.mem_bot]
      induction x using QuotientGroup.induction_on
      rename_i z -- there's a better way of doing these last two lines
      simp only [QuotientGroup.lift_mk, QuotientGroup.eq_one_iff, ker_subgroupMap]
      intro (h : z ∈ (((QuotientGroup.mk' V).subgroupMap H)).ker)
      rwa [ker_subgroupMap, QuotientGroup.ker_mk'] at h
    . rintro ⟨_, g, hg, rfl⟩
      use QuotientGroup.mk ⟨g, hg⟩
      simp [inv_fun, lift_inv_fun]
      rfl