English
In the mapping cone triangle, the v-component of inl φ composed with the triangle mor₃ matches a canonical shifted isomorphism.
Русский
В компоненте v в треугольнике отображающего конуса композиция inl φ с mor₃ треугольника совпадает с каноническим сдвинутым изоморфизмом.
LaTeX
$$$(inl φ).v_{p,q} \\circ (triangle φ).mor_3^{f,q} = -\\big( K.shiftFunctorObjXIso 1 q p \\big)^{-1}$$$
Lean4
@[reassoc (attr := simp)]
theorem inl_v_triangle_mor₃_f (p q : ℤ) (hpq : p + (-1) = q) :
(inl φ).v p q hpq ≫ (triangle φ).mor₃.f q =
-(K.shiftFunctorObjXIso 1 q p (by rw [← hpq, neg_add_cancel_right])).inv :=
by
dsimp [triangle]
-- the following list of lemmas was obtained by doing
-- simp? [Cochain.rightShift_v _ 1 0 (zero_add 1) q q (add_zero q) p (by omega)]
simp only [Int.reduceNeg, Cochain.rightShift_neg, Cochain.neg_v, shiftFunctor_obj_X',
Cochain.rightShift_v _ 1 0 (zero_add 1) q q (add_zero q) p (by cutsat), shiftFunctor_obj_X, shiftFunctorObjXIso,
Preadditive.comp_neg, inl_v_fst_v_assoc]
