## 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