English
Let F be a pseudofunctor, and sq a commutative square with t, l, r, b. For any φ: X1 → Y2, and any equation hφ: t ≫ r = φ, the canonical map map map of the square equals the composite of the two canonical mapComp' isomorphisms: the inverse of mapComp' t r φ together with φ, followed by mapComp' l b φ with φ adjusted by hφ.
Русский
Пусть F — псевдофунктор, и sq — комм-квадрат с t, l, r, b. Для любого φ: X1 → Y2 и равенства hφ: t ≫ r = φ, каноническое отображение квадрата равно композиции двух канонических изоморфизмов mapComp': сначала обратная карта mapComp' t r φ вместе с φ, затем mapComp' l b φ с учётом hφ.
LaTeX
$$$ F.isoMapOfCommSq sq = (F.mapComp' t r φ (by rw [hφ])).symm \\circ F.mapComp' l b φ (by rw [← hφ, sq.w]) $$
Lean4
theorem isoMapOfCommSq_eq (φ : X₁ ⟶ Y₂) (hφ : t ≫ r = φ) :
F.isoMapOfCommSq sq = (F.mapComp' t r φ (by rw [hφ])).symm ≪≫ F.mapComp' l b φ (by rw [← hφ, sq.w]) :=
by
subst hφ
simp [isoMapOfCommSq, mapComp'_eq_mapComp]
