# mathlibdocumentation

category_theory.monoidal.functor_category

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

@[simp]
theorem category_theory.monoidal.functor_category.tensor_obj_obj {C : Type u₁} {D : Type u₂} (F G : C D) (X : C) :
= F.obj X G.obj X
def category_theory.monoidal.functor_category.tensor_obj {C : Type u₁} {D : Type u₂} (F G : C D) :
C D

(An auxiliary definition for functor_category_monoidal.) Tensor product of functors C ⥤ D, when D is monoidal.

Equations
@[simp]
theorem category_theory.monoidal.functor_category.tensor_obj_map {C : Type u₁} {D : Type u₂} (F G : C D) (X Y : C) (f : X Y) :
= F.map f G.map f
@[simp]
theorem category_theory.monoidal.functor_category.tensor_hom_app {C : Type u₁} {D : Type u₂} {F G F' G' : C D} (α : F G) (β : F' G') (X : C) :
= α.app X β.app X
def category_theory.monoidal.functor_category.tensor_hom {C : Type u₁} {D : Type u₂} {F G F' G' : C D} (α : F G) (β : F' G') :

(An auxiliary definition for functor_category_monoidal.) Tensor product of natural transformations into D, when D is monoidal.

Equations
@[protected, instance]
def category_theory.monoidal.functor_category_monoidal {C : Type u₁} {D : Type u₂}  :

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
@[simp]
theorem category_theory.monoidal.tensor_unit_obj {C : Type u₁} {D : Type u₂} {X : C} :
(𝟙_ (C D)).obj X = 𝟙_ D
@[simp]
theorem category_theory.monoidal.tensor_unit_map {C : Type u₁} {D : Type u₂} {X Y : C} {f : X Y} :
(𝟙_ (C D)).map f = 𝟙 (𝟙_ D)
@[simp]
theorem category_theory.monoidal.tensor_obj_obj {C : Type u₁} {D : Type u₂} {F G : C D} {X : C} :
(F G).obj X = F.obj X G.obj X
@[simp]
theorem category_theory.monoidal.tensor_obj_map {C : Type u₁} {D : Type u₂} {F G : C D} {X Y : C} {f : X Y} :
(F G).map f = F.map f G.map f
@[simp]
theorem category_theory.monoidal.tensor_hom_app {C : Type u₁} {D : Type u₂} {F G F' G' : C D} {α : F G} {β : F' G'} {X : C} :
β).app X = α.app X β.app X
@[simp]
theorem category_theory.monoidal.left_unitor_hom_app {C : Type u₁} {D : Type u₂} {F : C D} {X : C} :
(λ_ F).hom.app X = (λ_ (F.obj X)).hom
@[simp]
theorem category_theory.monoidal.left_unitor_inv_app {C : Type u₁} {D : Type u₂} {F : C D} {X : C} :
(λ_ F).inv.app X = (λ_ (F.obj X)).inv
@[simp]
theorem category_theory.monoidal.right_unitor_hom_app {C : Type u₁} {D : Type u₂} {F : C D} {X : C} :
(ρ_ F).hom.app X = (ρ_ (F.obj X)).hom
@[simp]
theorem category_theory.monoidal.right_unitor_inv_app {C : Type u₁} {D : Type u₂} {F : C D} {X : C} :
(ρ_ F).inv.app X = (ρ_ (F.obj X)).inv
@[simp]
theorem category_theory.monoidal.associator_hom_app {C : Type u₁} {D : Type u₂} {F G H : C D} {X : C} :
(α_ F G H).hom.app X = (α_ (F.obj X) (G.obj X) (H.obj X)).hom
@[simp]
theorem category_theory.monoidal.associator_inv_app {C : Type u₁} {D : Type u₂} {F G H : C D} {X : C} :
(α_ F G H).inv.app X = (α_ (F.obj X) (G.obj X) (H.obj X)).inv
@[protected, instance]
def category_theory.monoidal.functor_category_braided {C : Type u₁} {D : Type u₂}  :

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
@[protected, instance]
def category_theory.monoidal.functor_category_symmetric {C : Type u₁} {D : Type u₂}  :

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.

Equations