English
On objects, the normalized Moore complex functor assigns to a simplicial object X the chain complex with nth object objX X n and differentials given by objD X, forming a functor on the category of simplicial objects to chain complexes.
Русский
На уровне объектов нормализованный Moore-функтор отправляет симплициальный объект X в цепной комплекс с n-ым объектом objX X n и дифференциалами objD X, образуя функтор из категории симплициальных объектов в цепные комплексы.
LaTeX
$$$\\mathrm{normalizedMooreComplex}(X) : \\mathrm{SimplicialObject}(C) \\to \\mathrm{ChainComplex}(C,\\mathbb{N})$, на объектах задаётся как $n \\mapsto \\mathrm{objX}\,X\,n$, дифференциалы — $\\mathrm{objD}\,X$ и собственно определение даёт структуру функторного отображения.$$
Lean4
/-- The (normalized) Moore complex of a simplicial object `X` in an abelian category `C`.
The `n`-th object is intersection of
the kernels of `X.δ i : X.obj n ⟶ X.obj (n-1)`, for `i = 1, ..., n`.
The differentials are induced from `X.δ 0`,
which maps each of these intersections of kernels to the next.
-/
@[simps]
def normalizedMooreComplex : SimplicialObject C ⥤ ChainComplex C ℕ
where
obj := obj
map f := map f
