Monoidal structure on C ⥤ D
when D
is monoidal. #
When C
is any category, and D
is a monoidal category,
there is a natural "pointwise" monoidal structure on C ⥤ D
.
The initial intended application is tensor product of presheaves.
(An auxiliary definition for functor_category_monoidal
.)
Tensor product of functors C ⥤ D
, when D
is monoidal.
(An auxiliary definition for functor_category_monoidal
.)
Tensor product of natural transformations into D
, when D
is monoidal.
Equations
- category_theory.monoidal.functor_category.tensor_hom α β = {app := λ (X : C), α.app X ⊗ β.app X, naturality' := _}
When C
is any category, and D
is a monoidal category,
the functor category C ⥤ D
has a natural pointwise monoidal structure,
where (F ⊗ G).obj X = F.obj X ⊗ G.obj X
.
Equations
- category_theory.monoidal.functor_category_monoidal = {tensor_obj := λ (F G : C ⥤ D), category_theory.monoidal.functor_category.tensor_obj F G, tensor_hom := λ (F G F' G' : C ⥤ D) (α : F ⟶ G) (β : F' ⟶ G'), category_theory.monoidal.functor_category.tensor_hom α β, tensor_id' := _, tensor_comp' := _, tensor_unit := (category_theory.functor.const C).obj (𝟙_ D), associator := λ (F G H : C ⥤ D), category_theory.nat_iso.of_components (λ (X : C), α_ (F.obj X) (G.obj X) (H.obj X)) _, associator_naturality' := _, left_unitor := λ (F : C ⥤ D), category_theory.nat_iso.of_components (λ (X : C), λ_ (F.obj X)) _, left_unitor_naturality' := _, right_unitor := λ (F : C ⥤ D), category_theory.nat_iso.of_components (λ (X : C), ρ_ (F.obj X)) _, right_unitor_naturality' := _, pentagon' := _, triangle' := _}
When C
is any category, and D
is a braided monoidal category,
the natural pointwise monoidal structure on the functor category C ⥤ D
is also braided.
Equations
- category_theory.monoidal.functor_category_braided = {braiding := λ (F G : C ⥤ D), category_theory.nat_iso.of_components (λ (X : C), β_ (F.obj X) (G.obj X)) _, braiding_naturality' := _, hexagon_forward' := _, hexagon_reverse' := _}
When C
is any category, and D
is a symmetric monoidal category,
the natural pointwise monoidal structure on the functor category C ⥤ D
is also symmetric.