English
Another instance of Localization.Lifting for HomotopyCategory with respect to the quasi-isomorphisms Up and the map to DerivedCategory.
Русский
Ещё одно подстановление локализации для HomotopyCategory относительно квазиизоморфизмов Up и отображения в DerivedCategory.
LaTeX
$$$\text{Localization.Lifting}\ DerivedCategory.Qh\ (HomotopyCategory.quasiIso\ C_1\ (ComplexShape.up\; \mathbb{Z}))\ ((F.mapHomotopyCategory\ (ComplexShape.up\; \mathbb{Z}))\circ DerivedCategory.Qh)\ F.mapDerivedCategory$$$
Lean4
instance : NatTrans.CommShift F.mapDerivedCategoryFactorsh.hom ℤ :=
inferInstanceAs
(NatTrans.CommShift
(Localization.Lifting.iso DerivedCategory.Qh (HomotopyCategory.quasiIso C₁ (ComplexShape.up ℤ))
(F.mapHomotopyCategory _ ⋙ DerivedCategory.Qh) F.mapDerivedCategory).hom
ℤ)
