English
For f: X → Y and injective resolutions I,J, the natural isomorphisms I^F_n, J^F_n commute with F.mapHomologicalComplex and φ: I.cocomplex → J.cocomplex.
Русский
Для отображения f: X → Y и разрешений I,J натуральные изоморфизмы I^F_n и J^F_n коммутируют с отображением F и с φ: I.cocomplex → J.cocomplex.
LaTeX
$$$ (I.isoRightDerivedToHomotopyCategoryObj Fn) \\circ F.map = F.map \\circ (J.isoRightDerivedToHomotopyCategoryObj Fn) $$$
Lean4
/-- If `I : InjectiveResolution Z` and `F : C ⥤ D` is an additive functor, this is
an isomorphism between `F.rightDerivedToHomotopyCategory.obj X` and the complex
obtained by applying `F` to `I.cocomplex`. -/
noncomputable def isoRightDerivedToHomotopyCategoryObj {X : C} (I : InjectiveResolution X) (F : C ⥤ D) [F.Additive] :
F.rightDerivedToHomotopyCategory.obj X ≅
(F.mapHomologicalComplex _ ⋙ HomotopyCategory.quotient _ _).obj I.cocomplex :=
(F.mapHomotopyCategory _).mapIso I.iso ≪≫ (F.mapHomotopyCategoryFactors _).app I.cocomplex
