associator_inv — Mathlib

English

The inverse of the associator is given by a dual explicit product decomposition with fst and snd projections as above.

Русский

Обратный ассоциатор задаётся явным образом через соответствующее разложение на произведении с использованием fst и snd.

LaTeX

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

Lean4

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

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