rightUnitor_tensor_inv — Mathlib

English

In a monoidal category, the right unitor of a tensor product X ⊗ Y has its inverse equal to the composite X ⊳ (ρ_Y)^{-1} ≫ (α_{X,Y,I})^{-1}.

Русский

В монойдальной категории обратный правого унитора тензорного произведения X ⊗ Y равен композиции X ⊳ (ρ_Y)^{-1} затем (α_{X,Y,I})^{-1}.

LaTeX

$$$ (\rho_{X\otimes Y})^{-1} = X \triangleleft (\rho_Y)^{-1} \;\circ\; (\alpha_{X,Y,\mathbb{1}})^{-1}$$$

Lean4

@[reassoc]
theorem rightUnitor_tensor_inv (X Y : C) : (ρ_ (X ⊗ Y)).inv = X ◁ (ρ_ Y).inv ≫ (α_ X Y (𝟙_ C)).inv := by simp

Похожие утверждения