English
Let η: F ≅ G be an isomorphism of functors C ⥤ D and H: D ⥤ E a functor. Then the core of the right whiskering isomorphism satisfies a similar identity: (isoWhiskerRight η H).core = F.coreComp H ≪≫ isoWhiskerRight η.core H.core ≪≫ (G.coreComp H).symm.
Русский
Пусть η: F ≅ G — изоморфизм между функторaми C ⥤ D, и H: D ⥤ E — функтор. Тогда ядро правого whiskerRight совпадает с аналогичным соответствием: (isoWhiskerRight η H).core = F.coreComp H ≪≫ isoWhiskerRight η.core H.core ≪≫ (G.coreComp H).symm.
LaTeX
$$$ (\\text{isoWhiskerRight } \\eta H).\\text{core} = F.\\text{coreComp } H \\\\llcorner\\\\;\\\\, (\\text{isoWhiskerRight } \\eta.\\text{core } H.\\text{core}) \\\\llcorner\\\\;\\\\, (G.\\text{coreComp } H).\\text{symm}. $$$
Lean4
theorem coreWhiskerRight {E : Type u₃} [Category.{v₃} E] {F G : C ⥤ D} (η : F ≅ G) (H : D ⥤ E) :
(isoWhiskerRight η H).core = F.coreComp H ≪≫ isoWhiskerRight η.core H.core ≪≫ (G.coreComp H).symm := by cat_disch
