Quotient of a quotient

Stream: Is there code for X?

[Vincent Beffara]

I would like to show that the quotient of a quotient of V : Type can be written as a quotient of V, and although I manage to prove something in this direction, the proof I am getting is extremely awkward (see left_inv and right_inv below). Would what I am looking for already be somewhere in mathlib? If not, what would be the "right" way to write this proof?

import init.function data.quot tactic
open function classical quotient

lemma toto : ∀ (V : Type) (s : setoid V) (s' : setoid (quotient s)),
        ∃ (s'' : setoid V) (φ : quotient s'' -> quotient s'), bijective φ

    := by { intros, cases s with r hᵣ, cases s' with r' hᵣ',

        let r'' := λ x y, r' (quot.mk r x) (quot.mk r y),

        have eqv : equivalence r''
            := ⟨λ _, hᵣ'.1 _, λ _ _ h, hᵣ'.2.1 h, λ x y z h1 h2, hᵣ'.2.2 h1 h2⟩,

        have eqv_r' : eqv_gen r' = r' := equivalence.eqv_gen_eq hᵣ',
        have eqv_r'' : eqv_gen r'' = r'' := equivalence.eqv_gen_eq eqv,

        let φ := λ xx, quot.mk r' (quot.mk r (quot.out xx)),
        let ψ := λ xx, quot.mk r'' (quot.out (quot.out xx)),

        have left_inv : left_inverse ψ φ, by {
            intro x, simp only [φ,ψ],
            refine eq.trans _ (quot.out_eq x),
            apply quot.eq.mpr,
            rw eqv_r'', simp only [r''], rw <-eqv_r',
            apply quot.eq.mp,
            rw [eqv_r',quot.out_eq,quot.out_eq] },

        have right_inv : right_inverse ψ φ, by {
            intro x, simp only [φ,ψ],
            have h0: ∀ {x y}, r'' x y = r' (quot.mk r x) (quot.mk r y) := λ x y, rfl,
            have h1 := quot.out_eq x,
            have h2 := quot.out_eq x.out,
            rw <-h1, rw <-h2,
            apply quot.eq.mpr,
            rw eqv_r', rw <-h0, rw <-eqv_r'',
            apply quot.eq.mp,
            rw [eqv_r'',quot.out_eq,quot.out_eq,quot.out_eq] },

        have : bijective φ
            := ⟨left_inverse.injective left_inv, right_inverse.surjective right_inv⟩,

        exact ⟨⟨r'',eqv⟩,φ,this⟩
    }

[Thomas Browning]

I feel like you should be able to prove this quicker in terms of composition of surjective functions.

[Adam Topaz]

Or you could come up with the relation for the associated setoid directly.

[Adam Topaz]

E.g.

import init.function data.quot tactic
open function classical quotient

lemma setoid.compose {V : Type*} (s : setoid V) (t : setoid (quotient s)) :
  setoid V :=
{ r := λ a b, @setoid.r (quotient s) t (quotient.mk' a) (quotient.mk' b),
  iseqv := begin
    refine ⟨_,_,_⟩,
    { intros a, rw ← quotient.eq' },
    { intros a b h, rw ← quotient.eq' at *, exact h.symm },
    { intros a b c h1 h2, rw ← quotient.eq' at *, cc }
  end }

def setoid.quotient_compose_equiv {V : Type*} (s : setoid V) (t : setoid (quotient s)) :
  quotient (s.compose t) ≃ quotient t :=
{ to_fun := λ i, quotient.lift_on' i (λ v, quotient.mk' $ quotient.mk' v) sorry,
  inv_fun := λ j, quotient.lift_on' j (λ k, quotient.lift_on' k (λ v, quotient.mk' v) sorry) sorry,
  left_inv := sorry,
  right_inv := sorry }

[Adam Topaz]

I would be surprised if we don't already have something similar.

[Vincent Beffara]

The relation itself is clear enough (λ x y, r' (quot.mk r x) (quot.mk r y)), it's the proofs of left_inv and right_inv that I have trouble with. I will try your suggestion :-)

[Thomas Browning]

Here's a slightly different way

lemma toto (V : Type) (s : setoid V) (s' : setoid (quotient s)) :
  ∃ (s'' : setoid V) (φ : quotient s'' → quotient s'), bijective φ :=
begin
  let f : V → quotient s := quotient.mk,
  let g : quotient s → quotient s' := quotient.mk,
  let h := setoid.quotient_ker_equiv_of_surjective (g ∘ f)
    ((surjective_quotient_mk (quotient s)).comp (surjective_quotient_mk V)),
  exact ⟨setoid.ker (g ∘ f), h, h.bijective⟩,
end

[Adam Topaz]

What I'm mostly saying is that it doesn't make sense to have an existential statement, when you can construct the relation itself, and obtain a useful bijection between the quotients, not just the fact that some random bijection exists.

[Adam Topaz]

(my definition of setoid.compose should be a def not a lemma)

[Vincent Beffara]

Mixing the two:

import tactic

variables {V : Type*} (s : setoid V) (t : setoid (quotient s))

def setoid.comp (s : setoid V) (t : setoid (quotient s)) : setoid V :=
    let f : V → quotient s := quotient.mk,
        g : quotient s → quotient t := quotient.mk
    in setoid.ker (g ∘ f)

noncomputable def setoid.comp.iso : quotient (setoid.comp s t) ≃ quotient t :=
    let f : V → quotient s := quotient.mk,
        g : quotient s → quotient t := quotient.mk
    in setoid.quotient_ker_equiv_of_surjective (g ∘ f)
        ((surjective_quotient_mk (quotient s)).comp (surjective_quotient_mk V))

noncomputable def setoid.comp.iso' : quotient (setoid.comp s t) ≃ quotient t :=
    let gof : V -> quotient t := quotient.mk ∘ quotient.mk
    in setoid.quotient_ker_equiv_of_surjective gof
        ((surjective_quotient_mk (quotient s)).comp (surjective_quotient_mk V))

[Adam Topaz]

You can make everything computable if you don't use setoid.ker_equiv_of_surjective

[Eric Wieser]

Is compose just docs#setoid.comap quotient.mk?

[Adam Topaz]

@Eric Wieser yes, that's right

[Vincent Beffara]

Hi again, so I managed to make a computable version like this:

import data.setoid.basic

def setoid.comp {V : Type} (s : setoid V) (t : setoid (quotient s)) : setoid V :=
let f : V → quotient s := quotient.mk,
    g : quotient s → quotient t := quotient.mk
in setoid.ker (g ∘ f)

def setoid.comp.iso {V : Type} {s : setoid V} {t : setoid (quotient s)} :
    quotient (s.comp t) ≃ quotient t :=
by {
    let f : V -> quotient s := quotient.mk,
    let g : quotient s -> quotient t := quotient.mk',
    let h : V -> quotient (s.comp t) := quotient.mk',

    have p₁ : ∀ {a b}, f a = f b <-> s.rel a b := λ a b, quotient.eq',
    have p₂ : ∀ {a b}, g a = g b <-> t.rel a b := λ a b, quotient.eq',
    have p₃ : ∀ {a b}, h a = h b <-> (s.comp t).rel a b := λ a b, quotient.eq',
    have p₄ : ∀ {a b}, (s.comp t).rel a b <-> g (f a) = g (f b) := λ a b, setoid.ker_def,
    have p₅ : ∀ a b, s.rel a b -> h a = h b := λ a b, by { rw [p₃,p₄,<-p₁], exact congr_arg g },

    let ζ : quotient s -> quotient (s.comp t) := λ y, y.lift_on' h p₅,

    have p₆ : ∀ a b, t.rel a b -> ζ a = ζ b := λ a b, by {
        refine a.induction_on' (λ x, _),
        refine b.induction_on' (λ y, _),
        rw [<-p₂], change g (f x) = g (f y) -> h x = h y, rw [p₃,p₄], exact id
    },

    exact {
        to_fun := λ x, x.lift_on' (g ∘ f) (λ _ _, id),
        inv_fun := λ y, y.lift_on' (λ y, y.lift_on' h p₅) p₆,
        left_inv := λ x, quotient.induction_on' x (λ _, rfl),
        right_inv := λ y, quotient.induction_on' y (λ a, quotient.induction_on' a (λ b, rfl)),
    }
}

It kind of works but there are too many quotient.eq's and quotient.mk's for my taste. Am I missing something?