isoRightDerivedToHomotopyCategoryObj_hom_naturality

English

The naturality of the isomorphism with an associative refinement holds; i.e., the associativity-compatible diagram commutes.

Русский

Согласованность натурализации изоморфизма с ассоциативной редукцией: диаграмма сходится.

LaTeX

$$$ \\text{naturality with assoc of } isoRightDerivedToHomotopyCategory \\, $$$

Lean4

@[reassoc]
theorem isoRightDerivedToHomotopyCategoryObj_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] :
    F.rightDerivedToHomotopyCategory.map f ≫ (J.isoRightDerivedToHomotopyCategoryObj F).hom =
      (I.isoRightDerivedToHomotopyCategoryObj F).hom ≫
        (F.mapHomologicalComplex _ ⋙ HomotopyCategory.quotient _ _).map φ :=
  by
  dsimp [Functor.rightDerivedToHomotopyCategory, isoRightDerivedToHomotopyCategoryObj]
  rw [← Functor.map_comp_assoc, iso_hom_naturality f I J φ comm, Functor.map_comp, assoc, assoc]
  erw [(F.mapHomotopyCategoryFactors (ComplexShape.up ℕ)).hom.naturality]
  rfl

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