obj — Mathlib

English

The normalized Moore complex functor on objects sends a simplicial object X to a chain complex whose nth object is objX X n, with differential given by objD X and the differential squares to zero by d_squared X.

Русский

Нормализованный Moore-функтор на объектам отображает симплициальный объект X в комплекс Морра: в степени n объект равен objX X n, дифференциал — objD X, и d² = 0 по теореме d_squared X.

LaTeX

$$$\mathrm{obj}(X) = \mathrm{ChainComplex.of}\big( n \mapsto (\mathrm{objX}\,X\,n) \big)\; (\mathrm{objD}\,X)\; (\mathrm{d\_squared}\,X) $$$

Lean4

/-- The normalized Moore complex functor, on objects.
-/
@[simps!]
def obj (X : SimplicialObject C) : ChainComplex C ℕ :=
  ChainComplex.of (fun n => (objX X n : C)) (objD X) (d_squared X)

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