English
The tensor product in a braided monoidal category satisfies the pentagon-like coherence condition relating the tensor μ and the associator, ensuring coherence when grouping multiple tensors.
Русский
Умножение тензора в braided-монодной категории удовлетворяет когерентному условию, аналогичному пятиугольнику, связывающему μ и ассоциатором.
LaTeX
$$$\; (\,tensorμ_{X_1,X_2,Y_1,Y_2} \; \mathrm{whisker} \; (Z_1 \otimes Z_2)) \; \gg\; tensorμ_{X_1\otimes Y_1,X_2\otimes Y_2,Z_1,Z_2} \; \gg\; ((α_{X_1,Y_1,Z_1}.\mathrm{hom} \otimes_m α_{X_2,Y_2,Z_2}.\mathrm{hom})) = (α_{(X_1⊗X_2)(Y_1⊗Y_2)(Z_1⊗Z_2)} }.\mathrm{hom} \gg\; ((X_1⊗X_2) \triangleleft tensorμ_{Y_1,Y_2,Z_1,Z_2}) \gg\; tensorμ_{X_1,X_2,(Y_1⊗Z_1),(Y_2⊗Z_2)}.$$$
Lean4
@[reassoc]
theorem tensor_associativity (X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C) :
(tensorμ X₁ X₂ Y₁ Y₂ ▷ (Z₁ ⊗ Z₂)) ≫ tensorμ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) Z₁ Z₂ ≫ ((α_ X₁ Y₁ Z₁).hom ⊗ₘ (α_ X₂ Y₂ Z₂).hom) =
(α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (Z₁ ⊗ Z₂)).hom ≫ ((X₁ ⊗ X₂) ◁ tensorμ Y₁ Y₂ Z₁ Z₂) ≫ tensorμ X₁ X₂ (Y₁ ⊗ Z₁) (Y₂ ⊗ Z₂) :=
by
dsimp only [tensor_obj, prodMonoidal_tensorObj, tensorμ]
simp only [braiding_tensor_left_hom, braiding_tensor_right_hom]
calc
_ =
𝟙 _ ⊗≫
X₁ ◁ ((β_ X₂ Y₁).hom ▷ (Y₂ ⊗ Z₁) ≫ (Y₁ ⊗ X₂) ◁ (β_ Y₂ Z₁).hom) ▷ Z₂ ⊗≫
X₁ ◁ Y₁ ◁ (β_ X₂ Z₁).hom ▷ Y₂ ▷ Z₂ ⊗≫ 𝟙 _ :=
by monoidal
_ = _ := by rw [← whisker_exchange]; monoidal
