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
- category_theory.endofunctor_monoidal_category C = {tensor_obj := λ (F G : C ⥤ C), F ⋙ G, tensor_hom := λ (F G F' G' : C ⥤ C) (α : F ⟶ G) (β : F' ⟶ G'), α ◫ β, tensor_id' := _, tensor_comp' := _, tensor_unit := 𝟭 C _inst_1, associator := λ (F G H : C ⥤ C), F.associator G H, associator_naturality' := _, left_unitor := λ (F : C ⥤ C), F.left_unitor, left_unitor_naturality' := _, right_unitor := λ (F : C ⥤ C), F.right_unitor, right_unitor_naturality' := _, pentagon' := _, triangle' := _}
def
category_theory.tensoring_right_monoidal
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C] :
category_theory.monoidal_functor C (C ⥤ C)
Tensoring on the right gives a monoidal functor from C into endofunctors of C.
Equations
- category_theory.tensoring_right_monoidal C = {to_lax_monoidal_functor := {to_functor := {obj := (category_theory.monoidal_category.tensoring_right C).obj, map := (category_theory.monoidal_category.tensoring_right C).map, map_id' := _, map_comp' := _}, ε := (category_theory.monoidal_category.right_unitor_nat_iso C).inv, μ := λ (X Y : C), {app := λ (Z : C), (α_ Z X Y).hom, naturality' := _}, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}, ε_is_iso := category_theory.nat_iso.is_iso_of_is_iso_app' {to_functor := {obj := (category_theory.monoidal_category.tensoring_right C).obj, map := (category_theory.monoidal_category.tensoring_right C).map, map_id' := _, map_comp' := _}, ε := (category_theory.monoidal_category.right_unitor_nat_iso C).inv, μ := λ (X Y : C), {app := λ (Z : C), (α_ Z X Y).hom, naturality' := _}, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}.ε (λ (X : C), category_theory.nat_iso.inv_app_is_iso (category_theory.monoidal_category.right_unitor_nat_iso C) X), μ_is_iso := λ (X Y : C), {inv := {app := λ (Z : C), (α_ Z X Y).inv, naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}}
@[simp]
@[simp]
theorem
category_theory.tensoring_right_monoidal_ε_is_iso
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C] :
(category_theory.tensoring_right_monoidal C).ε_is_iso = category_theory.nat_iso.is_iso_of_is_iso_app' {to_functor := {obj := (category_theory.monoidal_category.tensoring_right C).obj, map := (category_theory.monoidal_category.tensoring_right C).map, map_id' := _, map_comp' := _}, ε := (category_theory.monoidal_category.right_unitor_nat_iso C).inv, μ := λ (X Y : C), {app := λ (Z : C), (α_ Z X Y).hom, naturality' := _}, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}.ε
@[simp]
theorem
category_theory.tensoring_right_monoidal_μ_is_iso_inv_app
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C]
(X Y Z : C) :
(category_theory.is_iso.inv ({to_functor := {obj := (category_theory.monoidal_category.tensoring_right C).obj, map := (category_theory.monoidal_category.tensoring_right C).map, map_id' := _, map_comp' := _}, ε := (category_theory.monoidal_category.right_unitor_nat_iso C).inv, μ := λ (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
@[simp]
theorem
category_theory.tensoring_right_monoidal_to_lax_monoidal_functor_μ_app
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C]
(X Y Z : C) :
((category_theory.tensoring_right_monoidal C).to_lax_monoidal_functor.μ X Y).app Z = (α_ Z X Y).hom
@[simp]