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.
@[simp]
theorem
CategoryTheory.Monoidal.FunctorCategory.tensorObj_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor C D)
:
∀ {X Y : C} (f : X ⟶ Y),
(CategoryTheory.Monoidal.FunctorCategory.tensorObj F G).map f = CategoryTheory.MonoidalCategory.tensorHom (F.map f) (G.map f)
@[simp]
theorem
CategoryTheory.Monoidal.FunctorCategory.tensorObj_obj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor C D)
(X : C)
:
(CategoryTheory.Monoidal.FunctorCategory.tensorObj F G).obj X = CategoryTheory.MonoidalCategory.tensorObj (F.obj X) (G.obj X)
def
CategoryTheory.Monoidal.FunctorCategory.tensorObj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor C D)
:
(An auxiliary definition for functorCategoryMonoidal.)
Tensor product of functors C ⥤ D, when D is monoidal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Monoidal.FunctorCategory.tensorHom_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
{F' : CategoryTheory.Functor C D}
{G' : CategoryTheory.Functor C D}
(α : F ⟶ G)
(β : F' ⟶ G')
(X : C)
:
(CategoryTheory.Monoidal.FunctorCategory.tensorHom α β).app X = CategoryTheory.MonoidalCategory.tensorHom (α.app X) (β.app X)
def
CategoryTheory.Monoidal.FunctorCategory.tensorHom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
{F' : CategoryTheory.Functor C D}
{G' : CategoryTheory.Functor C D}
(α : F ⟶ G)
(β : F' ⟶ G')
:
(An auxiliary definition for functorCategoryMonoidal.)
Tensor product of natural transformations into D, when D is monoidal.
Equations
- CategoryTheory.Monoidal.FunctorCategory.tensorHom α β = { app := fun (X : C) => CategoryTheory.MonoidalCategory.tensorHom (α.app X) (β.app X), naturality := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.Monoidal.FunctorCategory.whiskerLeft_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F' : CategoryTheory.Functor C D}
{G' : CategoryTheory.Functor C D}
(F : CategoryTheory.Functor C D)
(β : F' ⟶ G')
(X : C)
:
(CategoryTheory.Monoidal.FunctorCategory.whiskerLeft F β).app X = CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X) (β.app X)
def
CategoryTheory.Monoidal.FunctorCategory.whiskerLeft
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F' : CategoryTheory.Functor C D}
{G' : CategoryTheory.Functor C D}
(F : CategoryTheory.Functor C D)
(β : F' ⟶ G')
:
(An auxiliary definition for functorCategoryMonoidal.)
Equations
- CategoryTheory.Monoidal.FunctorCategory.whiskerLeft F β = { app := fun (X : C) => CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X) (β.app X), naturality := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.Monoidal.FunctorCategory.whiskerRight_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
(α : F ⟶ G)
(F' : CategoryTheory.Functor C D)
(X : C)
:
(CategoryTheory.Monoidal.FunctorCategory.whiskerRight α F').app X = CategoryTheory.MonoidalCategory.whiskerRight (α.app X) (F'.obj X)
def
CategoryTheory.Monoidal.FunctorCategory.whiskerRight
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
(α : F ⟶ G)
(F' : CategoryTheory.Functor C D)
:
(An auxiliary definition for functorCategoryMonoidal.)
Equations
- CategoryTheory.Monoidal.FunctorCategory.whiskerRight α F' = { app := fun (X : C) => CategoryTheory.MonoidalCategory.whiskerRight (α.app X) (F'.obj X), naturality := ⋯ }
Instances For
instance
CategoryTheory.Monoidal.functorCategoryMonoidalStruct
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory 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
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Monoidal.tensorUnit_obj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{X : C}
:
(𝟙_ (CategoryTheory.Functor C D)).obj X = 𝟙_ D
@[simp]
theorem
CategoryTheory.Monoidal.tensorUnit_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{X : C}
{Y : C}
{f : X ⟶ Y}
:
(𝟙_ (CategoryTheory.Functor C D)).map f = CategoryTheory.CategoryStruct.id (𝟙_ D)
@[simp]
theorem
CategoryTheory.Monoidal.tensorObj_obj
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
{X : C}
:
(CategoryTheory.MonoidalCategory.tensorObj F G).obj X = CategoryTheory.MonoidalCategory.tensorObj (F.obj X) (G.obj X)
@[simp]
theorem
CategoryTheory.Monoidal.tensorObj_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
{X : C}
{Y : C}
{f : X ⟶ Y}
:
(CategoryTheory.MonoidalCategory.tensorObj F G).map f = CategoryTheory.MonoidalCategory.tensorHom (F.map f) (G.map f)
@[simp]
theorem
CategoryTheory.Monoidal.tensorHom_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
{F' : CategoryTheory.Functor C D}
{G' : CategoryTheory.Functor C D}
{α : F ⟶ G}
{β : F' ⟶ G'}
{X : C}
:
(CategoryTheory.MonoidalCategory.tensorHom α β).app X = CategoryTheory.MonoidalCategory.tensorHom (α.app X) (β.app X)
@[simp]
theorem
CategoryTheory.Monoidal.whiskerLeft_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F : CategoryTheory.Functor C D}
{F' : CategoryTheory.Functor C D}
{G' : CategoryTheory.Functor C D}
{β : F' ⟶ G'}
{X : C}
:
(CategoryTheory.MonoidalCategory.whiskerLeft F β).app X = CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X) (β.app X)
@[simp]
theorem
CategoryTheory.Monoidal.whiskerRight_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
{F' : CategoryTheory.Functor C D}
{α : F ⟶ G}
{X : C}
:
(CategoryTheory.MonoidalCategory.whiskerRight α F').app X = CategoryTheory.MonoidalCategory.whiskerRight (α.app X) (F'.obj X)
@[simp]
theorem
CategoryTheory.Monoidal.leftUnitor_hom_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F : CategoryTheory.Functor C D}
{X : C}
:
(CategoryTheory.MonoidalCategory.leftUnitor F).hom.app X = (CategoryTheory.MonoidalCategory.leftUnitor (F.obj X)).hom
@[simp]
theorem
CategoryTheory.Monoidal.leftUnitor_inv_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F : CategoryTheory.Functor C D}
{X : C}
:
(CategoryTheory.MonoidalCategory.leftUnitor F).inv.app X = (CategoryTheory.MonoidalCategory.leftUnitor (F.obj X)).inv
@[simp]
theorem
CategoryTheory.Monoidal.rightUnitor_hom_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F : CategoryTheory.Functor C D}
{X : C}
:
(CategoryTheory.MonoidalCategory.rightUnitor F).hom.app X = (CategoryTheory.MonoidalCategory.rightUnitor (F.obj X)).hom
@[simp]
theorem
CategoryTheory.Monoidal.rightUnitor_inv_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F : CategoryTheory.Functor C D}
{X : C}
:
(CategoryTheory.MonoidalCategory.rightUnitor F).inv.app X = (CategoryTheory.MonoidalCategory.rightUnitor (F.obj X)).inv
@[simp]
theorem
CategoryTheory.Monoidal.associator_hom_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
{H : CategoryTheory.Functor C D}
{X : C}
:
(CategoryTheory.MonoidalCategory.associator F G H).hom.app X = (CategoryTheory.MonoidalCategory.associator (F.obj X) (G.obj X) (H.obj X)).hom
@[simp]
theorem
CategoryTheory.Monoidal.associator_inv_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
{H : CategoryTheory.Functor C D}
{X : C}
:
(CategoryTheory.MonoidalCategory.associator F G H).inv.app X = (CategoryTheory.MonoidalCategory.associator (F.obj X) (G.obj X) (H.obj X)).inv
instance
CategoryTheory.Monoidal.functorCategoryMonoidal
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory 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
- CategoryTheory.Monoidal.functorCategoryMonoidal = CategoryTheory.MonoidalCategory.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
instance
CategoryTheory.Monoidal.functorCategoryBraided
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.BraidedCategory 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
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Monoidal.functorCategorySymmetric
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
[CategoryTheory.SymmetricCategory 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
- CategoryTheory.Monoidal.functorCategorySymmetric = CategoryTheory.SymmetricCategory.mk ⋯