English
The core of the associator between F, G, H equals the composite of the cores and whiskers as detailed: coreAssociator equality expresses compatibility of the core with the associator under various whiskers and inverses.
Русский
Ядро ассоциатора между F, G, H совпадает с соответствующим композиционным выражением через ядра и whisker-операции.
LaTeX
$$$ (F.\\mathrm{associator} G H).\\mathrm{core} = (F \\;\\cdot\\; G).\\mathrm{coreComp} H \\;\\ll≫\\; \\mathrm{isoWhiskerRight}(F.\\mathrm{coreComp} G) H.\\mathrm{core} \\;\\ll≫\\; \\mathrm{Functor.associator} F.\\mathrm{core} G.\\mathrm{core} H.\\mathrm{core} \\;\\ll≫\\; (\\mathrm{isoWhiskerLeft} F.\\mathrm{core} (G.\\mathrm{coreComp} H)).\\mathrm{symm} \\;\\ll≫\\; (F.\\mathrm{coreComp} (G \\;\\cdot\\; H)).\\mathrm{symm} $$$
Lean4
theorem coreAssociator {E : Type u₃} [Category.{v₃} E] {E' : Type u₄} [Category.{v₄} E'] (F : C ⥤ D) (G : D ⥤ E)
(H : E ⥤ E') :
(Functor.associator F G H).core =
(F ⋙ G).coreComp H ≪≫
isoWhiskerRight (F.coreComp G) H.core ≪≫
Functor.associator F.core G.core H.core ≪≫
(isoWhiskerLeft F.core (G.coreComp H)).symm ≪≫ (F.coreComp (G ⋙ H)).symm :=
by cat_disch
