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