More on quotients of categories

[rwbarton]

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 and quotient. 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):

• definition of a hom_rel: Π ⦃a b : C⦄, (a ⟶ b) → (a ⟶ b) → Prop;
• say what it means for a hom_rel to be a congruence;
• closure of a hom_rel as a congruence;
• category.quot for quotient by a hom_rel;
• category.quotient for quotient by a congruence;
• sound and exact for each of these (exact for a category.quot would produce the congruence generated by the original hom_rel);
• construction of the functors given by the universal property of each of these;
• maybe their uniqueness; possibly just up to unique isomorphism.

I may get around to this eventually, but probably not in the immediate future.

cc @dwarn as the original author of category_theory.quotient.

[kim-em]

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.

[b-mehta]

(Just to say that I shouldn't get any credit for that PR, it was @dwarn's work)