isoLeftDerivedToHomotopyCategoryObj_hom_naturality

English

The naturality of the homology component in the isomorphism for left-derived objects holds with additive functors.

Русский

Естественность гомологического компонента в изоморфизме для левого производного сохранена для аддитивных функторов.

LaTeX

$$$\text{hom}_n: (F.mapHomologicalComplex _) \;\to\; \text{HomotopyCategory.homology}(D, n) \text{ is natural in } φ.$$$

Lean4

@[reassoc]
theorem isoLeftDerivedToHomotopyCategoryObj_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] :
    F.leftDerivedToHomotopyCategory.map f ≫ (Q.isoLeftDerivedToHomotopyCategoryObj F).hom =
      (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
        (F.mapHomologicalComplex _ ⋙ HomotopyCategory.quotient _ _).map φ :=
  by
  dsimp
  rw [← cancel_epi (P.isoLeftDerivedToHomotopyCategoryObj F).inv, Iso.inv_hom_id_assoc,
    isoLeftDerivedToHomotopyCategoryObj_inv_naturality_assoc f P Q φ comm F, Iso.inv_hom_id, comp_id]

Похожие утверждения