English
The construction of equivHomotopy respects δ in the sense that applying δ to the image under the equivalence equals the image under the equivalence of δ applied to the original cochain, up to the appropriate shift in indices.
Русский
Построение equivHomotopy сохраняет δ; применение δ к образу через эквивалентность равняется образу через эквивалентность δ к исходному кокейну (с соответствующим сдвигом индексов).
LaTeX
$$$\\text{δ-map compatibility under equivalence: } δ(-1)0(z) \\mapsto δ(-1)0(z).$$$
Lean4
/-- If `Φ : C ⥤ D` is an additive functor, a cochain `z : Cochain K L n` between
cochain complexes in `C` can be mapped to a cochain between the cochain complexes
in `D` obtained by applying the functor
`Φ.mapHomologicalComplex _ : CochainComplex C ℤ ⥤ CochainComplex D ℤ`. -/
def map : Cochain ((Φ.mapHomologicalComplex _).obj K) ((Φ.mapHomologicalComplex _).obj L) n :=
Cochain.mk (fun p q hpq => Φ.map (z.v p q hpq))
