English
Let φ: K → L be a morphism of cochain complexes. In the mapping cone triangle attached to φ, the hom component of the rotated homotopy equivalence composed with the third morphism of the triangle on inr φ equals the negative of φ with a unit degree shift: (rotateHomotopyEquiv φ).hom ∘ (triangle(inr φ)).mor_3 = - φ⟦1⟧'.
Русский
Пусть φ: K → L — морфизм комплексів Кохейнов; в треугольнике конуса отображения, получаемом из φ, композиция компоненты гомотопии вращения с траекторией mor_3 треугольника над inr φ равна отрицательному сдвигу φ на единицу: (rotateHomotopyEquiv φ).hom ∘ (triangle(inr φ)).mor_3 = - φ⟦1⟧'.
LaTeX
$$$ (\\mathrm{rotateHomotopyEquiv}(\\phi)).hom \\circ (\\mathrm{triangle}(\\mathrm{inr}(\\phi))).mor_3 = -\\, \\phi^{\\langle 1\\rangle}' $$$
Lean4
@[reassoc (attr := simp)]
theorem rotateHomotopyEquiv_comm₃ : (rotateHomotopyEquiv φ).hom ≫ (triangle (inr φ)).mor₃ = -φ⟦1⟧' :=
by
ext p
dsimp [rotateHomotopyEquiv]
-- the following list of lemmas has been obtained by doing
-- simp? [lift_f _ _ _ _ _ (p + 1) rfl,
-- (Cochain.ofHom φ).leftShift_v 1 1 (zero_add 1) p (p + 1) rfl (p + 1) (by omega)]
simp only [Int.reduceNeg, lift_f _ _ _ _ _ (p + 1) rfl, shiftFunctor_obj_X', Cocycle.coe_neg, Cocycle.leftShift_coe,
Cocycle.ofHom_coe, Cochain.neg_v, (Cochain.ofHom φ).leftShift_v 1 1 (zero_add 1) p (p + 1) rfl (p + 1) (by cutsat),
shiftFunctor_obj_X, mul_one, sub_self, mul_zero, Int.zero_ediv, add_zero, Int.negOnePow_one, shiftFunctorObjXIso,
HomologicalComplex.XIsoOfEq_rfl, Iso.refl_hom, Cochain.ofHom_v, id_comp, Units.neg_smul, one_smul, neg_neg,
Preadditive.neg_comp, Preadditive.add_comp, assoc, inl_v_triangle_mor₃_f, Iso.refl_inv, Preadditive.comp_neg,
comp_id, inr_f_triangle_mor₃_f, comp_zero, neg_zero]
