English
For a pseudofunctor F, with a square where the top map is identity, the left and right maps are f, and the bottom is identity, the associated iso mapMapOfCommSq is equal to the pasting of whiskered id maps and unitors on the sides.
Русский
Пусть псевдофунктор F имеет квадрат, в котором верхняя стрелка — тождество, левая и правая стрелки равны f, нижняя — тождество; соответствующий изоморфизм F.isoMapOfCommSq равен пастингу с штриховками по обе стороны и едва заметными единичными униторами.
LaTeX
$$$ F.isoMapOfCommSq = \\big(\\mathrm{whiskerRightIso} (F.mapId X_1) (F.map f)\\big) \\\\; \\circ \\big(\\rho_{F.map f}\\big) \\circ (\\lambda_{F.map f})^{\\mathrm{symm}} \\circ \\big(\\mathrm{whiskerLeftIso} (F.map f) (F.mapId X_2)\\mathrm{symm}\\big) $$$
Lean4
/-- Equational lemma for `Pseudofunctor.isoMapOfCommSq` when
both vertical maps of the square are the same and horizontal maps are identities. -/
theorem isoMapOfCommSq_horiz_id (f : X₁ ⟶ X₂) :
F.isoMapOfCommSq (t := 𝟙 _) (l := f) (r := f) (b := 𝟙 _) ⟨by simp⟩ =
whiskerRightIso (F.mapId X₁) (F.map f) ≪≫ λ_ _ ≪≫ (ρ_ _).symm ≪≫ (whiskerLeftIso (F.map f) (F.mapId X₂)).symm :=
by
ext
rw [isoMapOfCommSq_eq _ _ f (by simp), mapComp'_comp_id, mapComp'_id_comp]
simp
