alternatingFaceMapComplex_obj_X — Mathlib

English

The alternating face map complex is a functor from simplicial objects in C to chain complexes in C.

Русский

Чередующийся лицевой отображение образует функтор от симпликсиальных объектов в C к цепным комплексам в C.

LaTeX

$$alternatingFaceMapComplex : SimplicialObject C ⥤ ChainComplex C ℕ$$

Lean4

@[simp]
theorem alternatingFaceMapComplex_obj_X (X : SimplicialObject C) (n : ℕ) :
    ((alternatingFaceMapComplex C).obj X).X n = X _⦋n⦌ :=
  rfl

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