mapHomologicalComplexUpToQuasiIsoFactorsh

Lean4

/-- The functor `F.mapHomologicalComplexUpToQuasiIso c` is induced by
`F.mapHomotopyCategory c`. -/
noncomputable def mapHomologicalComplexUpToQuasiIsoFactorsh :
    HomologicalComplexUpToQuasiIso.Qh ⋙ F.mapHomologicalComplexUpToQuasiIso c ≅
      F.mapHomotopyCategory c ⋙ HomologicalComplexUpToQuasiIso.Qh :=
  Localization.liftNatIso (HomotopyCategory.quotient C c) (HomologicalComplex.homotopyEquivalences C c)
    (HomotopyCategory.quotient C c ⋙ HomologicalComplexUpToQuasiIso.Qh ⋙ F.mapHomologicalComplexUpToQuasiIso c)
    (HomotopyCategory.quotient C c ⋙ F.mapHomotopyCategory c ⋙ HomologicalComplexUpToQuasiIso.Qh) _ _
    (F.mapHomologicalComplexUpToQuasiIsoFactors c)

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