quotient_obj_mem_subcategoryAcyclic_iff_exactAt

English

In the quotient category, an object is acyclic iff every ExactAt of K vanishes.

Русский

В факторной категории аксиома acyclic эквивалентна нулю каждого ExactAt для K.

LaTeX

$$$\\text{quotientObj}_\\star(K) \\in \\text{subcategoryAcyclic}(C) \\iff \\forall n, \\mathrm{ExactAt}_n(K).$$$

Lean4

theorem quotient_obj_mem_subcategoryAcyclic_iff_exactAt (K : CochainComplex C ℤ) :
    subcategoryAcyclic C ((quotient _ _).obj K) ↔ ∀ (n : ℤ), K.ExactAt n :=
  by
  rw [mem_subcategoryAcyclic_iff]
  refine forall_congr' (fun n => ?_)
  simp only [HomologicalComplex.exactAt_iff_isZero_homology]
  exact ((homologyFunctorFactors C (ComplexShape.up ℤ) n).app K).isZero_iff

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