Open rwbarton opened 4 years ago
Just updating this issue. The current state of mathlib, after @b-mehta's #7501, is that we have a class
/-- A `hom_rel` is a congruence when it's an equivalence on every hom-set, and it can be composed
from left and right. -/
class congruence (r : hom_rel C) : Prop :=
(is_equiv : ∀ {X Y}, is_equiv _ (@r X Y))
(comp_left : ∀ {X Y Z} (f : X ⟶ Y) {g g' : Y ⟶ Z}, r g g' → r (f ≫ g) (f ≫ g'))
(comp_right : ∀ {X Y Z} {f f' : X ⟶ Y} (g : Y ⟶ Z), r f f' → r (f ≫ g) (f' ≫ g))
and a lemma
lemma functor_map_eq_iff [congruence r] {X Y : C} (f f' : X ⟶ Y) :
(functor r).map f = (functor r).map f' ↔ r f f' := ...
This is not the API setup that @rwbarton proposed above: in particular we still only have category.quotient
(which would be Reid's proposed category.quot
), rather than having two separate constructions.
I think this issue should remain open --- Reid's API is still an improvement over what we have. Happily, after the subsequent PRs, I think it would be quite easy to implement. It's just a bit of refactoring.
(Just to say that I shouldn't get any credit for that PR, it was @dwarn's work)
In
category_theory.quotient
we currently have a construction of the quotient of a category by an arbitrary relation on the Hom-sets, and half of its universal property (we could also prove the factorization through the quotient is unique).In https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.2/src/category_theory/congruence.lean I have the quotient of a category by a congruence (an equivalence relation closed under composition). The advantage of knowing that you are in this situation is that two morphisms become equal in the quotient if and only if they are already related. This situation arises in homotopy theory and homological algebra, e.g., homotopy and chain homotopy are congruences.
The whole situation is analogous to the relationship between relations and equivalence relations, and between
quot
andquotient
. Thus, I suggest that we should merge these into a file containing the following (off the top of my head, list may not be exhaustive):hom_rel
:Π ⦃a b : C⦄, (a ⟶ b) → (a ⟶ b) → Prop
;hom_rel
to be a congruence;hom_rel
as a congruence;category.quot
for quotient by ahom_rel
;category.quotient
for quotient by a congruence;sound
andexact
for each of these (exact
for acategory.quot
would produce the congruence generated by the originalhom_rel
);I may get around to this eventually, but probably not in the immediate future.
cc @dwarn as the original author of
category_theory.quotient
.