mem_subcategoryAcyclic_iff — Mathlib

English

An object of the homotopy category lies in the acyclic subcategory iff all its homology objects vanish.

Русский

Объект в гомотопической категории относится к acyclic, если все его гомологии нулевые.

LaTeX

$$$X\\in \\text{subcategoryAcyclic}(C) \\;\\Leftrightarrow\\; \\forall n, IsZero((\\operatorname{homologyFunctor}\\, C\\,(ComplexShape.up\\,\\mathbb{Z}))_n(X)).$$$

Lean4

theorem mem_subcategoryAcyclic_iff (X : HomotopyCategory C (ComplexShape.up ℤ)) :
    subcategoryAcyclic C X ↔ ∀ (n : ℤ), IsZero ((homologyFunctor _ _ n).obj X) :=
  Functor.mem_homologicalKernel_iff _ X

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