English
For F : B ⥤ C and η : G ⟶ H with G,H : C ⥤ D, the natural transformation mapWhiskerLeft _ (whiskerLeft F η) factors through a canonical composite involving mapCompRight and mapWhiskerLeft of η.
Русский
Для F : B ⥤ C и η : G ⟶ H с G,H : C ⥤ D, естественное отношение mapWhiskerLeft ... раскладывается через канонический композиционный фактор, включающий mapCompRight и mapWhiskerLeft η.
LaTeX
$$$\operatorname{mapWhiskerLeft}\_\; (\operatorname{whiskerLeft} F\, \eta) = (\operatorname{mapCompRight}\ A F G)^{\mathrm{hom}} \;\circ \; \mathrm{whiskerLeft}(\operatorname{mapPair}(\mathbf{1}_A, F))\; (\operatorname{mapWhiskerLeft}\_\eta) \; \circ (\operatorname{mapCompRight}\ A F H)^{\mathrm{inv}}$$$
Lean4
@[reassoc]
theorem mapWhiskerLeft_whiskerLeft (F : B ⥤ C) {G H : C ⥤ D} (η : G ⟶ H) :
mapWhiskerLeft _ (whiskerLeft F η) =
(mapCompRight A F G).hom ≫ whiskerLeft (mapPair (𝟭 A) F) (mapWhiskerLeft _ η) ≫ (mapCompRight A F H).inv :=
by apply natTrans_ext <;> ext <;> simp [mapCompRight]
