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
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] :
(An auxiliary definition for functor_category_monoidal.)
Tensor product of functors C ⥤ D, when D is monoidal.
@[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) :
@[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) :
@[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) :
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
- category_theory.monoidal.functor_category.tensor_hom α β = {app := λ (X : C), α.app X ⊗ β.app X, naturality' := _}
@[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] :
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
- category_theory.monoidal.functor_category_monoidal = {tensor_obj := λ (F G : C ⥤ D), category_theory.monoidal.functor_category.tensor_obj F G, tensor_hom := λ (F G F' G' : C ⥤ D) (α : F ⟶ G) (β : F' ⟶ G'), category_theory.monoidal.functor_category.tensor_hom α β, tensor_id' := _, tensor_comp' := _, tensor_unit := (category_theory.functor.const C).obj (𝟙_ D), associator := λ (F G H : C ⥤ D), category_theory.nat_iso.of_components (λ (X : C), α_ (F.obj X) (G.obj X) (H.obj X)) _, associator_naturality' := _, left_unitor := λ (F : C ⥤ D), category_theory.nat_iso.of_components (λ (X : C), λ_ (F.obj X)) _, left_unitor_naturality' := _, right_unitor := λ (F : C ⥤ D), category_theory.nat_iso.of_components (λ (X : C), ρ_ (F.obj X)) _, right_unitor_naturality' := _, pentagon' := _, triangle' := _}
@[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} :
@[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} :
@[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} :
@[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} :
@[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} :
@[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} :
@[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} :
@[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} :
@[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} :
@[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} :
@[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} :