Zulip Chat Archive

Stream: general

Topic: Quotients by functions


Violeta Hernández (Dec 24 2021 at 05:56):

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 (Dec 24 2021 at 05:59):

docs#setoid.ker is the setoid for that

Violeta Hernández (Dec 24 2021 at 06:00):

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

Kyle Miller (Dec 24 2021 at 06:02):

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

Violeta Hernández (Dec 24 2021 at 06:04):

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

Kyle Miller (Dec 24 2021 at 06:04):

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 (Dec 24 2021 at 06:09):

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 (Dec 24 2021 at 06:10):

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 (Dec 24 2021 at 06:13):

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

Joe Hendrix (Dec 24 2021 at 06:17):

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 (Dec 24 2021 at 06:19):

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

Kyle Miller (Dec 24 2021 at 06:32):

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 (Dec 24 2021 at 08:24):

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

Anne Baanen (Dec 24 2021 at 10:29):

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

Eric Wieser (Dec 24 2021 at 11:22):

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


Last updated: Dec 20 2023 at 11:08 UTC