Documentation

Mathlib.CategoryTheory.Monoidal.End

Endofunctors as a monoidal category. #

We give the monoidal category structure on C ⥤ C, and show that when C itself is monoidal, it embeds via a monoidal functor into C ⥤ C.

TODO #

Can we use this to show coherence results, e.g. a cheap proof that λ_ (𝟙_ C) = ρ_ (𝟙_ C)? I suspect this is harder than is usually made out.

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).

Instances For

    Tensoring on the right gives a monoidal functor from C into endofunctors of C.

    Instances For
      theorem CategoryTheory.μ_naturality₂ {C : Type u} [CategoryTheory.Category.{v, u} C] {M : Type u_1} [CategoryTheory.Category.{u_2, u_1} M] [CategoryTheory.MonoidalCategory M] (F : CategoryTheory.MonoidalFunctor M (CategoryTheory.Functor C C)) {m : M} {n : M} {m' : M} {n' : M} (f : m m') (g : n n') (X : C) :
      CategoryTheory.CategoryStruct.comp ((F.map g).app ((F.obj m).obj X)) (CategoryTheory.CategoryStruct.comp ((F.obj n').map ((F.map f).app X)) ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m' n').app X)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor m n).app X) ((F.map (CategoryTheory.MonoidalCategory.tensorHom f g)).app X)