braid_natural — Mathlib

English

The braiding morphism for a binary product is natural with respect to maps f: X → Y and g: Z → W; i.e., prod.map f g ≫ braiding = braiding ≫ prod.map g f.

Русский

Перемешивание (braiding) для двоичного произведения естественно относится к отображениям f и g: prod.map f g ≫ braiding = braiding ≫ prod.map g f.

LaTeX

$$$\forall f: X\to Y, g: Z\to W,\; prod.map f g ≫ prod.braiding Y W = prod.braiding X Z ≫ prod.map g f$$$

Lean4

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

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