English
In a braided monoidal category, for any X1, X2, there is a coherence identity expressing the right unitor on X1 ⊗ X2 in terms of the left whisker, the tensor associator, and the right unitors of X1 and X2.
Русский
В braided-мономодульной категории существует когерентное тождество для правого унитора на X1 ⊗ X2, выражающее его через левый отодвигатель, ассоциатор тензора и правые униторы X1 и X2.
LaTeX
$$$(\rho_{X_1\otimes X_2}).\mathrm{hom} = ((X_1\otimes X_2) \Triangleleft (\lambda_{\mathbb{1}_C})^{-1}) \circ \mathrm{tensorμ}_{X_1,X_2,\mathbb{1}_C,\mathbb{1}_C} \circ (\rho_{X_1}.\mathrm{hom} \otimes_{\mathsf{m}} \rho_{X_2}.\mathrm{hom}).$$$
Lean4
@[reassoc]
theorem tensor_right_unitality (X₁ X₂ : C) :
(ρ_ (X₁ ⊗ X₂)).hom = ((X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).inv) ≫ tensorμ X₁ X₂ (𝟙_ C) (𝟙_ C) ≫ ((ρ_ X₁).hom ⊗ₘ (ρ_ X₂).hom) :=
by
dsimp only [tensorμ]
have :
((X₁ ⊗ X₂) ◁ (λ_ (𝟙_ C)).inv) ≫ (α_ X₁ X₂ (𝟙_ C ⊗ 𝟙_ C)).hom ≫ (X₁ ◁ (α_ X₂ (𝟙_ C) (𝟙_ C)).inv) =
(α_ X₁ X₂ (𝟙_ C)).hom ≫ (X₁ ◁ (ρ_ X₂).inv ▷ 𝟙_ C) :=
by monoidal
slice_rhs 1 3 => rw [this]
clear this
slice_rhs 2 3 => rw [← whiskerLeft_comp, ← comp_whiskerRight, rightUnitor_inv_braiding]
simp [tensorHom_def]
