English
A symmetric version of the lifting between DerivedCategory and its QuasiIso framework exists with respect to F.mapDerivedCategory.
Русский
Существуют симметричные варианты подстановления между DerivedCategory и фреймворком квазиизоморфизмов относительно 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
theorem mapDerivedCategoryFactorsh_hom_app (K : CochainComplex C₁ ℤ) :
F.mapDerivedCategoryFactorsh.hom.app ((HomotopyCategory.quotient _ _).obj K) =
F.mapDerivedCategory.map ((DerivedCategory.quotientCompQhIso C₁).hom.app K) ≫
F.mapDerivedCategoryFactors.hom.app K ≫
(DerivedCategory.quotientCompQhIso C₂).inv.app _ ≫
DerivedCategory.Qh.map ((F.mapHomotopyCategoryFactors (ComplexShape.up ℤ)).inv.app K) :=
F.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app K
