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.

def CategoryTheory.Monoidal.FunctorCategory.tensorObj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F G : Functor C D) : Functor C D

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

@[simp]

theorem CategoryTheory.Monoidal.FunctorCategory.tensorObj_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F G : Functor C D) (X : C) : (tensorObj F G).obj X = MonoidalCategoryStruct.tensorObj (F.obj X) (G.obj X)

@[simp]

theorem CategoryTheory.Monoidal.FunctorCategory.tensorObj_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F G : Functor C D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (tensorObj F G).map f = MonoidalCategoryStruct.tensorHom (F.map f) (G.map f)

def CategoryTheory.Monoidal.FunctorCategory.tensorHom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F G F' G' : Functor C D} (α : F ⟶ G) (β : F' ⟶ G') : tensorObj F F' ⟶ tensorObj G G'

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

@[simp]

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

def CategoryTheory.Monoidal.FunctorCategory.whiskerLeft {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F' G' : Functor C D} (F : Functor C D) (β : F' ⟶ G') : tensorObj F F' ⟶ tensorObj F G'

(An auxiliary definition for functorCategoryMonoidal.)

@[simp]

theorem CategoryTheory.Monoidal.FunctorCategory.whiskerLeft_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F' G' : Functor C D} (F : Functor C D) (β : F' ⟶ G') (X : C) : (whiskerLeft F β).app X = MonoidalCategoryStruct.whiskerLeft (F.obj X) (β.app X)

def CategoryTheory.Monoidal.FunctorCategory.whiskerRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F G : Functor C D} (α : F ⟶ G) (F' : Functor C D) : tensorObj F F' ⟶ tensorObj G F'

(An auxiliary definition for functorCategoryMonoidal.)

@[simp]

theorem CategoryTheory.Monoidal.FunctorCategory.whiskerRight_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F G : Functor C D} (α : F ⟶ G) (F' : Functor C D) (X : C) : (whiskerRight α F').app X = MonoidalCategoryStruct.whiskerRight (α.app X) (F'.obj X)

instance CategoryTheory.Monoidal.functorCategoryMonoidalStruct {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] : MonoidalCategoryStruct (Functor C D)

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.

@[simp]

theorem CategoryTheory.Monoidal.tensorUnit_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {X : C} : (MonoidalCategoryStruct.tensorUnit (Functor C D)).obj X = MonoidalCategoryStruct.tensorUnit D

@[simp]

theorem CategoryTheory.Monoidal.tensorUnit_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {X Y : C} {f : X ⟶ Y} : (MonoidalCategoryStruct.tensorUnit (Functor C D)).map f = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit D)

@[simp]

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

@[simp]

theorem CategoryTheory.Monoidal.tensorObj_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F G : Functor C D} {X Y : C} {f : X ⟶ Y} : (MonoidalCategoryStruct.tensorObj F G).map f = MonoidalCategoryStruct.tensorHom (F.map f) (G.map f)

@[simp]

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

@[simp]

theorem CategoryTheory.Monoidal.whiskerLeft_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F F' G' : Functor C D} {β : F' ⟶ G'} {X : C} : (MonoidalCategoryStruct.whiskerLeft F β).app X = MonoidalCategoryStruct.whiskerLeft (F.obj X) (β.app X)

@[simp]

theorem CategoryTheory.Monoidal.whiskerRight_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F G F' : Functor C D} {α : F ⟶ G} {X : C} : (MonoidalCategoryStruct.whiskerRight α F').app X = MonoidalCategoryStruct.whiskerRight (α.app X) (F'.obj X)

@[simp]

theorem CategoryTheory.Monoidal.leftUnitor_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {X : C} : (MonoidalCategoryStruct.leftUnitor F).hom.app X = (MonoidalCategoryStruct.leftUnitor (F.obj X)).hom

@[simp]

theorem CategoryTheory.Monoidal.leftUnitor_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {X : C} : (MonoidalCategoryStruct.leftUnitor F).inv.app X = (MonoidalCategoryStruct.leftUnitor (F.obj X)).inv

@[simp]

theorem CategoryTheory.Monoidal.rightUnitor_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {X : C} : (MonoidalCategoryStruct.rightUnitor F).hom.app X = (MonoidalCategoryStruct.rightUnitor (F.obj X)).hom

@[simp]

theorem CategoryTheory.Monoidal.rightUnitor_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F : Functor C D} {X : C} : (MonoidalCategoryStruct.rightUnitor F).inv.app X = (MonoidalCategoryStruct.rightUnitor (F.obj X)).inv

@[simp]

theorem CategoryTheory.Monoidal.associator_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F G H : Functor C D} {X : C} : (MonoidalCategoryStruct.associator F G H).hom.app X = (MonoidalCategoryStruct.associator (F.obj X) (G.obj X) (H.obj X)).hom

@[simp]

theorem CategoryTheory.Monoidal.associator_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] {F G H : Functor C D} {X : C} : (MonoidalCategoryStruct.associator F G H).inv.app X = (MonoidalCategoryStruct.associator (F.obj X) (G.obj X) (H.obj X)).inv

instance CategoryTheory.Monoidal.functorCategoryMonoidal {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] : MonoidalCategory (Functor C D)

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.

instance CategoryTheory.Monoidal.functorCategoryBraided {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [BraidedCategory D] : BraidedCategory (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.

instance CategoryTheory.Monoidal.functorCategorySymmetric {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] [SymmetricCategory D] : SymmetricCategory (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.

instance CategoryTheory.Functor.LaxMonoidal.whiskeringRight {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] [MonoidalCategory D] [MonoidalCategory E] (L : Functor D E) [L.LaxMonoidal] : ((Functor.whiskeringRight C D E).obj L).LaxMonoidal

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.whiskeringRight_ε_app {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] [MonoidalCategory D] [MonoidalCategory E] (L : Functor D E) [L.LaxMonoidal] (X : C) : (ε ((Functor.whiskeringRight C D E).obj L)).app X = ε L

@[simp]

theorem CategoryTheory.Functor.LaxMonoidal.whiskeringRight_μ_app {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] [MonoidalCategory D] [MonoidalCategory E] (L : Functor D E) [L.LaxMonoidal] (F G : Functor C D) (X : C) : (μ ((Functor.whiskeringRight C D E).obj L) F G).app X = μ L (F.obj X) (G.obj X)

instance CategoryTheory.Functor.OplaxMonoidal.whiskeringRight {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] [MonoidalCategory D] [MonoidalCategory E] (L : Functor D E) [L.OplaxMonoidal] : ((Functor.whiskeringRight C D E).obj L).OplaxMonoidal

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.whiskeringRight_η_app {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] [MonoidalCategory D] [MonoidalCategory E] (L : Functor D E) [L.OplaxMonoidal] (X : C) : (η ((Functor.whiskeringRight C D E).obj L)).app X = η L

@[simp]

theorem CategoryTheory.Functor.OplaxMonoidal.whiskeringRight_δ_app {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] [MonoidalCategory D] [MonoidalCategory E] (L : Functor D E) [L.OplaxMonoidal] (F G : Functor C D) (X : C) : (δ ((Functor.whiskeringRight C D E).obj L) F G).app X = δ L (F.obj X) (G.obj X)

instance CategoryTheory.instMonoidalFunctorObjWhiskeringRight {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] [MonoidalCategory D] [MonoidalCategory E] (L : Functor D E) [L.Monoidal] : ((Functor.whiskeringRight C D E).obj L).Monoidal

@[deprecated CategoryTheory.Functor.LaxMonoidal.whiskeringRight (since := "2025-11-06")]

def CategoryTheory.instLaxMonoidalFunctorObjWhiskeringRight {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] [MonoidalCategory D] [MonoidalCategory E] (L : Functor D E) [L.LaxMonoidal] : ((Functor.whiskeringRight C D E).obj L).LaxMonoidal

Alias of CategoryTheory.Functor.LaxMonoidal.whiskeringRight.

@[deprecated CategoryTheory.Functor.OplaxMonoidal.whiskeringRight (since := "2025-11-06")]

def CategoryTheory.instOplaxMonoidalFunctorObjWhiskeringRight {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] [MonoidalCategory D] [MonoidalCategory E] (L : Functor D E) [L.OplaxMonoidal] : ((Functor.whiskeringRight C D E).obj L).OplaxMonoidal

Alias of CategoryTheory.Functor.OplaxMonoidal.whiskeringRight.

@[deprecated CategoryTheory.Functor.LaxMonoidal.whiskeringRight_ε_app (since := "2025-11-06")]

theorem CategoryTheory.ε_app {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] [MonoidalCategory D] [MonoidalCategory E] (L : Functor D E) [L.LaxMonoidal] (X : C) : (Functor.LaxMonoidal.ε ((Functor.whiskeringRight C D E).obj L)).app X = Functor.LaxMonoidal.ε L

Alias of CategoryTheory.Functor.LaxMonoidal.whiskeringRight_ε_app.

@[deprecated CategoryTheory.Functor.LaxMonoidal.whiskeringRight_μ_app (since := "2025-11-06")]

theorem CategoryTheory.μ_app {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] [MonoidalCategory D] [MonoidalCategory E] (L : Functor D E) [L.LaxMonoidal] (F G : Functor C D) (X : C) : (Functor.LaxMonoidal.μ ((Functor.whiskeringRight C D E).obj L) F G).app X = Functor.LaxMonoidal.μ L (F.obj X) (G.obj X)

Alias of CategoryTheory.Functor.LaxMonoidal.whiskeringRight_μ_app.

@[deprecated CategoryTheory.Functor.OplaxMonoidal.whiskeringRight_η_app (since := "2025-11-06")]

theorem CategoryTheory.η_app {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] [MonoidalCategory D] [MonoidalCategory E] (L : Functor D E) [L.OplaxMonoidal] (X : C) : (Functor.OplaxMonoidal.η ((Functor.whiskeringRight C D E).obj L)).app X = Functor.OplaxMonoidal.η L

Alias of CategoryTheory.Functor.OplaxMonoidal.whiskeringRight_η_app.

@[deprecated CategoryTheory.Functor.OplaxMonoidal.whiskeringRight_δ_app (since := "2025-11-06")]

theorem CategoryTheory.δ_app {C : Type u_1} {D : Type u_2} {E : Type u_3} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Category.{v_3, u_3} E] [MonoidalCategory D] [MonoidalCategory E] (L : Functor D E) [L.OplaxMonoidal] (F G : Functor C D) (X : C) : (Functor.OplaxMonoidal.δ ((Functor.whiskeringRight C D E).obj L) F G).app X = Functor.OplaxMonoidal.δ L (F.obj X) (G.obj X)

Alias of CategoryTheory.Functor.OplaxMonoidal.whiskeringRight_δ_app.

instance CategoryTheory.Functor.Monoidal.whiskeringLeft {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : Type u_1) [Category.{v_1, u_1} E] [MonoidalCategory E] (F : Functor C D) : ((Functor.whiskeringLeft C D E).obj F).Monoidal

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskeringLeft_δ_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : Type u_1) [Category.{v_1, u_1} E] [MonoidalCategory E] (F : Functor C D) (X Y : Functor D E) (X✝ : C) : (OplaxMonoidal.δ ((Functor.whiskeringLeft C D E).obj F) X Y).app X✝ = CategoryStruct.id (MonoidalCategoryStruct.tensorObj (X.obj (F.obj X✝)) (Y.obj (F.obj X✝)))

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskeringLeft_η_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : Type u_1) [Category.{v_1, u_1} E] [MonoidalCategory E] (F : Functor C D) (X : C) : (OplaxMonoidal.η ((Functor.whiskeringLeft C D E).obj F)).app X = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit E)

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskeringLeft_ε_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : Type u_1) [Category.{v_1, u_1} E] [MonoidalCategory E] (F : Functor C D) (X : C) : (LaxMonoidal.ε ((Functor.whiskeringLeft C D E).obj F)).app X = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit E)

@[simp]

theorem CategoryTheory.Functor.Monoidal.whiskeringLeft_μ_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : Type u_1) [Category.{v_1, u_1} E] [MonoidalCategory E] (F : Functor C D) (X Y : Functor D E) (X✝ : C) : (LaxMonoidal.μ ((Functor.whiskeringLeft C D E).obj F) X Y).app X✝ = CategoryStruct.id (MonoidalCategoryStruct.tensorObj (X.obj (F.obj X✝)) (Y.obj (F.obj X✝)))

instance CategoryTheory.instMonoidalFunctorFunctorCongrLeft {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : Type u_1) [Category.{v_1, u_1} E] [MonoidalCategory E] (e : C ≌ D) : e.congrLeft.functor.Monoidal

instance CategoryTheory.instMonoidalFunctorInverseCongrLeft {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : Type u_1) [Category.{v_1, u_1} E] [MonoidalCategory E] (e : C ≌ D) : e.congrLeft.inverse.Monoidal

instance CategoryTheory.instIsMonoidalFunctorCongrLeft {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : Type u_1) [Category.{v_1, u_1} E] [MonoidalCategory E] (e : C ≌ D) : e.congrLeft.IsMonoidal