English
The left unitor interacts with tensor μ in a specific way, giving a coherence relation between the left unitor on a unit and the tensor product of two objects.
Русский
Левый унитор взаимодействует с μ через когерентное равенство, связывающее левый унитор единицы и тензор двух объектов.
LaTeX
$$$$ (\lambda_X).\mathrm{hom} \otimes_m (\lambda_Y).\mathrm{hom} = tensorμ (\mathbb{1}_C) X_1 (\mathbb{1}_C) X_2 ≫ ((\lambda_{\mathbb{1}_C}).hom ▷ (X_1 ⊗ X_2)) ≫ (\lambda_{(X_1 ⊗ X_2)}).hom. $$$$
Lean4
@[reassoc]
theorem rightUnitor_monoidal (X₁ X₂ : C) :
(ρ_ X₁).hom ⊗ₘ (ρ_ X₂).hom = tensorμ X₁ (𝟙_ C) X₂ (𝟙_ C) ≫ ((X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).hom) ≫ (ρ_ (X₁ ⊗ X₂)).hom :=
by
dsimp only [tensorμ]
have :
(ρ_ X₁).hom ⊗ₘ (ρ_ X₂).hom =
(α_ X₁ (𝟙_ C) (X₂ ⊗ 𝟙_ C)).hom ≫
(X₁ ◁ (α_ (𝟙_ C) X₂ (𝟙_ C)).inv) ≫ (X₁ ◁ (ρ_ (𝟙_ C ⊗ X₂)).hom) ≫ (X₁ ◁ (λ_ X₂).hom) :=
by monoidal
rw [this]; clear this
rw [← braiding_rightUnitor]
monoidal
