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

CategoryTheory.Pi.symmetricCategory = { toBraidedCategory := CategoryTheory.Pi.braidedCategory, symmetry := ⋯ }

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_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

@[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

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

CategoryTheory.Pi.closedUnit X = { app := fun (Y : (i : I) → C i) (i : I) => (CategoryTheory.ihom.coev (X i)).app (Y i), naturality := ⋯ }

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

CategoryTheory.Pi.closedCounit X = { app := fun (Y : (i : I) → C i) (i : I) => (CategoryTheory.ihom.ev (X i)).app (Y i), naturality := ⋯ }

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_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_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_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

source

instance CategoryTheory.Pi.instMonoidalForallEval {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] (i : I) :

(eval C i).Monoidal

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem CategoryTheory.Pi.ε_def {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] (i : I) :

Functor.LaxMonoidal.ε (eval C i) = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit (C i))

source

@[simp]

theorem CategoryTheory.Pi.δ_def {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] (i : I) (X Y : (i : I) → C i) :

Functor.OplaxMonoidal.δ (eval C i) X Y = CategoryStruct.id (MonoidalCategoryStruct.tensorObj (X i) (Y i))

source

@[simp]

theorem CategoryTheory.Pi.η_def {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] (i : I) :

Functor.OplaxMonoidal.η (eval C i) = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit (C i))

source

@[simp]

theorem CategoryTheory.Pi.μ_def {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] (i : I) (X Y : (i : I) → C i) :

Functor.LaxMonoidal.μ (eval C i) X Y = CategoryStruct.id (MonoidalCategoryStruct.tensorObj (X i) (Y i))

source

instance CategoryTheory.Pi.instBraidedForallEval {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] [(i : I) → BraidedCategory (C i)] (i : I) :

(eval C i).Braided

Equations

CategoryTheory.Pi.instBraidedForallEval i = { toMonoidal := CategoryTheory.Pi.instMonoidalForallEval i, braided := ⋯ }

source

instance CategoryTheory.Pi.laxMonoidalPi' {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {D : Type u_1} [Category.{v_1, u_1} D] [MonoidalCategory D] (F : (i : I) → Functor D (C i)) [(i : I) → (F i).LaxMonoidal] :

(Functor.pi' F).LaxMonoidal

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem CategoryTheory.Pi.laxMonoidalPi'_μ {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {D : Type u_1} [Category.{v_1, u_1} D] [MonoidalCategory D] (F : (i : I) → Functor D (C i)) [(i : I) → (F i).LaxMonoidal] (X Y : D) (i : I) :

Functor.LaxMonoidal.μ (Functor.pi' F) X Y i = Functor.LaxMonoidal.μ (F i) X Y

source

@[simp]

theorem CategoryTheory.Pi.laxMonoidalPi'_ε {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {D : Type u_1} [Category.{v_1, u_1} D] [MonoidalCategory D] (F : (i : I) → Functor D (C i)) [(i : I) → (F i).LaxMonoidal] (i : I) :

Functor.LaxMonoidal.ε (Functor.pi' F) i = Functor.LaxMonoidal.ε (F i)

source

instance CategoryTheory.Pi.opLaxMonoidalPi' {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {D : Type u_1} [Category.{v_1, u_1} D] [MonoidalCategory D] (F : (i : I) → Functor D (C i)) [(i : I) → (F i).OplaxMonoidal] :

(Functor.pi' F).OplaxMonoidal

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem CategoryTheory.Pi.opLaxMonoidalPi'_η {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {D : Type u_1} [Category.{v_1, u_1} D] [MonoidalCategory D] (F : (i : I) → Functor D (C i)) [(i : I) → (F i).OplaxMonoidal] (i : I) :

Functor.OplaxMonoidal.η (Functor.pi' F) i = Functor.OplaxMonoidal.η (F i)

source

@[simp]

theorem CategoryTheory.Pi.opLaxMonoidalPi'_δ {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {D : Type u_1} [Category.{v_1, u_1} D] [MonoidalCategory D] (F : (i : I) → Functor D (C i)) [(i : I) → (F i).OplaxMonoidal] (X Y : D) (i : I) :

Functor.OplaxMonoidal.δ (Functor.pi' F) X Y i = Functor.OplaxMonoidal.δ (F i) X Y

source

instance CategoryTheory.Pi.monoidalPi' {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {D : Type u_1} [Category.{v_1, u_1} D] [MonoidalCategory D] (F : (i : I) → Functor D (C i)) [(i : I) → (F i).Monoidal] :

(Functor.pi' F).Monoidal

Equations

CategoryTheory.Pi.monoidalPi' F = { toLaxMonoidal := CategoryTheory.Pi.laxMonoidalPi' F, toOplaxMonoidal := CategoryTheory.Pi.opLaxMonoidalPi' F, ε_η := ⋯, η_ε := ⋯, μ_δ := ⋯, δ_μ := ⋯ }

source

@[simp]

theorem CategoryTheory.Pi.monoidalPi'_ε {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {D : Type u_1} [Category.{v_1, u_1} D] [MonoidalCategory D] (F : (i : I) → Functor D (C i)) [(i : I) → (F i).Monoidal] (i : I) :

Functor.LaxMonoidal.ε (Functor.pi' F) i = Functor.LaxMonoidal.ε (F i)

source

@[simp]

theorem CategoryTheory.Pi.monoidalPi'_δ {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {D : Type u_1} [Category.{v_1, u_1} D] [MonoidalCategory D] (F : (i : I) → Functor D (C i)) [(i : I) → (F i).Monoidal] (X Y : D) (i : I) :

Functor.OplaxMonoidal.δ (Functor.pi' F) X Y i = Functor.OplaxMonoidal.δ (F i) X Y

source

@[simp]

theorem CategoryTheory.Pi.monoidalPi'_μ {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {D : Type u_1} [Category.{v_1, u_1} D] [MonoidalCategory D] (F : (i : I) → Functor D (C i)) [(i : I) → (F i).Monoidal] (X Y : D) (i : I) :

Functor.LaxMonoidal.μ (Functor.pi' F) X Y i = Functor.LaxMonoidal.μ (F i) X Y

source

@[simp]

theorem CategoryTheory.Pi.monoidalPi'_η {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {D : Type u_1} [Category.{v_1, u_1} D] [MonoidalCategory D] (F : (i : I) → Functor D (C i)) [(i : I) → (F i).Monoidal] (i : I) :

Functor.OplaxMonoidal.η (Functor.pi' F) i = Functor.OplaxMonoidal.η (F i)

source

instance CategoryTheory.Pi.instLaxBraidedForallPi' {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] [(i : I) → BraidedCategory (C i)] {D : Type u_1} [Category.{v_1, u_1} D] [MonoidalCategory D] [BraidedCategory D] (F : (i : I) → Functor D (C i)) [(i : I) → (F i).LaxBraided] :

(Functor.pi' F).LaxBraided

Equations

CategoryTheory.Pi.instLaxBraidedForallPi' F = { toLaxMonoidal := CategoryTheory.Pi.laxMonoidalPi' F, braided := ⋯ }

source

instance CategoryTheory.Pi.instBraidedForallPi' {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] [(i : I) → BraidedCategory (C i)] {D : Type u_1} [Category.{v_1, u_1} D] [MonoidalCategory D] [BraidedCategory D] (F : (i : I) → Functor D (C i)) [(i : I) → (F i).Braided] :

(Functor.pi' F).Braided

Equations

CategoryTheory.Pi.instBraidedForallPi' F = { toMonoidal := CategoryTheory.Pi.monoidalPi' F, braided := ⋯ }

source

instance CategoryTheory.Pi.laxMonoidalPi {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] [(i : I) → MonoidalCategory (D i)] (F : (i : I) → Functor (D i) (C i)) [(i : I) → (F i).LaxMonoidal] :

(Functor.pi F).LaxMonoidal

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem CategoryTheory.Pi.laxMonoidalPi_μ {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] [(i : I) → MonoidalCategory (D i)] (F : (i : I) → Functor (D i) (C i)) [(i : I) → (F i).LaxMonoidal] (X Y : (i : I) → D i) (i : I) :

Functor.LaxMonoidal.μ (Functor.pi F) X Y i = Functor.LaxMonoidal.μ (F i) (X i) (Y i)

source

@[simp]

theorem CategoryTheory.Pi.laxMonoidalPi_ε {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] [(i : I) → MonoidalCategory (D i)] (F : (i : I) → Functor (D i) (C i)) [(i : I) → (F i).LaxMonoidal] (i : I) :

Functor.LaxMonoidal.ε (Functor.pi F) i = Functor.LaxMonoidal.ε (F i)

source

instance CategoryTheory.Pi.opLaxMonoidalPi {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] [(i : I) → MonoidalCategory (D i)] (F : (i : I) → Functor (D i) (C i)) [(i : I) → (F i).OplaxMonoidal] :

(Functor.pi F).OplaxMonoidal

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem CategoryTheory.Pi.opLaxMonoidalPi_η {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] [(i : I) → MonoidalCategory (D i)] (F : (i : I) → Functor (D i) (C i)) [(i : I) → (F i).OplaxMonoidal] (i : I) :

Functor.OplaxMonoidal.η (Functor.pi F) i = Functor.OplaxMonoidal.η (F i)

source

@[simp]

theorem CategoryTheory.Pi.opLaxMonoidalPi_δ {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] [(i : I) → MonoidalCategory (D i)] (F : (i : I) → Functor (D i) (C i)) [(i : I) → (F i).OplaxMonoidal] (X Y : (i : I) → D i) (i : I) :

Functor.OplaxMonoidal.δ (Functor.pi F) X Y i = Functor.OplaxMonoidal.δ (F i) (X i) (Y i)

source

instance CategoryTheory.Pi.monoidalPi {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] [(i : I) → MonoidalCategory (D i)] (F : (i : I) → Functor (D i) (C i)) [(i : I) → (F i).Monoidal] :

(Functor.pi F).Monoidal

Equations

CategoryTheory.Pi.monoidalPi F = { toLaxMonoidal := CategoryTheory.Pi.laxMonoidalPi F, toOplaxMonoidal := CategoryTheory.Pi.opLaxMonoidalPi F, ε_η := ⋯, η_ε := ⋯, μ_δ := ⋯, δ_μ := ⋯ }

source

@[simp]

theorem CategoryTheory.Pi.monoidalPi_η {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] [(i : I) → MonoidalCategory (D i)] (F : (i : I) → Functor (D i) (C i)) [(i : I) → (F i).Monoidal] (i : I) :

Functor.OplaxMonoidal.η (Functor.pi F) i = Functor.OplaxMonoidal.η (F i)

source

@[simp]

theorem CategoryTheory.Pi.monoidalPi_δ {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] [(i : I) → MonoidalCategory (D i)] (F : (i : I) → Functor (D i) (C i)) [(i : I) → (F i).Monoidal] (X Y : (i : I) → D i) (i : I) :

Functor.OplaxMonoidal.δ (Functor.pi F) X Y i = Functor.OplaxMonoidal.δ (F i) (X i) (Y i)

source

@[simp]

theorem CategoryTheory.Pi.monoidalPi_ε {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] [(i : I) → MonoidalCategory (D i)] (F : (i : I) → Functor (D i) (C i)) [(i : I) → (F i).Monoidal] (i : I) :

Functor.LaxMonoidal.ε (Functor.pi F) i = Functor.LaxMonoidal.ε (F i)

source

@[simp]

theorem CategoryTheory.Pi.monoidalPi_μ {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] [(i : I) → MonoidalCategory (D i)] (F : (i : I) → Functor (D i) (C i)) [(i : I) → (F i).Monoidal] (X Y : (i : I) → D i) (i : I) :

Functor.LaxMonoidal.μ (Functor.pi F) X Y i = Functor.LaxMonoidal.μ (F i) (X i) (Y i)

source

instance CategoryTheory.Pi.instLaxBraidedForallPi {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] [(i : I) → BraidedCategory (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] [(i : I) → MonoidalCategory (D i)] [(i : I) → BraidedCategory (D i)] (F : (i : I) → Functor (D i) (C i)) [(i : I) → (F i).LaxBraided] :

(Functor.pi F).LaxBraided

Equations

CategoryTheory.Pi.instLaxBraidedForallPi F = { toLaxMonoidal := CategoryTheory.Pi.laxMonoidalPi F, braided := ⋯ }

source

instance CategoryTheory.Pi.instBraidedForallPi {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] [(i : I) → BraidedCategory (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] [(i : I) → MonoidalCategory (D i)] [(i : I) → BraidedCategory (D i)] (F : (i : I) → Functor (D i) (C i)) [(i : I) → (F i).Braided] :

(Functor.pi F).Braided

Equations

CategoryTheory.Pi.instBraidedForallPi F = { toMonoidal := CategoryTheory.Pi.monoidalPi F, braided := ⋯ }

source

instance CategoryTheory.Pi.instIsMonoidalForallPi' {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {D : Type u_1} [Category.{v_1, u_1} D] [MonoidalCategory D] {F G : Functor D ((i : I) → C i)} [F.LaxMonoidal] [G.LaxMonoidal] (τ : (i : I) → F.comp (eval C i) ⟶ G.comp (eval C i)) [∀ (i : I), NatTrans.IsMonoidal (τ i)] :

NatTrans.IsMonoidal (NatTrans.pi' τ)

source

instance CategoryTheory.Pi.instIsMonoidalForallPi {I : Type w₁} {C : I → Type u₁} [(i : I) → Category.{v₁, u₁} (C i)] [(i : I) → MonoidalCategory (C i)] {D : I → Type u₂} [(i : I) → Category.{v₂, u₂} (D i)] [(i : I) → MonoidalCategory (D i)] {F G : (i : I) → Functor (D i) (C i)} [(i : I) → (F i).LaxMonoidal] [(i : I) → (G i).LaxMonoidal] (τ : (i : I) → F i ⟶ G i) [∀ (i : I), NatTrans.IsMonoidal (τ i)] :

NatTrans.IsMonoidal (NatTrans.pi τ)

Documentation

Mathlib.CategoryTheory.Pi.Monoidal

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