English
Let C and D be cochain complexes of V indexed by the natural numbers, in a preadditive category. For every i ∈ ℕ and every family of morphisms f = (f i j) with f i j : C.X i → D.X j, the boundary operator prevD evaluated at i acts by composing the component f i,i−1 with the differential D.d (i−1) i; with the convention prevD 0 f = 0 (there is no i−1 when i = 0).
Русский
Пусть C и D — кограничные комплексы (коцепные?) объектов V, индексируемые по натуральным числам, в предадитивной категории. Для каждого i ∈ ℕ и всякая семейство морфизмов f = (f i j) cоответствует f i j : C.X i → D.X j, предел prevD на i действует как композиция f i,i−1 с дифференциалом D.d (i−1) i; при i = 0 имеем prevD 0 f = 0 (нет i−1).
LaTeX
$$$\displaystyle\forall i\in\mathbb{N},\, (\text{prevD}\, i\, f)=\begin{cases} f_{i,i-1}\circ D_{i-1,i}, & i>0,\\ 0, & i=0.\end{cases}$$$
Lean4
theorem prevD_nat (C D : CochainComplex V ℕ) (i : ℕ) (f : ∀ i j, C.X i ⟶ D.X j) :
prevD i f = f i (i - 1) ≫ D.d (i - 1) i := by
dsimp [prevD]
cases i
· simp only [shape, CochainComplex.prev_nat_zero, ComplexShape.up_Rel, not_false_iff, comp_zero, reduceCtorEq]
· congr <;> simp
