equivalence_functor — Mathlib

English

There is an equivalence of categories between simplicial objects in A and chain complexes of A with natural numbers indexing.

Русский

Существует эквивалентность категорий между симплициальными объектами в A и цепными комплексами в A с индексами в ℕ.

LaTeX

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

Lean4

theorem equivalence_functor : (equivalence : SimplicialObject C ≌ _).functor = N :=
  rfl

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