English
There exists a localization lifting from DerivedCategory.Q to the target given by quasi-isomorphisms of Up-shift complexes, compatible with F.mapDerivedCategory.
Русский
Существует подстановочное сопряжение локализации от DerivedCategory.Q к цели, заданной квазиизоморфизмами Up-цикла, совместимое с F.mapDerivedCategory.
LaTeX
$$$\text{Localization.Lifting}\; DerivedCategory.Q\; (HomologicalComplex.quasiIso\; C_1\ (ComplexShape.up\; \mathbb{Z}))\ ((F.mapHomologicalComplex\ (ComplexShape.up\; \mathbb{Z}))\circ DerivedCategory.Q)\ F.mapDerivedCategory$$$
Lean4
noncomputable instance :
Localization.Lifting DerivedCategory.Q (HomologicalComplex.quasiIso C₁ (ComplexShape.up ℤ))
(F.mapHomologicalComplex _ ⋙ DerivedCategory.Q) F.mapDerivedCategory :=
⟨F.mapDerivedCategoryFactors⟩
