English
The right unitor interacts with tensor μ in a symmetric, coherent manner with the associator, ensuring compatibility of right unitality with tensoring two objects.
Русский
Правый унитор согласован с μ и ассоциатором, обеспечивая совместимость правая еденица с тензорированием двух объектов.
LaTeX
$$$$ (\rho_X).\mathrm{hom} ⊗_m (\rho_Y).\mathrm{hom} = tensorμ X (\mathbb{1}_C) X_2 (\mathbb{1}_C) ≫ ((X ⊗ X_2) ◁ (λ_{\mathbb{1}_C}).hom) ≫ (\rho_{(X ⊗ X_2)}).hom. $$$$
Lean4
@[reassoc]
theorem associator_monoidal (X₁ X₂ X₃ Y₁ Y₂ Y₃ : C) :
tensorμ (X₁ ⊗ X₂) X₃ (Y₁ ⊗ Y₂) Y₃ ≫ (tensorμ X₁ X₂ Y₁ Y₂ ▷ (X₃ ⊗ Y₃)) ≫ (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (X₃ ⊗ Y₃)).hom =
((α_ X₁ X₂ X₃).hom ⊗ₘ (α_ Y₁ Y₂ Y₃).hom) ≫
tensorμ X₁ (X₂ ⊗ X₃) Y₁ (Y₂ ⊗ Y₃) ≫ ((X₁ ⊗ Y₁) ◁ tensorμ X₂ X₃ Y₂ Y₃) :=
by
dsimp only [tensorμ]
calc
_ =
𝟙 _ ⊗≫
X₁ ◁ X₂ ◁ (β_ X₃ Y₁).hom ▷ Y₂ ▷ Y₃ ⊗≫
X₁ ◁ ((X₂ ⊗ Y₁) ◁ (β_ X₃ Y₂).hom ≫ (β_ X₂ Y₁).hom ▷ (Y₂ ⊗ X₃)) ▷ Y₃ ⊗≫ 𝟙 _ :=
by rw [braiding_tensor_right_hom]; monoidal
_ = _ := by rw [whisker_exchange, braiding_tensor_left_hom]; monoidal
