braiding_naturality_left — Mathlib

English

Braiding on the left is natural with respect to morphisms on the left argument.

Русский

Брейдинг по левому аргументу естественен по отношению к морфизмам слева.

LaTeX

$$$\forall X,f,Z:\, \mathrm{tensorHom}(f, \mathrm{id}_Z) \circ \mathrm{braiding}(X, Z) = \mathrm{braiding}(X, Y) \circ \mathrm{tensorHom}(\mathrm{id}_Z, f)$$$

Lean4

theorem braiding_naturality_left {X Y : Dial C} (f : X ⟶ Y) (Z : Dial C) :
    tensorHom f (𝟙 Z) ≫ (braiding Y Z).hom = (braiding X Z).hom ≫ tensorHom (𝟙 Z) f := by cat_disch

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