quotient classes

Stream: maths

[Chris Hughes]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

(this might be a use for is_equiv, if that was ever added for the category stuff)

[Kenny Lau]

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

[Chris Hughes]

I think you actually mean set.preimage f ∘ eq ∘ f, though I've no idea why you'd write it like this.

[Chris Hughes]

Or even better (∘ f) ∘ eq ∘ f

[Kevin Buzzard]

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

[Mario Carneiro]

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.