Documentation

Mathlib.CategoryTheory.Monoidal.FunctorCategory

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.

source
@[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)
source
@[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)
source
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) :
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
    source
    @[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)
    source
    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') :
    CategoryTheory.Monoidal.FunctorCategory.tensorObj F F' ⟶ CategoryTheory.Monoidal.FunctorCategory.tensorObj G G'

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

    Equations
    Instances For
      source
      @[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)
      source
      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') :
      CategoryTheory.Monoidal.FunctorCategory.tensorObj F F' ⟶ CategoryTheory.Monoidal.FunctorCategory.tensorObj F G'

      (An auxiliary definition for functorCategoryMonoidal.)

      Equations
      Instances For
        source
        @[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)
        source
        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) :
        CategoryTheory.Monoidal.FunctorCategory.tensorObj F F' ⟶ CategoryTheory.Monoidal.FunctorCategory.tensorObj G F'

        (An auxiliary definition for functorCategoryMonoidal.)

        Equations
        Instances For
          source
          instance CategoryTheory.Monoidal.functorCategoryMonoidalStruct {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] :
          CategoryTheory.MonoidalCategoryStruct (CategoryTheory.Functor 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
          • One or more equations did not get rendered due to their size.
          source
          @[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
          source
          @[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)
          source
          @[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)
          source
          @[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)
          source
          @[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)
          source
          @[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)
          source
          @[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)
          source
          @[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
          source
          @[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
          source
          @[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
          source
          @[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
          source
          @[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
          source
          @[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
          source
          instance CategoryTheory.Monoidal.functorCategoryMonoidal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] :
          CategoryTheory.MonoidalCategory (CategoryTheory.Functor 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
          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] :
          CategoryTheory.BraidedCategory (CategoryTheory.Functor 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
          • One or more equations did not get rendered due to their size.
          source
          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] :
          CategoryTheory.SymmetricCategory (CategoryTheory.Functor 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