Quotients by functions

Stream: general

[Violeta Hernández]

I'm interested in quotienting a set by a function, so that if f a = f b, then the corresponding quotients are equal. This seems like a common enough use case to have its own dedicated name and theorems. Is this something that exists?

[Kyle Miller]

docs#setoid.ker is the setoid for that

[Violeta Hernández]

What's the difference between a setoid and a quot? Being honest, I don't really fully understand either of them.

[Kyle Miller]

setoid is just an equivalence relation, and you still need to feed it to docs#quotient or docs#quot

[Violeta Hernández]

Ah thanks, I think I'm getting the hang of it

[Kyle Miller]

What quotient does is give you the ⟦a⟧ syntax, using some implicit argument magic to turn it into the correct quot.mk incantation.

[Kyle Miller]

But it's also somewhat awkward because quotient lemmas expect the setoid to come from a typeclass instance. Depending on what you're doing, you might either use setoid.ker to define a setoid instance for your type, or you might write things like quot.mk (setoid.ker f).rel a directly.

[Kyle Miller]

Like, docs#setoid.ker_apply_mk_out looks nice in the documentation, but it takes some contortions to use the quotient interface:

lemma ker_apply_mk_out {f : α → β} (a : α) :
  f (by haveI := setoid.ker f; exact ⟦a⟧.out) = f a := ...

[Violeta Hernández]

Yeah, I'm having to make a lot of arguments explicit here

[Joe Hendrix]

I'm not sure if this helps, but the convention I adapted the last time I used a quotient was to define a type that had all the operations on them along with proofs they preserved the equivalence relation. Then I defined the quotient type and the operations on the quotient type using quotient.lift.

[Joe Hendrix]

Here's some relevant code for building finite sets on top of ordered trees.

[Kyle Miller]

There are also these sorts of tricks you can do, which let you work with quotients of the same type by multiple different functions, while still giving you access to lemmas like quotient.eq:

import data.setoid.basic

def with_fmod {α β : Type*} (f : α → β) := α

instance with_fmod.setoid {α β : Type*} (f : α → β) : setoid (with_fmod f) := setoid.ker f

variables {α β : Type*}

def fmod (f : α → β) (x : α) : quotient (with_fmod.setoid f) := ⟦x⟧

example (f : α → β) (x y : α) : fmod f x = fmod f y ↔ f x = f y :=
begin
  dunfold fmod,
  rw [quotient.eq, ← setoid.ker_def],
  refl,
end

[Eric Wieser]

If the instance arguments are annoying, use docs#quotient.mk' and the other primed definitions instead

[Anne Baanen]

Naïve question: is there any reason to prefer the quotient by f over docs#set.range?

[Eric Wieser]

Yes, because you can extract both a and f a computably from terms of the former