singleFunctorCompHomologyFunctorIso

English

There is a canonical isomorphism between the derived-category-level homology and the homology functor on the underlying complexes, realized via a chain of natural isomorphisms.

Русский

Существует каноническое изоморфие между гомологией в вывводимой категории и гомологией на базовых комплексах, реализованное через цепочку естественных изоморфий.

LaTeX

$$$\\text{singleFunctor } C n \\;\\circ\\; \\text{homologyFunctor } C n \\cong \\mathrm{Id}_C$$$

Lean4

/-- The canonical isomorphism
`DerivedCategory.singleFunctor C n ⋙ DerivedCategory.homologyFunctor C n ≅ 𝟭 C` -/
noncomputable def singleFunctorCompHomologyFunctorIso (n : ℤ) : singleFunctor C n ⋙ homologyFunctor C n ≅ 𝟭 C :=
  Functor.isoWhiskerRight ((SingleFunctors.evaluation _ _ n).mapIso (singleFunctorsPostcompQIso C)) _ ≪≫
    Functor.associator _ _ _ ≪≫
      Functor.isoWhiskerLeft _ (homologyFunctorFactors C n) ≪≫ (HomologicalComplex.homologyFunctorSingleIso _ _ _)

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