English
The homology component of the isomorphism is natural in morphisms f: X → Y between objects with projective resolutions.
Русский
Гомологический компонент изоморфизма естествен по морфизмам f: X → Y между объектами с проективными разрешениями.
LaTeX
$$$\text{hom}_n: (F.leftDerived n).map f \to \text{...}$ is natural in f.$$
Lean4
@[reassoc]
theorem isoLeftDerivedObj_hom_naturality {X Y : C} (f : X ⟶ Y) (P : ProjectiveResolution X) (Q : ProjectiveResolution Y)
(φ : P.complex ⟶ Q.complex) (comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f) (F : C ⥤ D) [F.Additive] (n : ℕ) :
(F.leftDerived n).map f ≫ (Q.isoLeftDerivedObj F n).hom =
(P.isoLeftDerivedObj F n).hom ≫ (F.mapHomologicalComplex _ ⋙ HomologicalComplex.homologyFunctor _ _ n).map φ :=
by
dsimp [isoLeftDerivedObj, Functor.leftDerived]
rw [assoc, ← Functor.map_comp_assoc,
ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality f P Q φ comm F, Functor.map_comp, assoc]
erw [(HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.naturality]
rfl
