English
In a localized setting, the hom component of the commShiftOfLocalization iso is given by a specific composite involving inv and hom of the Lifting iso and commShiftIso.
Русский
В локализованной обстановке гомоморфизм изоморфизма commShiftOfLocalization выражается через композицию с inv и hom из Lifting и commShiftIso.
LaTeX
$$$ (commShiftOfLocalization.iso\ L\ W\ F\ F'\ a).hom.app (L.obj X) = F'.map ((L.commShiftIso a).inv.app X) \gg (Lifting.iso L W F F').hom.app (X⟦a⟧) \gg (F.commShiftIso a).hom.app X \gg (shiftFunctor E a).map ((Lifting.iso L W F F').inv.app X) $$$
Lean4
@[simp, reassoc]
theorem iso_hom_app (a : A) (X : C) :
(commShiftOfLocalization.iso L W F F' a).hom.app (L.obj X) =
F'.map ((L.commShiftIso a).inv.app X) ≫
(Lifting.iso L W F F').hom.app (X⟦a⟧) ≫
(F.commShiftIso a).hom.app X ≫ (shiftFunctor E a).map ((Lifting.iso L W F F').inv.app X) :=
by simp [commShiftOfLocalization.iso]
