English
The commShift iso for PullbackShift along φ and F is equal to the whiskered pullback shift iso, followed by F's commShift iso, and then whiskered inverse pullback shift iso.
Русский
КоммShift-изоморфизм PullbackShift вдоль φ и F равен композиции изоморфизмов pullbackShift с обрамлением и затем – коммShift-изоморфизм F, завершающийся обратным обрамлением.
LaTeX
$$$\text{PullbackShift.functor }\varphi\; F\;\text{ isomorphism } = \ isoWhiskerRight (pullbackShiftIso C \varphi a b h) F \; \llCorner\llCorner\, (F.commShiftIso b) \; \llCorner\llCorner\; isoWhiskerLeft F (pullbackShiftIso D \varphi a b h).symm$$$
Lean4
theorem commShiftPullback_iso_eq (a : A) (b : B) (h : b = φ a) :
(PullbackShift.functor φ F).commShiftIso a (C := PullbackShift C φ) (D := PullbackShift D φ) =
isoWhiskerRight (pullbackShiftIso C φ a b h) F ≪≫
(F.commShiftIso b) ≪≫ isoWhiskerLeft F (pullbackShiftIso D φ a b h).symm :=
by
obtain rfl : b = φ a := h
rfl
