category — Mathlib

English

There is a category structure on the single object category for a monoid M, where composition corresponds to multiplication.

Русский

Существует категориальная структура на однообъектной категории для моид М, где композиция соответствует умножению.

LaTeX

$$$ \text{CategoryTheory.SingleObj.M} \text{ induces a category with } f \circ g = fg. $$$

Lean4

/-- Monoid laws become category laws for the single object category. -/
instance category : Category (SingleObj M) where
  comp_id := one_mul
  id_comp := mul_one
  assoc x y z := (mul_assoc z y x).symm

Похожие утверждения