mathlib documentation

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.

(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_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) :

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

Equations
@[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]
theorem category_theory.monoidal.tensor_unit_map {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {X Y : C} {f : X Y} :
(𝟙_ (C D)).map f = 𝟙 (𝟙_ D)
@[simp]
theorem category_theory.monoidal.tensor_obj_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {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₁} [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.left_unitor_hom_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {F : C D} {X : C} :
(ρ_ F).inv.app X = (ρ_ (F.obj X)).inv
@[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
@[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
@[instance]

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