English
The opposite of the associator is obtained by a long composite involving opComp, isoWhiskerLeft on op, and op of F, G, H.
Русский
Противоположность ассоциатора получается через длинную композицию, включающую opComp и isoWhiskerLeft, а также операции op.
LaTeX
$$$\\\\forall {C} [Category C], \\\\forall {D} [Category D], \\\\forall {E} [Category E], \\\\forall {F : CategoryTheory.Functor C D}, \\\\forall {G : CategoryTheory.Functor D E}, \\\\forall {H : CategoryTheory.Functor E E'}, \\\\text{NatIso}.op (F.associator G H) = (F.opComp (G.comp H)).trans \\\\circ (F.op.isoWhiskerLeft (G.opComp H)).trans \\\\circ (F.op.associator G.op H.op).symm \\\\circ \\\\mathrm{isoWhiskerRight}( (\\\\mathrm{Functor}.opComp _ _).symm ) H.op \\\\circ (\\\\mathrm{Functor}.opComp _ _).symm.$$$
Lean4
theorem op_associator {E E' : Type*} [Category E] [Category E'] {F : C ⥤ D} {G : D ⥤ E} {H : E ⥤ E'} :
NatIso.op (Functor.associator F G H) =
Functor.opComp _ _ ≪≫
isoWhiskerLeft F.op (Functor.opComp _ _) ≪≫
(Functor.associator F.op G.op H.op).symm ≪≫
isoWhiskerRight (Functor.opComp _ _).symm H.op ≪≫ (Functor.opComp _ _).symm :=
by cat_disch
