whiskerLeft_rightUnitor_inv — Mathlib

English

The inverse right unitor whiskered on the left equals the composition of the right unitor inverse on X ⊗ Y and the associator inverse, illustrating coherence.

Русский

Обратный правый унитор, взятый слева, равен композиции обратного правого унитора на X ⊗ Y и обратной ассоциаторной инверсии.

LaTeX

$$$X \\;◁ (\\rho_Y)^{-1} = (\\rho_{X \\otimes Y})^{-1} \\circ α_{X,Y,I}^{-1}$$$

Lean4

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

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