English
Theorem equating mapWhiskerLeft (whiskerLeft η H) with a composite built from mapCompRight, mapPair and mapWhiskerLeft η and mapWhiskerLeft of η.
Русский
Теорема устанавливает равенство mapWhiskerLeft (whiskerLeft η H) и композиции, построенной из mapCompRight, mapPair и mapWhiskerLeft η и mapWhiskerLeft η.
LaTeX
$$$\operatorname{mapWhiskerLeft}\_ (\mathrm{whiskerLeft}\ F\, \eta) = (\operatorname{mapCompRight}\ A F H)^{\mathrm{hom}} \;\circ \; \mathrm{whiskerLeft}(\operatorname{mapPair}(\mathbf{1}_A, F))\; (\operatorname{mapWhiskerLeft}\ _\eta) \; \circ (\operatorname{mapCompRight}\ A F G)^{\mathrm{inv}}$$$
Lean4
@[reassoc]
theorem mapWhiskerLeft_whiskerRight {F G : B ⥤ C} (η : F ⟶ G) (H : C ⥤ D) :
mapWhiskerLeft _ (whiskerRight η H) =
(mapCompRight A F H).hom ≫ whiskerRight (mapWhiskerLeft _ η) (mapPair (𝟭 A) H) ≫ (mapCompRight A G H).inv :=
by apply natTrans_ext <;> ext <;> simp [mapCompRight]
