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.

source
@[simp]
theorem category_theory.monoidal.functor_category.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) :
(category_theory.monoidal.functor_category.tensor_obj F G).obj X = F.obj X ⊗ G.obj X
source
def category_theory.monoidal.functor_category.tensor_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] (F G : C ⥤ D) :
C ⥤ D

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

Equations
source
@[simp]
theorem category_theory.monoidal.functor_category.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) :
(category_theory.monoidal.functor_category.tensor_obj F G).map f = F.map f ⊗ G.map f
source
@[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) :
(category_theory.monoidal.functor_category.tensor_hom α β).app X = α.app X ⊗ β.app X
source
def category_theory.monoidal.functor_category.tensor_hom {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') :
category_theory.monoidal.functor_category.tensor_obj F F' ⟶ category_theory.monoidal.functor_category.tensor_obj G G'

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

Equations
source
@[protected, instance]
def category_theory.monoidal.functor_category_monoidal {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] :
category_theory.monoidal_category (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.

Equations
source
@[simp]
theorem category_theory.monoidal.tensor_unit_obj {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] {X : C} :
(𝟙_ (C ⥤ D)).obj X = 𝟙_ D
source
@[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)
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[protected, instance]
def category_theory.monoidal.functor_category_braided {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] [category_theory.braided_category D] :
category_theory.braided_category (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.

Equations
source
@[protected, instance]
def category_theory.monoidal.functor_category_symmetric {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] [category_theory.monoidal_category D] [category_theory.symmetric_category D] :
category_theory.symmetric_category (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.

Equations