braiding_inv_naturality_left — Mathlib

English

Inverse left braiding is given by a standard composite with α and β and their inverses.

Русский

Левый обратимый braiding задаётся через α и β и их обратные.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem braiding_inv_naturality_left {X Y : C} (f : X ⟶ Y) (Z : C) : f ▷ Z ≫ (β_ Z Y).inv = (β_ Z X).inv ≫ Z ◁ f :=
  CommSq.w <| .vert_inv <| .mk <| braiding_naturality_right Z f

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