cechNerve — Mathlib

English

The differential at level n in the alternating coface map complex is the alternating sum of the coface maps: objD X n = sum_i (-1)^i X.δ_i.

Русский

Дифференциал на уровне n в чередующем Coface-комплексе равен чередующейся сумме Coface-карт: objD X n = ∑_i (-1)^i X.δ_i.

LaTeX

$$$\text{objD } X\; n = \sum_{i: F(n+2)} (-1)^{i} X.\delta_i$$$

Lean4

/-- The Čech nerve associated to an arrow. -/
@[simps]
def cechNerve : SimplicialObject C
    where
  obj n := widePullback.{0} f.right (fun _ : Fin (n.unop.len + 1) => f.left) fun _ => f.hom
  map g := WidePullback.lift (WidePullback.base _) (fun i => WidePullback.π _ (g.unop.toOrderHom i)) (by simp)

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