obj — Mathlib

English

The alternating coface map complex on objects is the CochainComplex with terms X.obj ⟦n⟧ and differential given by objD X.

Русский

Чередующийся Coface-комплекс по объектам является сопоставлением CochainComplex с компонентами X.obj ⟦n⟧ и дифференциалом objD X.

LaTeX

$$$\text{obj: }\mathrm{CochainComplex}\; C\;\mathbb{N}, \; (\text{obj } X)_n = X.\mathrm{obj}\; ⟦n⟧, \; d = \text{objD } X$$$

Lean4

/-- The alternating coface map complex, on objects -/
def obj : CochainComplex C ℕ :=
  CochainComplex.of (fun n => X.obj ⦋n⦌) (objD X) (d_squared X)

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