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