Zulip Chat Archive
Stream: triage
Topic: issue #2710: More on quotients of categories
Random Issue Bot (Dec 18 2020 at 14:27):
Today I chose issue 2710 for discussion!
More on quotients of categories
Created by @Reid Barton (@rwbarton) on 2020-05-17
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Mar 10 2021 at 14:24):
Today I chose issue 2710 for discussion!
More on quotients of categories
Created by @Reid Barton (@rwbarton) on 2020-05-17
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Apr 04 2021 at 14:39):
Today I chose issue 2710 for discussion!
More on quotients of categories
Created by @Reid Barton (@rwbarton) on 2020-05-17
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Oct 01 2021 at 16:49):
Today I chose issue 2710 for discussion!
More on quotients of categories
Created by @Reid Barton (@rwbarton) on 2020-05-17
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Scott Morrison (Oct 01 2021 at 21:40):
Random Issue Bot said:
More on quotients of categories
Created by Reid Barton (@rwbarton) on 2020-05-17
Labels: feature-request
Just updating this issue (crossposted on github). 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.
Random Issue Bot (Mar 02 2022 at 14:13):
Today I chose issue 2710 for discussion!
More on quotients of categories
Created by @Reid Barton (@rwbarton) on 2020-05-17
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jun 23 2022 at 14:19):
Today I chose issue 2710 for discussion!
More on quotients of categories
Created by @Reid Barton (@rwbarton) on 2020-05-17
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Dec 04 2022 at 14:08):
Today I chose issue 2710 for discussion!
More on quotients of categories
Created by @Reid Barton (@rwbarton) on 2020-05-17
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Last updated: Dec 20 2023 at 11:08 UTC