objD — Mathlib

English

For any Cosimplicial object X, the differential objD X n equals the unop of the differential in the cosimplicial image of X under the cosimplicialSimplicialEquiv, evaluated at n.

Русский

Для любой косимплициальной конструкции X дифференциал objD X n равен обратному по знаку дифференциалу в косимпликальной картинки X под cosimplicialSimplicialEquiv, в точке n.

LaTeX

$$$\\text{objD } X\\ n = (\\text{AlternatingFaceMapComplex.objD}((\\cosimplicialSimplicialEquiv C).\\mathrm{functor.obj}(\\mathrm{op}\,X))\\ n).\\mathrm{unop}$$$

Lean4

/-- The differential on the alternating coface map complex is the alternate
sum of the coface maps -/
@[simp]
def objD (n : ℕ) : X.obj ⦋n⦌ ⟶ X.obj ⦋n + 1⦌ :=
  ∑ i : Fin (n + 2), (-1 : ℤ) ^ (i : ℕ) • X.δ i

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