English
Let C1 and C2 be monoidal categories. Then their Cartesian product C1 × C2 can be endowed with a monoidal structure defined componentwise: the tensor of (X1, X2) and (Y1, Y2) is (X1 ⊗ Y1, X2 ⊗ Y2), morphisms are paired accordingly, and the associator, unitors, and their inverses are defined componentwise using the corresponding data in C1 and C2.
Русский
Пусть C1 и C2 — моноидальные категории. Их декартово произведение C1 × C2 можно наделить моноидальной структурой по компонентам: тензор пары (X1, X2) и (Y1, Y2) равен (X1 ⊗ Y1, X2 ⊗ Y2), морфизмы задаются попарно, а ассоциатор и униторы добавляются по компонентам равенств соответствующих категорий.
LaTeX
$$$\\text{MonoidalCategory}(C_1 \\times C_2)\\quad\\text{with}\\quad \\otimes((X_1,X_2),(Y_1,Y_2))=(X_1\\otimes Y_1, X_2\\otimes Y_2),\\; I=(I_1,I_2),\\; (f,g)\\otimes(h,k)=(f\\otimes h, g\\otimes k),\\;\\alpha_{(X_1,X_2),(Y_1,Y_2),(Z_1,Z_2)}=(\\alpha^{C_1}_{X_1,Y_1,Z_1},\\alpha^{C_2}_{X_2,Y_2,Z_2}),\\;\\text{etc.}$$$
Lean4
@[simps! tensorObj tensorHom tensorUnit whiskerLeft whiskerRight associator]
instance prodMonoidal : MonoidalCategory (C₁ × C₂)
where
tensorObj X Y := (X.1 ⊗ Y.1, X.2 ⊗ Y.2)
tensorHom f g := (f.1 ⊗ₘ g.1, f.2 ⊗ₘ g.2)
whiskerLeft X _ _ f := (whiskerLeft X.1 f.1, whiskerLeft X.2 f.2)
whiskerRight f X := (whiskerRight f.1 X.1, whiskerRight f.2 X.2)
tensorHom_def := by simp [tensorHom_def]
tensorUnit := (𝟙_ C₁, 𝟙_ C₂)
associator X Y Z := (α_ X.1 Y.1 Z.1).prod (α_ X.2 Y.2 Z.2)
leftUnitor := fun ⟨X₁, X₂⟩ => (λ_ X₁).prod (λ_ X₂)
rightUnitor := fun ⟨X₁, X₂⟩ => (ρ_ X₁).prod (ρ_ X₂)
