QuotientGroup.sound

Stream: Is there code for X?

[Alex Kontorovich]

I don't see a version of Quotient.sound for QuotientGroup; there's probably a much simpler way to do it than this?

import Mathlib.GroupTheory.QuotientGroup

open Set

open scoped Pointwise

variable (G : Type _) [Group G] (Γ : Subgroup G) [Subgroup.Normal Γ]

theorem QuotientGroup.sound [Subgroup.Normal Γ] (U : Set (G ⧸ Γ)) (g : (Subgroup.opposite Γ)) :
    g • (QuotientGroup.mk' Γ) ⁻¹' U = (QuotientGroup.mk' Γ) ⁻¹' U := by
  rw [QuotientGroup.coe_mk']
  ext x
  simp only [mem_preimage]
  constructor
  · intro hx
    rw [Set.mem_smul_set] at hx
    obtain ⟨y, y_mem, gy_eq_x⟩ := hx
    simp only [mem_preimage] at y_mem
    convert y_mem using 1
    symm
    apply Quotient.sound (b := x) (s := (QuotientGroup.leftRel Γ)) (a := y)
    rw [← gy_eq_x]
    refine ⟨g⁻¹, by simp⟩
  · intro hx
    rw [Set.mem_smul_set]
    refine ⟨g⁻¹ • x, ?_, by simp⟩
    simp only [mem_preimage]
    convert hx using 1
    symm
    apply Quotient.sound (b := g⁻¹ • x) (s := (QuotientGroup.leftRel Γ)) (a := x)
    refine ⟨g, by simp⟩

[Eric Wieser]

docs#QuotientGroup.eq

[Alex Kontorovich]

Yes I saw that, but it's for individual elements, whereas I want to move the preimage under the quotient map of an arbitrary set in the quotient, by an element of the subgroup...? Maybe I'm missing something trivial?

[Alex Kontorovich]

I can hit it with Set.mem_inv_smul_set_iff first; should help. I'm still struggling with QuotientGroup.eq because it doesn't recognize Subgroup.opposite Γ as a Subgroup G...?

[Alex Kontorovich]

Ok now I can just use Quotient.sound directly. Still, maybe there's a cleaner way?

import Mathlib.GroupTheory.QuotientGroup

open Set

open scoped Pointwise

variable (G : Type _) [Group G] (Γ : Subgroup G) [Subgroup.Normal Γ]

theorem QuotientGroup.sound [Subgroup.Normal Γ] (U : Set (G ⧸ Γ)) (g : (Subgroup.opposite Γ)) :
    g • (QuotientGroup.mk' Γ) ⁻¹' U = (QuotientGroup.mk' Γ) ⁻¹' U := by
  rw [QuotientGroup.coe_mk']
  ext x
  simp only [mem_preimage]
  have := @Set.mem_inv_smul_set_iff (x := x) (A := (mk' Γ) ⁻¹' U) (a := g⁻¹) _ _
  simp only [inv_inv, coe_mk', mem_preimage] at this
  convert this using 2
  apply @Quotient.sound (a := x) (s := (QuotientGroup.leftRel Γ)) (b := g⁻¹ • x)
  use g
  simp

[Eric Wieser]

Isn't sound just one direction of eq?

[Antoine Chambert-Loir]

If Gamma is a subgroup of G, why would Opposite Gamma be a subgroup of G? The law is reversed.