braiding_tensor_left_inv — Mathlib

English

Inverse braiding on the right is given by a standard composite with associators and braidings.

Русский

Обратимый braiding справа задаётся стандартной композицией через ассоциаторы и braiding.

LaTeX

$$$$ (β_X (Y ⊗ Z))^{−1} = (α_Y Z X)^{hom} ≫ Y ◁ (β_X Z)^{−1} ≫ (α_Y X Z)^{−1} ≫ (β_X Y)^{−1} ▷ Z ≫ (α_X Y Z)^{hom} $$$$

Lean4

@[simp, reassoc]
theorem braiding_tensor_left_inv (X Y Z : C) :
    (β_ (X ⊗ Y) Z).inv = (α_ Z X Y).inv ≫ (β_ X Z).inv ▷ Y ≫ (α_ X Z Y).hom ≫ X ◁ (β_ Y Z).inv ≫ (α_ X Y Z).inv :=
  eq_of_inv_eq_inv (by simp)

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