braiding_inv_tensorUnit_left — Mathlib

English

The inverse-forward hexagon relation expresses how the inverse of the forward hexagon identity behaves, yielding a dual form of the hexagon in terms of inverses.

Русский

Обратная-прямая гексагональная связь даёт двойственную форму гексагонального тождества через обращения.

LaTeX

$$$$ (\alpha_{Y Z X})^{−1} \circ (β_{X, (Y ⊗ Z)})^{−1} \circ (\alpha_{X Y Z})^{−1} = Y \triangleleft (β_{X Z})^{−1} \circ (\alpha_{Y X Z})^{−1} \circ (β_{X Y})^{−1} \triangleright Z, $$$$

Lean4

@[reassoc, simp]
theorem braiding_inv_tensorUnit_left (X : C) : (β_ (𝟙_ C) X).inv = (ρ_ X).hom ≫ (λ_ X).inv :=
  by
  rw [Iso.inv_ext]
  rw [braiding_tensorUnit_left]
  monoidal

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