associator_hom — Mathlib

English

The hom component of the associator is given by the explicit product of canonical projections; i.e., (associator X Y Z).hom is the canonical product morphism built from fst and snd projections.

Русский

Гомоморф ассоциатора задаётся явным образом как канонический продукт проекций fst и snd (гомоморфия ассоциатора).

LaTeX

$$$$ (\mathrm{associator} X Y Z).hom = \mathrm{prod'}\Big(\mathrm{fst}(X \times Y) Z \circ \mathrm{fst} X Y, \mathrm{prod'}\big(\mathrm{fst}(X \times Y) Z \circ \mathrm{snd} X Y\big) (\mathrm{snd}(X \times Y) Z) \Big). $$$$

Lean4

theorem associator_hom (X : Cat) (Y : Cat) (Z : Cat) :
    (associator X Y Z).hom =
      Functor.prod' (Prod.fst (X × Y) Z ⋙ Prod.fst X Y)
        ((Functor.prod' ((Prod.fst (X × Y) Z ⋙ Prod.snd X Y)) (Prod.snd (X × Y) Z : (X × Y) × Z ⥤ Z))) :=
  rfl

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