# 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 CategoryTheory.Monoidal.FunctorCategory.tensorObj_map {C : Type u₁} [] {D : Type u₂} [] (F : ) (G : ) :
∀ {X Y : C} (f : X Y), = CategoryTheory.MonoidalCategory.tensorHom (F.map f) (G.map f)
@[simp]
theorem CategoryTheory.Monoidal.FunctorCategory.tensorObj_obj {C : Type u₁} [] {D : Type u₂} [] (F : ) (G : ) (X : C) :
def CategoryTheory.Monoidal.FunctorCategory.tensorObj {C : Type u₁} [] {D : Type u₂} [] (F : ) (G : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Monoidal.FunctorCategory.tensorHom_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {F' : } {G' : } (α : F G) (β : F' G') (X : C) :
def CategoryTheory.Monoidal.FunctorCategory.tensorHom {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {F' : } {G' : } (α : F G) (β : F' G') :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Monoidal.FunctorCategory.whiskerLeft_app {C : Type u₁} [] {D : Type u₂} [] {F' : } {G' : } (F : ) (β : F' G') (X : C) :
def CategoryTheory.Monoidal.FunctorCategory.whiskerLeft {C : Type u₁} [] {D : Type u₂} [] {F' : } {G' : } (F : ) (β : F' G') :

(An auxiliary definition for functorCategoryMonoidal.)

Equations
Instances For
@[simp]
theorem CategoryTheory.Monoidal.FunctorCategory.whiskerRight_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : F G) (F' : ) (X : C) :
def CategoryTheory.Monoidal.FunctorCategory.whiskerRight {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (α : F G) (F' : ) :

(An auxiliary definition for functorCategoryMonoidal.)

Equations
Instances For
instance CategoryTheory.Monoidal.functorCategoryMonoidalStruct {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
• One or more equations did not get rendered due to their size.
@[simp]
theorem CategoryTheory.Monoidal.tensorUnit_obj {C : Type u₁} [] {D : Type u₂} [] {X : C} :
(𝟙_ ()).obj X = 𝟙_ D
@[simp]
theorem CategoryTheory.Monoidal.tensorUnit_map {C : Type u₁} [] {D : Type u₂} [] {X : C} {Y : C} {f : X Y} :
(𝟙_ ()).map f =
@[simp]
theorem CategoryTheory.Monoidal.tensorObj_obj {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {X : C} :
@[simp]
theorem CategoryTheory.Monoidal.tensorObj_map {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {X : C} {Y : C} {f : X Y} :
@[simp]
theorem CategoryTheory.Monoidal.tensorHom_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {F' : } {G' : } {α : F G} {β : F' G'} {X : C} :
@[simp]
theorem CategoryTheory.Monoidal.whiskerLeft_app {C : Type u₁} [] {D : Type u₂} [] {F : } {F' : } {G' : } {β : F' G'} {X : C} :
@[simp]
theorem CategoryTheory.Monoidal.whiskerRight_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {F' : } {α : F G} {X : C} :
.app X = CategoryTheory.MonoidalCategory.whiskerRight (α.app X) (F'.obj X)
@[simp]
theorem CategoryTheory.Monoidal.leftUnitor_hom_app {C : Type u₁} [] {D : Type u₂} [] {F : } {X : C} :
.app X = ().hom
@[simp]
theorem CategoryTheory.Monoidal.leftUnitor_inv_app {C : Type u₁} [] {D : Type u₂} [] {F : } {X : C} :
.app X = ().inv
@[simp]
theorem CategoryTheory.Monoidal.rightUnitor_hom_app {C : Type u₁} [] {D : Type u₂} [] {F : } {X : C} :
.app X = ().hom
@[simp]
theorem CategoryTheory.Monoidal.rightUnitor_inv_app {C : Type u₁} [] {D : Type u₂} [] {F : } {X : C} :
.app X = ().inv
@[simp]
theorem CategoryTheory.Monoidal.associator_hom_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {H : } {X : C} :
.hom.app X = (CategoryTheory.MonoidalCategory.associator (F.obj X) (G.obj X) (H.obj X)).hom
@[simp]
theorem CategoryTheory.Monoidal.associator_inv_app {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {H : } {X : C} :
.inv.app X = (CategoryTheory.MonoidalCategory.associator (F.obj X) (G.obj X) (H.obj X)).inv
instance CategoryTheory.Monoidal.functorCategoryMonoidal {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
instance CategoryTheory.Monoidal.functorCategoryBraided {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
• One or more equations did not get rendered due to their size.

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
• CategoryTheory.Monoidal.functorCategorySymmetric =