Zulip Chat Archive

Stream: new members

Topic: Subgroup of quotient


Sophia Rodriguez (Mar 22 2025 at 16:44):

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 (Mar 22 2025 at 16:46):

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

Sophia Rodriguez (Mar 22 2025 at 16:46):

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 (Mar 22 2025 at 16:46):

You don't need injective (I think)

Aaron Liu (Mar 22 2025 at 16:50):

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 (Mar 22 2025 at 16:55):

Ah it works! thanks!

Sophia Rodriguez (Mar 22 2025 at 17:21):

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 (Mar 22 2025 at 18:08):

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

Sophia Rodriguez (Mar 23 2025 at 02:59):

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 (Mar 23 2025 at 07:22):

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 (Mar 23 2025 at 08:30):

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 (Mar 23 2025 at 11:44):

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 (Mar 23 2025 at 18:17):

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 (Mar 23 2025 at 18:30):

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 (Mar 23 2025 at 21:42):

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 (Mar 23 2025 at 23:22):

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

Last updated: May 02 2025 at 03:31 UTC