English
A construction of a homotopy between morphisms from mappingCone φ to K yields an equality relating fst, snd, and descComponents with δ and φ.
Русский
Построение гомотопии между морфизмами из mappingCone φ в K устанавливает равенство между компонентами fst, snd и desc, связанное с δ и φ.
LaTeX
$$$\text{Homotopy relations for mappingCone}$$$
Lean4
/-- Constructor for homotopies between morphisms from a mapping cone. -/
noncomputable def descHomotopy {K : CochainComplex C ℤ} (f₁ f₂ : mappingCone φ ⟶ K) (γ₁ : Cochain F K (-2))
(γ₂ : Cochain G K (-1))
(h₁ :
(inl φ).comp (Cochain.ofHom f₁) (add_zero (-1)) =
δ (-2) (-1) γ₁ + (Cochain.ofHom φ).comp γ₂ (zero_add (-1)) + (inl φ).comp (Cochain.ofHom f₂) (add_zero (-1)))
(h₂ : Cochain.ofHom (inr φ ≫ f₁) = δ (-1) 0 γ₂ + Cochain.ofHom (inr φ ≫ f₂)) : Homotopy f₁ f₂ :=
(Cochain.equivHomotopy f₁ f₂).symm
⟨descCochain φ γ₁ γ₂ (by simp), by
simp only [Cochain.ofHom_comp] at h₂
simp [ext_cochain_from_iff _ _ _ (neg_add_cancel 1), δ_descCochain _ _ _ _ _ (neg_add_cancel 1), h₁, h₂]⟩
