Zulip Chat Archive
Stream: general
Topic: category_theory.epi and category_theory.mono
Utensil Song (Aug 11 2020 at 15:41):
Alex J. Best (Aug 11 2020 at 15:41):
The composition operator >> is the reverse of the "standard" order.
Utensil Song (Aug 11 2020 at 15:42):
I'm a little confused by the left/right naming here and it seems to be inconsistent with Wikipedia.
(Ignore the typo, PRed as #3741 )
Bryan Gin-ge Chen (Aug 11 2020 at 15:46):
Right-cancellative for the standard composition operator \circ (used in Wikipedia) is left-cancellative for the composition operator \>> used in category_theory (see docs) since f \circ g = g \>> f.
Utensil Song (Aug 11 2020 at 15:46):
I understand that it's in the "arrow" order. But isn't it "right-cancellative" in that "arrow" order for Epimorphism? (Both in Wikipedia and texts)
Utensil Song (Aug 11 2020 at 15:50):
Oh, I see, I got the "left/right-cancellative" wrong. left/right stands for the position of the morphism, not where the cancellation happened.
Utensil Song (Aug 11 2020 at 15:52):
Because I got a text using wordings like "canceled out of morphism equations on the left/right", hence the confusion.
Kevin Buzzard (Aug 11 2020 at 17:15):
Mathlib was not consistent in their use of ..._left_cancel_... for a long time. I think that recently they tried to tighten things up.
Simon Hudon (Aug 11 2020 at 17:16):
@Kevin Buzzard I'm glad to hear that it's improving. What is the convention that the consensus is favoring?
Reid Barton (Aug 11 2020 at 17:19):
This is kind of a different issue though--"left cancellative" is apparently a standard piece of math terminology--I'm not sure I would know off the top of my head which way it goes, but I definitely know e.g. what a left inverse of a map is, and the category theory library gives it the wrong meaning
Reid Barton (Aug 11 2020 at 17:19):
(this is just an example, I'm not sure that "left inverse" is a concept which currently exists in the category theory library)
Adam Topaz (Aug 11 2020 at 17:20):
I always get confused by left/right anyway. I actually like the "pre/postcompose" terminology.
Kevin Buzzard (Aug 11 2020 at 17:26):
@Simon Hudon I was thinking of this PR
Simon Hudon (Aug 11 2020 at 17:28):
If I summarize then right_cancel means the thing that's disappearing is on the right. That's appealing to me because I usually assume that's what it means and sometimes get confused
Last updated: Dec 20 2023 at 11:08 UTC