quotient of a group by a subgroup bijects with left cosets

Stream: Is there code for X?

[Kevin Buzzard]

If L : subgroup G then quotient L is defined to be the quotient (in the sense of core Lean) of G by the equivalence relation "we're in the same left coset of L". However I could not find the equiv between quotient L and the type of left cosets of L in G, and indeed I could not even find this type. Are these things not there or am I looking in the wrong places?

[Eric Wieser]

By "I cannot find this type" do you mean that you can't work out how to state the isomorphism you're looking for?

[Eric Wieser]

I think {s // ∃ a, s = left_coset a L} is the type you need?

[Eric Wieser]

Definitely golfable:

import group_theory.quotient_group

variables {G : Type*} [group G] (L : subgroup G)

noncomputable def the_equiv : {s // ∃ a : G, s = left_coset a L} ≃ quotient_group.quotient L :=
{ to_fun := λ s, quotient_group.mk s.prop.some,
  inv_fun := λ q, quotient.lift_on' q
    (λ g : G, (⟨left_coset g L, g, rfl⟩ : {s // ∃ a : G, s = left_coset a L})) $ λ a b h, begin
      ext,
      simp only [subtype.coe_mk, set_like.mem_coe],
      rw [←quotient_group.eq_class_eq_left_coset, ←quotient_group.eq_class_eq_left_coset],
      exact eq.congr_right (quotient_group.eq.mpr h),
    end,
  left_inv := λ s, begin
    ext1, dsimp,
    generalize_proofs h,
    exact h.some_spec.symm,
  end,
  right_inv := quotient.ind' $ begin
    dsimp,
    intro a,
    generalize_proofs h,
    apply quotient.sound',
    dunfold quotient_group.left_rel setoid.r,
    rw [←set_like.mem_coe, ← mem_left_coset_iff],
    rw [←h.some_spec, subtype.coe_mk],
    exact mem_own_left_coset L.to_submonoid a,
  end }

[Eric Wieser]

map_mul left as an exercise to the reader

[Eric Wieser]

I PR'd a variant of the first half of this as #8382