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: Aug 03 2023 at 10:10 UTC