English
Naturality of the right-derived object with respect to a morphism f: X → Y in the source category.
Русский
Естественность правого производного по отношению к отображению f: X → Y в исходной категории.
LaTeX
$$$ (F.rightDerived n).map f \\; = \\; \\cdots $$$
Lean4
@[reassoc]
theorem isoRightDerivedObj_hom_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] (n : ℕ) :
(F.rightDerived n).map f ≫ (J.isoRightDerivedObj F n).hom =
(I.isoRightDerivedObj F n).hom ≫ (F.mapHomologicalComplex _ ⋙ HomologicalComplex.homologyFunctor _ _ n).map φ :=
by
dsimp [isoRightDerivedObj, Functor.rightDerived]
rw [assoc, ← Functor.map_comp_assoc,
InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality f I J φ comm F, Functor.map_comp, assoc]
erw [(HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.naturality]
rfl
