The differential of a cochain complex as a cochain

Mathlib's CochainComplex.HomComplex.Cochain.diff K is the differential of a cochain complex K read as a degree 1 cochain from K to itself, and CochainComplex.HomComplex.δ is the differential of the Hom complex. This file records the elementary calculus relating the two: δ is composition with the differential cochains on either side, a morphism of cochain complexes commutes with them, and they square to zero.

These are general facts about Mathlib's Hom complex, independent of any particular use.

Main results

• TauCeti.δ_eq_comp_diff_add_diff_comp: the differential of the Hom complex is δ z = z d + (-1)^(n+1) d z.
• TauCeti.ofHom_comp_diff: a morphism of cochain complexes commutes with the differential cochains.
• TauCeti.diff_comp_diff: the differential cochain squares to zero.

theorem TauCeti.δ_eq_comp_diff_add_diff_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (n m : ℤ) (hnm : n + 1 = m) (z : CochainComplex.HomComplex.Cochain F G n) : CochainComplex.HomComplex.δ n m z = z.comp (CochainComplex.HomComplex.Cochain.diff G) ⋯ + m.negOnePow • (CochainComplex.HomComplex.Cochain.diff F).comp z ⋯

The differential of the Hom complex, written through composition with the differential cochains of the source and of the target: δ z = z d + (-1)^(n+1) d z.

theorem TauCeti.ofHom_comp_diff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) : (CochainComplex.HomComplex.Cochain.ofHom φ).comp (CochainComplex.HomComplex.Cochain.diff G) ⋯ = (CochainComplex.HomComplex.Cochain.diff F).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯

A morphism of cochain complexes commutes with the differential cochains.

@[simp]

theorem TauCeti.diff_comp_diff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (F : CochainComplex C ℤ) : (CochainComplex.HomComplex.Cochain.diff F).comp (CochainComplex.HomComplex.Cochain.diff F) diff_comp_diff._proof_2 = 0

The differential cochain squares to zero.