# mathlibdocumentation

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

Equations
@[simp]
theorem category_theory.tensoring_right_monoidal_μ_is_iso_inv_app (C : Type u) (X Y Z : C) :
(category_theory.is_iso.inv ({to_functor := , ε := , μ := λ (X Y : C), {app := λ (Z : C), (α_ Z X Y).hom, naturality' := _}, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}.μ X Y)).app Z = (α_ Z X Y).inv

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

Equations
@[simp]

@[simp]

@[simp]