instIsHomologicalIntUpHomologyFunctor

English

For every integer n, the homology functor on the category of shifted complexes is a homological functor; that is, it preserves exact triangles up to the usual isomorphisms in the triangulated structure.

Русский

Для каждого целого n, гомологическая функтор на категории сдвинутых комплексов является гомологическим функтором; он сохраняет точные тройки в обычном смысле треугольной структуры.

LaTeX

$$$\text{IsHomological}(\mathrm{Hom}(-, -),\mathrm{ComplexShape\,up}\,\mathbb{Z}, n).$$$

Lean4

instance (n : ℤ) : (homologyFunctor C (ComplexShape.up ℤ) n).IsHomological :=
  Functor.IsHomological.mk' _
    (fun T hT => by
      rw [distinguished_iff_iso_trianglehOfDegreewiseSplit] at hT
      obtain ⟨S, σ, ⟨e⟩⟩ := hT
      have hS := HomologicalComplex.shortExact_of_degreewise_shortExact S (fun n => (σ n).shortExact)
      exact
        ⟨_, e,
          (ShortComplex.exact_iff_of_iso (S.mapNatIso (homologyFunctorFactors C (ComplexShape.up ℤ) n))).2
            (hS.homology_exact₂ n)⟩)

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