associator_natural — Mathlib

English

Passing braiding through a map: (biprod.braiding X W).hom ≫ biprod.map f g ≫ (biprod.braiding Y Z).hom = biprod.map g f.

Русский

Проход BRAIDING через отображение: (braiding X W).hom ≫ biprod.map f g ≫ (braiding Y Z).hom = biprod.map g f.

LaTeX

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

Lean4

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

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