English
For p1, p2, p3 in integers with h1, h2 relations, the lift’s fst-variation respects the v-components, yielding a stable identity with α.
Русский
Для p1, p2, p3 целых чисел с условиями h1 и h2, компонент fst лифта сохраняет соответствие в α.
LaTeX
$$$ (\mathrm{lift}(φ, α, β, h))_v(p_1,p_2,h_1 2) \circ (\mathrm{fst}(φ))_v(p_2,p_3,h_2) = α_v(p_1,p_3, h) $$$
Lean4
/-- Constructor for homotopies between morphisms to a mapping cone. -/
noncomputable def liftHomotopy {K : CochainComplex C ℤ} (f₁ f₂ : K ⟶ mappingCone φ) (α : Cochain K F 0)
(β : Cochain K G (-1))
(h₁ : (Cochain.ofHom f₁).comp (fst φ).1 (zero_add 1) = -δ 0 1 α + (Cochain.ofHom f₂).comp (fst φ).1 (zero_add 1))
(h₂ :
(Cochain.ofHom f₁).comp (snd φ) (zero_add 0) =
δ (-1) 0 β + α.comp (Cochain.ofHom φ) (zero_add 0) + (Cochain.ofHom f₂).comp (snd φ) (zero_add 0)) :
Homotopy f₁ f₂ :=
(Cochain.equivHomotopy f₁ f₂).symm
⟨liftCochain φ α β (neg_add_cancel 1), by
simp [δ_liftCochain _ _ _ _ _ (zero_add 1), ext_cochain_to_iff _ _ _ (zero_add 1), h₁, h₂]⟩
