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