Documentation

Mathlib.CategoryTheory.Pi.Monoidal

The pointwise monoidal structure on the product of families of monoidal categories #

Given a family of monoidal categories C i, we define a monoidal structure on Π i, C i where the tensor product is defined pointwise.

source
instance CategoryTheory.Pi.monoidalCategoryStruct {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] :
MonoidalCategoryStruct ((i : I) → C i)
Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.Pi.monoidalCategoryStruct_tensorObj {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] (X Y : (i : I) → C i) (i : I) :
MonoidalCategoryStruct.tensorObj X Y i = MonoidalCategoryStruct.tensorObj (X i) (Y i)
source
@[simp]
theorem CategoryTheory.Pi.monoidalCategoryStruct_tensorHom {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {X₁✝ Y₁✝ X₂✝ Y₂✝ : (i : I) → C i} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) (i : I) :
MonoidalCategoryStruct.tensorHom f g i = MonoidalCategoryStruct.tensorHom (f i) (g i)
source
@[simp]
theorem CategoryTheory.Pi.monoidalCategoryStruct_whiskerLeft {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] (X x✝ x✝¹ : (i : I) → C i) (f : x✝ ⟶ x✝¹) (i : I) :
MonoidalCategoryStruct.whiskerLeft X f i = MonoidalCategoryStruct.whiskerLeft (X i) (f i)
source
@[simp]
theorem CategoryTheory.Pi.monoidalCategoryStruct_tensorUnit {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] (i : I) :
MonoidalCategoryStruct.tensorUnit ((i : I) → C i) i = MonoidalCategoryStruct.tensorUnit (C i)
source
@[simp]
theorem CategoryTheory.Pi.monoidalCategoryStruct_whiskerRight {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {X₁✝ X₂✝ : (i : I) → C i} (f : X₁✝ ⟶ X₂✝) (Y : (i : I) → C i) (i : I) :
MonoidalCategoryStruct.whiskerRight f Y i = MonoidalCategoryStruct.whiskerRight (f i) (Y i)
source
@[simp]
theorem CategoryTheory.Pi.associator_hom_apply {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {X Y Z : (i : I) → C i} {i : I} :
(MonoidalCategoryStruct.associator X Y Z).hom i = (MonoidalCategoryStruct.associator (X i) (Y i) (Z i)).hom
source
@[simp]
theorem CategoryTheory.Pi.associator_inv_apply {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {X Y Z : (i : I) → C i} {i : I} :
(MonoidalCategoryStruct.associator X Y Z).inv i = (MonoidalCategoryStruct.associator (X i) (Y i) (Z i)).inv
source
@[simp]
theorem CategoryTheory.Pi.isoApp_associator {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {X Y Z : (i : I) → C i} {i : I} :
isoApp (MonoidalCategoryStruct.associator X Y Z) i = MonoidalCategoryStruct.associator (X i) (Y i) (Z i)
source
@[simp]
theorem CategoryTheory.Pi.left_unitor_hom_apply {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {X : (i : I) → C i} {i : I} :
(MonoidalCategoryStruct.leftUnitor X).hom i = (MonoidalCategoryStruct.leftUnitor (X i)).hom
source
@[simp]
theorem CategoryTheory.Pi.left_unitor_inv_apply {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {X : (i : I) → C i} {i : I} :
(MonoidalCategoryStruct.leftUnitor X).inv i = (MonoidalCategoryStruct.leftUnitor (X i)).inv
source
@[simp]
theorem CategoryTheory.Pi.isoApp_left_unitor {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {X : (i : I) → C i} {i : I} :
isoApp (MonoidalCategoryStruct.leftUnitor X) i = MonoidalCategoryStruct.leftUnitor (X i)
source
@[simp]
theorem CategoryTheory.Pi.right_unitor_hom_apply {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {X : (i : I) → C i} {i : I} :
(MonoidalCategoryStruct.rightUnitor X).hom i = (MonoidalCategoryStruct.rightUnitor (X i)).hom
source
@[simp]
theorem CategoryTheory.Pi.right_unitor_inv_apply {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {X : (i : I) → C i} {i : I} :
(MonoidalCategoryStruct.rightUnitor X).inv i = (MonoidalCategoryStruct.rightUnitor (X i)).inv
source
@[simp]
theorem CategoryTheory.Pi.isoApp_right_unitor {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {X : (i : I) → C i} {i : I} :
isoApp (MonoidalCategoryStruct.rightUnitor X) i = MonoidalCategoryStruct.rightUnitor (X i)
source
instance CategoryTheory.Pi.monoidalCategory {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] :
MonoidalCategory ((i : I) → C i)

Pi.monoidalCategory C equips the product of an indexed family of categories with the pointwise monoidal structure.

Equations
  • One or more equations did not get rendered due to their size.
source
instance CategoryTheory.Pi.braidedCategory {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] [(i : I) → BraidedCategory (C i)] :
BraidedCategory ((i : I) → C i)

When each C i is a braided monoidal category, the natural pointwise monoidal structure on ∀ i, C i is also braided.

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.Pi.braiding_hom_apply {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] [(i : I) → BraidedCategory (C i)] {X Y : (i : I) → C i} {i : I} :
(β_ X Y).hom i = (β_ (X i) (Y i)).hom
source
@[simp]
theorem CategoryTheory.Pi.braiding_inv_apply {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] [(i : I) → BraidedCategory (C i)] {X Y : (i : I) → C i} {i : I} :
(β_ X Y).inv i = (β_ (X i) (Y i)).inv
source
@[simp]
theorem CategoryTheory.Pi.isoApp_braiding {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] [(i : I) → BraidedCategory (C i)] {X Y : (i : I) → C i} {i : I} :
isoApp (β_ X Y) i = β_ (X i) (Y i)
source
instance CategoryTheory.Pi.symmetricCategory {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] [(i : I) → SymmetricCategory (C i)] :
SymmetricCategory ((i : I) → C i)

When each C i is a symmetric monoidal category, the natural pointwise monoidal structure on ∀ i, C i is also symmetric.

Equations
source
def CategoryTheory.Pi.ihom {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] [(i : I) → MonoidalClosed (C i)] (X : (i : I) → C i) :
Functor ((i : I) → C i) ((i : I) → C i)

The internal hom functor X ⟶[∀ i, C i] -

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Pi.ihom_map {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] [(i : I) → MonoidalClosed (C i)] (X : (i : I) → C i) {Y Z : (i : I) → C i} (f : Y ⟶ Z) (i : I) :
    (ihom X).map f i = (CategoryTheory.ihom (X i)).map (f i)
    source
    @[simp]
    theorem CategoryTheory.Pi.ihom_obj {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] [(i : I) → MonoidalClosed (C i)] (X Y : (i : I) → C i) (i : I) :
    (ihom X).obj Y i = (CategoryTheory.ihom (X i)).obj (Y i)
    source
    def CategoryTheory.Pi.closedUnit {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] [(i : I) → MonoidalClosed (C i)] (X : (i : I) → C i) :
    Functor.id ((i : I) → C i) ⟶ (MonoidalCategory.tensorLeft X).comp (ihom X)

    The unit for the adjunction tensorLeft X ⊣ ihom X.

    Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Pi.closedUnit_app {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] [(i : I) → MonoidalClosed (C i)] (X Y : (i : I) → C i) (i : I) :
      (closedUnit X).app Y i = (ihom.coev (X i)).app (Y i)
      source
      def CategoryTheory.Pi.closedCounit {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] [(i : I) → MonoidalClosed (C i)] (X : (i : I) → C i) :
      (ihom X).comp (MonoidalCategory.tensorLeft X) ⟶ Functor.id ((i : I) → C i)

      The counit for the adjunction tensorLeft X ⊣ ihom X.

      Equations
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Pi.closedCounit_app {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] [(i : I) → MonoidalClosed (C i)] (X Y : (i : I) → C i) (i : I) :
        (closedCounit X).app Y i = (ihom.ev (X i)).app (Y i)
        source
        instance CategoryTheory.Pi.monoidalClosed {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] [(i : I) → MonoidalClosed (C i)] :
        MonoidalClosed ((i : I) → C i)

        equipps the product of a family of closed monoidal categories with a pointwise closed monoidal structure.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[simp]
        theorem CategoryTheory.Pi.monoidalClosed_closed_rightAdj {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] [(i : I) → MonoidalClosed (C i)] (X : (i : I) → C i) :
        Closed.rightAdj X = ihom X
        source
        @[simp]
        theorem CategoryTheory.Pi.monoidalClosed_closed_adj_counit {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] [(i : I) → MonoidalClosed (C i)] (X : (i : I) → C i) :
        Closed.adj.counit = closedCounit X
        source
        @[simp]
        theorem CategoryTheory.Pi.monoidalClosed_closed_adj_unit {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] [(i : I) → MonoidalClosed (C i)] (X : (i : I) → C i) :
        Closed.adj.unit = closedUnit X