Define Quotient Group

Stream: mathlib4

[Nick_adfor]

I'm now trying to define quotient group in this way. But I'm not familiar with Classical.choose. As in the sorry I need to prove Classical.choose ⋯ = g.

import Mathlib

suppress_compilation

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

open Pointwise

structure QGroup : Type where
  carrier : Set G
  isCoset : ∃ g : G, carrier = g • H

namespace QGroup

variable {H}

instance : SetLike (QGroup H) G where
  coe C := C.carrier
  coe_injective' := by
    intro C D; cases C; cases D; simp

@[ext]
lemma ext {C D : QGroup H} (h : (C : Set G) = D) : C = D := by
  cases C; cases D; simp at h; simp [h]

def out (C : QGroup H) : G := Classical.choose C.isCoset

@[simp]
lemma out_spec (C : QGroup H) : C.out • H = (C : Set G) :=
  Classical.choose_spec C.isCoset |>.symm

lemma mem_iff_out (C : QGroup H) (g : G) : g ∈ C ↔ ∃ h ∈ H, g = C.out • h := by
  rw [← SetLike.mem_coe, ← C.out_spec, Set.mem_smul_set]
  tauto

variable (H) in
def gen (g : G) : QGroup H :=
  ⟨g • H, ⟨g, rfl⟩⟩

lemma gen_def (g : G) : (gen H g : Set G) = g • H := rfl

@[simp]
lemma mem_gen_iff (g : G) {x : G} : x ∈ gen H g ↔ ∃ h ∈ H, x = g * h := by
  rw [← SetLike.mem_coe, gen_def, Set.mem_smul_set]
  tauto

@[simp]
lemma gen_out (C : QGroup H) : gen H C.out = C := by
  ext g
  simp only [SetLike.mem_coe, mem_gen_iff]
  rw [C.mem_iff_out]
  rfl

@[simp]
lemma mem_out_gen (g : G) {x : G} : x ∈ ((gen H g).out • H : Set G) ↔ x ∈ (g • H : Set G) := by
  simp [Set.mem_smul_set, eq_comm]


@[elab_as_elim]
theorem gen_induction {P : QGroup H → Prop}
    (h : ∀ g : G, P (gen H g)) :
    ∀ C : QGroup H, P C := by
  intro C
  rw [← C.gen_out]
  tauto

@[simp]
theorem gen_eq_iff (g : G) (C : QGroup H) : gen H g = C ↔ g ∈ C := by
  constructor
  · rintro rfl
    simp
  · intro h
    rw [C.mem_iff_out] at h
    obtain ⟨x, hx, rfl⟩ := h
    ext y
    simp only [smul_eq_mul, SetLike.mem_coe, mem_gen_iff]
    constructor
    · rintro ⟨y, hy, rfl⟩
      rw [C.mem_iff_out]
      use x * y, mul_mem hx hy
      simp [mul_assoc]
    · rw [C.mem_iff_out]
      rintro ⟨y, hy, rfl⟩
      use x⁻¹ * y, mul_mem (H.inv_mem hx) hy
      simp [mul_assoc]

instance : One (QGroup H) where
  one := ⟨H, ⟨1, by simp⟩⟩

lemma one_def : ((1 : QGroup H) : Set G) = H := rfl

@[simp]
lemma mem_one_iff {g : G} : g ∈ (1 : QGroup H) ↔ g ∈ H := Iff.rfl

@[simp]
lemma gen_one : gen H 1 = 1 := by
  ext g
  simp

instance : Mul (QGroup H) where
  mul C D := ⟨C.out • D.out • H, ⟨C.out * D.out, by simp [mul_smul, out_spec]⟩⟩

lemma mul_def (C D : QGroup H) :
    ((C * D : QGroup H) : Set G) = C.out • D.out • H := rfl

[Aaron Liu]

everything you can know about Classical.choose is contained in Classical.choose_spec

[Aaron Liu]

when working with quotients like this I strongly discourage the use of QGroup.out

[Nick_adfor]

What will QGroup.out cause?

[Aaron Liu]

the preferred way to do quotients if you don't have a way to pick out a canonical representative is to use docs#Quotient instead of making it the equivalence classes

[Aaron Liu]

that way you have access to docs#Quotient.lift

[Nick_adfor]

Now the problem is truly (gen H g).out = g, but I cannot Choose one.

[Aaron Liu]

Nick_adfor said:

Now the problem is truly (gen H g).out = g, but I cannot Choose one.

but that's not always true

[Nick_adfor]

It should be (gen H g).out ∈ (gen H g : Set G)

[Nick_adfor]

@[simp]
lemma gen_mul_gen (g g' : G) : gen H g * gen H g' = gen H (g * g') := by
  ext x
  simp only [SetLike.mem_coe, mul_def, gen_def, Set.mem_smul_set]
  constructor
  · rintro ⟨w, hw, rfl⟩
    obtain ⟨h₂, hh₂, rfl⟩ := hw
    have mem1 : (gen H g).out ∈ (gen H g).out • (H : Set G) := by
      use 1, H.one_mem
      simp
    rw [mem_out_gen] at mem1
    rw [Set.mem_smul_set] at mem1
    obtain ⟨h₁, hh₁, h_eq1⟩ := mem1
    have mem2 : (gen H g').out ∈ (gen H g').out • (H : Set G) := by
      use 1, H.one_mem
      simp
    rw [mem_out_gen] at mem2
    rw [Set.mem_smul_set] at mem2
    obtain ⟨k, hk, h_eq2⟩ := mem2
    rw [<-h_eq1, <-h_eq2]
    use (g'⁻¹ * h₁ * g') * (k * h₂)
    constructor
    · have hh₁' : h₁ ∈ H := hh₁
      have hk' : k ∈ H := hk
      have conj_mem : g'⁻¹ * h₁ * g' ∈ H := by exact?
      have mul_mem1 : k * h₂ ∈ H := by exact (Subgroup.mul_mem_cancel_right H hh₂).mpr hk
      exact mul_mem conj_mem mul_mem1
    · simp [mul_assoc]

It is the second exact? giving the wrong proof I've ever seen today......

[Notification Bot]

3 messages were moved from this topic to #mathlib4 > exact? gives incorrect line-wrapping by Eric Wieser.

[Nick_adfor]

It is really a disaster to Choose. I really cannot understand how the definition Choose gH. It is not the same as maths.

@[simp]
lemma gen_mul_gen (g g' : G) : gen H g * gen H g' = gen H (g * g') := by
  ext x
  simp only [SetLike.mem_coe, mem_gen_iff]
  constructor
  · rintro ⟨w, hw, rfl⟩
    obtain ⟨h₂, hh₂, rfl⟩ := hw
    have mem1 : (gen H g).out ∈ (gen H g).out • (H : Set G) := by
      use 1, H.one_mem
      simp
    rw [mem_out_gen] at mem1
    obtain ⟨h₁, hh₁, h_eq1⟩ := mem1
    have mem2 : (gen H g').out ∈ (gen H g').out • (H : Set G) := by
      use 1, H.one_mem
      simp
    rw [mem_out_gen] at mem2
    obtain ⟨k, hk, h_eq2⟩ := mem2
    rw [<-h_eq1, <-h_eq2]
    use (g'⁻¹ * h₁ * g') * (k * h₂)
    constructor
    · have hh₁' : h₁ ∈ H := hh₁
      have hk' : k ∈ H := hk
      have conj_mem : g'⁻¹ * h₁ * g' ∈ H := by
        (expose_names; exact Subgroup.Normal.conj_mem' inst_1 h₁ hh₁ g')
      have mul_mem1 : k * h₂ ∈ H := by
        exact (Subgroup.mul_mem_cancel_right H hh₂).mpr hk
      exact mul_mem conj_mem mul_mem1
    · simp only [smul_eq_mul, mul_assoc, mul_inv_cancel_left]

  · rintro ⟨h, hh, rfl⟩
    have : g' * h ∈ (gen H g').out • (H : Set G) := by
      rw [(gen H g').out_spec]
      exact ⟨h, hh, rfl⟩
    rw [mem_out_gen] at this
    obtain ⟨k, hk, h_eq⟩ := this
    have h1 : (gen H g).out ∈ g • (H : Set G) := by
      rw [← gen_def, ← (gen H g).out_spec]
      exact ⟨1, H.one_mem, by simp⟩
    have h2 : (gen H g').out ∈ g' • (H : Set G) := by
      rw [← gen_def, ← (gen H g').out_spec]
      exact ⟨1, H.one_mem, by simp⟩
    rcases h1 with ⟨a, ha, h1_eq⟩
    rcases h2 with ⟨b, hb, h2_eq⟩
    let w := (gen H g').out * (a⁻¹ * b⁻¹ * h)
    have hw : w ∈ (gen H g').out • (H : Set G) := by
      rw [Set.mem_smul_set]
      exact ⟨a⁻¹ * b⁻¹ * h, mul_mem (mul_mem (inv_mem ha) (inv_mem hb)) hh, rfl⟩
    refine ⟨(gen H g').out * (a⁻¹ * b⁻¹ * h), ⟨a⁻¹ * b⁻¹ * h, mul_mem (mul_mem (inv_mem ha) (inv_mem hb)) hh, rfl⟩, ?_⟩
    simp
    have h1_simple : (gen H g).out = g * a := Eq.symm h1_eq
    have h2_simple : (gen H g').out = g' * b := Eq.symm h2_eq
    rw [h1_simple, h2_simple]
    norm_num

    have mem1 : (gen H g).out ∈ (gen H g).out • (H : Set G) := by
      use 1, H.one_mem
      simp
    rw [mem_out_gen] at mem1
    obtain ⟨h₁, hh₁, h_eq1⟩ := mem1
    have mem2 : (gen H g').out ∈ (gen H g').out • (H : Set G) := by
      use 1, H.one_mem
      simp
    rw [mem_out_gen] at mem2
    obtain ⟨k, hk, h_eq2⟩ := mem2

    have h_conj : g'⁻¹ * h₁ * g' ∈ H := by
      (expose_names; exact Subgroup.Normal.conj_mem' inst_1 h₁ hh₁ g')
    have prodH : (g'⁻¹ * h₁ * g' * k) ∈ H := by
      exact (Subgroup.mul_mem_cancel_right H hk).mpr h_conj
    sorry

[Patrick Massot]

Nick_adfor said:

It is really a disaster to Choose. I really cannot understand how the definition Choose gH. It is not the same as maths.

Aaron already told you, you will keep suffering until you accept to do the same thing as on paper (except in super elementary courses): forget about equivalence classes as subset of the original group and embrace the universal property of quotients.

[Kevin Buzzard]

Nick_adfor said:

It is the second exact? giving the wrong proof I've ever seen today......

Sure, but exact? is telling you the relevant lemma, it's just struggling to apply it because Subgroup.Normal.conj_mem' takes a proof that a subgroup is normal as an explicit input, whereas Subgroup.Normal is a class. This is usually the reason that exact? spits out weird stuff about exposing names. have conj_mem : g'⁻¹ * h₁ * g' ∈ H := Subgroup.Normal.conj_mem' inferInstance _ hh₁' _ works fine.

[Eric Wieser]

Kevin, see the linked thread I moved to; the complaint is that "Try this" uses incorrect indentation.

[Nick_adfor]

Patrick Massot said:

Nick_adfor said:

It is really a disaster to Choose. I really cannot understand how the definition Choose gH. It is not the same as maths.

Aaron already told you, you will keep suffering until you accept to do the same thing as on paper (except in super elementary courses): forget about equivalence classes as subset of the original group and embrace the universal property of quotients.

It should be:

Forward direction (⇒)

Assume x ∈ (gH)(g'H). Then ∃ h₁, h₂ ∈ H such that
x = (g h₁)(g' h₂) = g h₁ g' h₂.

Since H is normal, h₁ g' = g' h₃ where h₃ = g'⁻¹ h₁ g' ∈ H.
Thus:
x = g (g' h₃) h₂ = g g' (h₃ h₂).
Let h = h₃ h₂ ∈ H, then x = g g' h.

Reverse direction (⇐)

Assume x = g g' h with h ∈ H.
Take h₁ = 1 ∈ H, h₂ = h ∈ H, then:
x = (g · 1) · (g' · h) ∈ (gH)(g'H).

[Kevin Buzzard]

Yes but what people are trying to tell you is that your definition of a quotient group is not idiomatic Lean. The reason Lean has a Quotient construction is precisely so you don't have to be in this hell. However I am sure that you can plough your way through the hell if you like; indeed I tried doing this myself many years ago as an experiment and I did make it through. One big difference is that with Quotient so many more things are rfl whereas everything is noncomputable with the Set approach.

[Kevin Buzzard]

Eric Wieser said:

Kevin, see the linked thread I moved to; the complaint is that "Try this" uses incorrect indentation.

Right: there are I think two independent issues here -- one is that the proof which exact? gives is weird (because it needs a name for a typeclass) and the other is that it doesn't compile (because of indentation issues).