English
Naturality of inverses in the isomorphisms between right-derived objects with respect to morphisms f.
Русский
Естественность обратных отображений в изоморфизмах правого производного при отображениях f.
LaTeX
$$$ (I.isoRightDerivedToHomotopyCategoryObj F).inv \\circ (F.rightDerived n).map f = (F.mapHomologicalComplex _ \\circ \\HomologicalComplex.homologyFunctor) \\circ φ \\circ (J.isoRightDerivedToHomotopyCategoryObj F).inv $$$
Lean4
@[reassoc]
theorem isoRightDerivedToHomotopyCategoryObj_inv_naturality {X Y : C} (f : X ⟶ Y) (I : InjectiveResolution X)
(J : InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex) (comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0) (F : C ⥤ D)
[F.Additive] :
(I.isoRightDerivedToHomotopyCategoryObj F).inv ≫ F.rightDerivedToHomotopyCategory.map f =
(F.mapHomologicalComplex _ ⋙ HomotopyCategory.quotient _ _).map φ ≫
(J.isoRightDerivedToHomotopyCategoryObj F).inv :=
by
rw [← cancel_epi (I.isoRightDerivedToHomotopyCategoryObj F).hom, Iso.hom_inv_id_assoc]
dsimp
rw [← isoRightDerivedToHomotopyCategoryObj_hom_naturality_assoc f I J φ comm F, Iso.hom_inv_id, comp_id]
