mathlib3 documentation

category_theory.monoidal.functor_category

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

Equations

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

Equations
@[protected, instance]

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]
@[simp]
theorem category_theory.monoidal.tensor_obj_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {F G F' G' : C D} {α : F G} {β : F' G'} {X : C} :
β).app X = α.app X β.app X
@[simp]
theorem category_theory.monoidal.associator_hom_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {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]

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