English
Equality of two expressions for a map between mapping cones: the direct map equals the map built from a homotopy between φ₁ and φ₂.
Русский
Эквивалентность двух выражений для отображения между отображающимися конусами: прямое отображение совпадает с отображением, построенным из гомотопии между φ₁ и φ₂.
LaTeX
$$$map φ_1 φ_2 a b comm = mapOfHomotopy (Homotopy.ofEq comm)$$$
Lean4
@[reassoc]
theorem triangleMapOfHomotopy_comm₃ : mapOfHomotopy H ≫ (triangle φ₂).mor₃ = (triangle φ₁).mor₃ ≫ a⟦1⟧' :=
by
ext p
dsimp [mapOfHomotopy, triangle]
-- the following list of lemmas as been obtained by doing
-- simp? [ext_from_iff _ _ _ rfl, Cochain.rightShift_v _ 1 0 _ p p _ (p + 1) rfl]
simp only [Int.reduceNeg, Cochain.rightShift_neg, Cochain.neg_v, shiftFunctor_obj_X',
Cochain.rightShift_v _ 1 0 _ p p _ (p + 1) rfl, shiftFunctor_obj_X, shiftFunctorObjXIso,
HomologicalComplex.XIsoOfEq_rfl, Iso.refl_inv, comp_id, Preadditive.comp_neg, Preadditive.neg_comp,
ext_from_iff _ _ _ rfl, inl_v_desc_f_assoc, Cochain.add_v, Cochain.zero_cochain_comp_v, Cochain.ofHom_v,
Cochain.comp_zero_cochain_v, Preadditive.add_comp, assoc, inl_v_fst_v, inr_f_fst_v, comp_zero, add_zero,
inl_v_fst_v_assoc, inr_f_desc_f_assoc, HomologicalComplex.comp_f, neg_zero, inr_f_fst_v_assoc, zero_comp, and_self]
