# Zulip Chat Archive

## Stream: maths

### Topic: quotient classes

#### Chris Hughes (Feb 08 2019 at 00:55):

Can I suggest the creation of something a bit like this. `quotient_map`

can be extended with `group_hom`

, `linear_map`

`localisation_map`

, etc., and used to do definitions on quotient objects that are not defined using the `quot`

constant. I'm considering a major refactoring using something like this.

import logic.function data.quot open function structure quotient_map (α β : Type*) := (to_fun : α → β) (inv_fun : trunc {f : β → α // right_inverse f to_fun})

#### Kenny Lau (Feb 08 2019 at 00:55):

I don't think you can prove that quotienting by a setoid is a `quotient_map`

#### Mario Carneiro (Feb 08 2019 at 01:03):

I think this is not the right assumption. The inverse map should be `B -> quotient (to_fun ⁻¹'o eq)`

#### Mario Carneiro (Feb 08 2019 at 01:03):

and it should be an equiv when paired with the lift of `to_fun`

#### Mario Carneiro (Feb 08 2019 at 01:05):

(this might be a use for `is_equiv`

, if that was ever added for the category stuff)

#### Kenny Lau (Feb 08 2019 at 01:09):

`quot`

is important because it is the only thing that can reach other universes

#### Chris Hughes (Feb 08 2019 at 13:00):

I think you actually mean `set.preimage f ∘ eq ∘ f`

, though I've no idea why you'd write it like this.

#### Chris Hughes (Feb 08 2019 at 13:05):

Or even better `(∘ f) ∘ eq ∘ f`

#### Kevin Buzzard (Feb 08 2019 at 14:00):

for some interpretations of "better", at least :-)

#### Mario Carneiro (Feb 08 2019 at 21:26):

I admit what I wrote is not quite type correct, but I do mean what I wrote. (That notation is `order.preimage`

.) We should have a setoid construction for this case since it's a very common situation (it is also universal, any equivalence relation can be written as f x = f y for an appropriate f), but there is already an easy proof using `preimage.equivalence`

and `eq.equivalence`

.

Last updated: May 18 2021 at 08:14 UTC