braiding_naturality_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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