Problem with Mono/Epi defs in Category.Basic?

Stream: mathlib4

[Mason McBride]

class Epi (f : X ⟶ Y) : Prop where
  /-- A morphism `f` is an epimorphism if it can be cancelled when precomposed. -/
  left_cancellation : ∀ {Z : C} (g h : Y ⟶ Z), f ≫ g = f ≫ h → g = h
#align category_theory.epi CategoryTheory.Epi

/-- A morphism `f` is a monomorphism if it can be cancelled when postcomposed:
`g ≫ f = h ≫ f` implies `g = h`.

See <https://stacks.math.columbia.edu/tag/003B>.
-/
class Mono (f : X ⟶ Y) : Prop where
  /-- A morphism `f` is a monomorphism if it can be cancelled when postcomposed. -/
  right_cancellation : ∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
#align category_theory.mono CategoryTheory.Mono

When \gg is defined this way, it makes it seem like a monomorphism is right cancellative like the above would say, but this wrong. Why is it written this way?

[Kevin Buzzard]

I don't understand your question. Are you claiming the definition is mathematically incorrect, asking about the definition of ≫ (it's "composition but backwards") or what?

[Mason McBride]

It says if f is Monomorphism then if (g ≫ f) = (h ≫ f) -> g = h
Screenshot-2024-03-22-at-5.01.07AM.png
But this is the def of a monomorphism

[Mason McBride]

It's not mathematically incorrect but it's confusing lefts and rights maybe?

[Kevin Buzzard]

Right, and those (lean def, screenshot) are exactly the same thing, right?

[Kevin Buzzard]

I am confused about what you are confused about.

[Yaël Dillies]

f ≫ g = g ∘ f, if that's what you are confused about

[Mason McBride]

no the f is on the right side in Lean and it should be on the left side of LHS and RHS

[Mason McBride]

Yaël Dillies said:

f ≫ g = g ∘ f

yes but why is this done?

[Kevin Buzzard]

Because then in commutative diagrams the maps are composed in the same order that they're written. f ≫ g is "f then g".

[Mason McBride]

Okay I understand this btw I am not confused, I see since writing programs we write left to right and writing commutative diagrams is common so we want to write them left to right. But you can write your commutative diagrams right to left and then not have to flip f and g for no reason (unless the reason above)

[Mason McBride]

Thank you for the insight