Monoidal structure on `C ⥤ D` when `D` is monoidal. #

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.

source

@[simp]

theorem CategoryTheory.Monoidal.tensorUnit_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {X : C} :

(CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Functor C D)).obj X = CategoryTheory.MonoidalCategory.tensorUnit D

source

@[simp]

theorem CategoryTheory.Monoidal.tensorUnit_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {X : C} {Y : C} {f : X ⟶ Y} :

(CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Functor C D)).map f = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit D)

source

@[simp]

theorem CategoryTheory.Monoidal.tensorObj_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {X : C} :

(CategoryTheory.MonoidalCategory.tensorObj F G).obj X = CategoryTheory.MonoidalCategory.tensorObj (F.obj X) (G.obj X)

source

@[simp]

theorem CategoryTheory.Monoidal.tensorObj_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {X : C} {Y : C} {f : X ⟶ Y} :

(CategoryTheory.MonoidalCategory.tensorObj F G).map f = CategoryTheory.MonoidalCategory.tensorHom (F.map f) (G.map f)

source

@[simp]

theorem CategoryTheory.Monoidal.tensorHom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {F' : CategoryTheory.Functor C D} {G' : CategoryTheory.Functor C D} {α : F ⟶ G} {β : F' ⟶ G'} {X : C} :

(CategoryTheory.MonoidalCategory.tensorHom α β).app X = CategoryTheory.MonoidalCategory.tensorHom (α.app X) (β.app X)

source

@[simp]

theorem CategoryTheory.Monoidal.leftUnitor_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} {X : C} :

(CategoryTheory.MonoidalCategory.leftUnitor F).hom.app X = (CategoryTheory.MonoidalCategory.leftUnitor (F.obj X)).hom

source

@[simp]

theorem CategoryTheory.Monoidal.leftUnitor_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} {X : C} :

(CategoryTheory.MonoidalCategory.leftUnitor F).inv.app X = (CategoryTheory.MonoidalCategory.leftUnitor (F.obj X)).inv

source

@[simp]

theorem CategoryTheory.Monoidal.rightUnitor_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} {X : C} :

(CategoryTheory.MonoidalCategory.rightUnitor F).hom.app X = (CategoryTheory.MonoidalCategory.rightUnitor (F.obj X)).hom

source

@[simp]

theorem CategoryTheory.Monoidal.rightUnitor_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} {X : C} :

(CategoryTheory.MonoidalCategory.rightUnitor F).inv.app X = (CategoryTheory.MonoidalCategory.rightUnitor (F.obj X)).inv

source

@[simp]

theorem CategoryTheory.Monoidal.associator_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor C D} {X : C} :

(CategoryTheory.MonoidalCategory.associator F G H).hom.app X = (CategoryTheory.MonoidalCategory.associator (F.obj X) (G.obj X) (H.obj X)).hom

source

@[simp]

theorem CategoryTheory.Monoidal.associator_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor C D} {X : C} :

(CategoryTheory.MonoidalCategory.associator F G H).inv.app X = (CategoryTheory.MonoidalCategory.associator (F.obj X) (G.obj X) (H.obj X)).inv

source

instance CategoryTheory.Monoidal.functorCategoryBraided {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] :

CategoryTheory.BraidedCategory (CategoryTheory.Functor C D)

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.

source

instance CategoryTheory.Monoidal.functorCategorySymmetric {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] :

CategoryTheory.SymmetricCategory (CategoryTheory.Functor C D)

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.

Monoidal structure on C ⥤ D when D is monoidal. #

Monoidal structure on `C ⥤ D` when `D` is monoidal. #