equivalence — Mathlib

English

For an abelian category A, there is an equivalence between the simplicial objects in A and chain complexes in A concentrated in nonnegative degrees, realized by the functors N and Γ with the Karoubi refinement.

Русский

Для абелевой категории A существует эквивалентность между симпликальными объектами A и цепочечными комплексами A в неотрицательных степенях, реализуемая через функторы N и Γ с уточнением Карауби.

LaTeX

$$$$ \mathrm{SimplicialObject}(A) \simeq \mathrm{ChainComplex}(A, \mathbb{N}) $$$$

Lean4

/-- The Dold-Kan equivalence for abelian categories -/
@[simps! functor]
def equivalence : SimplicialObject A ≌ ChainComplex A ℕ :=
  (Idempotents.DoldKan.equivalence (C := A)).changeFunctor comparisonN.symm

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