endofunctorMonoidalCategory — Mathlib

Lean4
/-- The category of endofunctors of any category is a monoidal category,
with tensor product given by composition of functors
(and horizontal composition of natural transformations).

Note: due to the fact that composition of functors in mathlib is reversed compared to the
one usually found in the literature, this monoidal structure is in fact the monoidal
opposite of the one usually considered in the literature.
-/
def endofunctorMonoidalCategory : MonoidalCategory (C ⥤ C)
    where
  tensorObj F G := F ⋙ G
  whiskerLeft X _ _ F := Functor.whiskerLeft X F
  whiskerRight F X := Functor.whiskerRight F X
  tensorHom α β := α ◫ β
  tensorUnit := 𝟭 C
  associator F G H := Functor.associator F G H
  leftUnitor F := Functor.leftUnitor F
  rightUnitor F := Functor.rightUnitor F
Похожие утверждения