English
Alternate expression for zero differential in CochainComplex as indices are not consecutive.
Русский
Альтернативное выражение нулевого дифференциала в CochainComplex, если индексы не соседние.
LaTeX
$$$ (\\mathrm{CochainComplex.of}\\ X\ d\ sq)_{i j} = 0 \\text{ если } i+1 \\neq j$$$
Lean4
/-- A constructor for chain maps between `α`-indexed cochain complexes built using `CochainComplex.of`,
from a dependently typed collection of morphisms.
-/
@[simps]
def ofHom (f : ∀ i : α, X i ⟶ Y i) (comm : ∀ i : α, f i ≫ d_Y i = d_X i ≫ f (i + 1)) : of X d_X sq_X ⟶ of Y d_Y sq_Y :=
{ f
comm' := fun n m => by
by_cases h : n + 1 = m
· subst h
simpa using comm n
· rw [of_d_ne X _ _ h, of_d_ne Y _ _ h]
simp }
