braid_natural — Mathlib

English

The map biprod.map commutes with braidings: biprod.map f g ≫ (biprod.braiding Y W).hom = (biprod.braiding X Z).hom ≫ biprod.map g f.

Русский

Отображение biprod.map становится совместимым с браидингами: biprod.map f g ≫ braiding.hom = braiding.hom ≫ biprod.map g f.

LaTeX

$$$\mathrm{biprod.map} \ f\ g \;\;≫\; (\mathrm{biprod.braiding} \ Y \ W)^{\mathrm{hom}} = (\mathrm{biprod.braiding} \ X \ Z)^{\mathrm{hom}} \;\;≫\; \mathrm{biprod.map} \ g\ f$$$

Lean4

/-- The braiding isomorphism can be passed through a map by swapping the order. -/
@[reassoc]
theorem braid_natural {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) :
    biprod.map f g ≫ (biprod.braiding _ _).hom = (biprod.braiding _ _).hom ≫ biprod.map g f := by cat_disch

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