descCochain — Mathlib

English

The δ-operator at (0,1) on the mapping cone’s snd component equals the negative of the fst-δ-contribution composed with φ plus the snd-δ contribution composed with G’s differential.

Русский

δ(0,1) на nd компоненты mapping cone равен противоположному вкладу δ fst с φ плюс δ snd с G.

LaTeX

$$$\delta_{0,1}(snd φ) = - (fst φ)_1 \circ φ + (snd φ) \circ G_{d}.$$$

Lean4

/-- Given `φ : F ⟶ G`, this is the cochain in `Cochain (mappingCone φ) K n` that is
constructed from two cochains `α : Cochain F K m` (with `m + 1 = n`) and `β : Cochain F K n`. -/
noncomputable def descCochain (α : Cochain F K m) (β : Cochain G K n) (h : m + 1 = n) : Cochain (mappingCone φ) K n :=
  (fst φ).1.comp α (by rw [← h, add_comm]) + (snd φ).comp β (zero_add n)

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