inr_f_triangle_mor₃_f — Mathlib

English

The composition of inr φ with the mor₃ part of the triangle φ is zero.

Русский

Составление inr φ с mor₃ части треугольника φ равно нулю.

LaTeX

$$$(inr φ).f_p \\circ (triangle φ).mor_3^{f p} = 0$$$

Lean4

@[reassoc (attr := simp)]
theorem inr_f_triangle_mor₃_f (p : ℤ) : (inr φ).f p ≫ (triangle φ).mor₃.f p = 0 :=
  by
  dsimp [triangle]
    -- the following list of lemmas was obtained by doing
      -- simp? [Cochain.rightShift_v _ 1 0 _ p p (add_zero p) (p+1) rfl]

  simp only [Cochain.rightShift_neg, Cochain.neg_v, shiftFunctor_obj_X',
    Cochain.rightShift_v _ 1 0 _ p p (add_zero p) (p + 1) rfl, shiftFunctor_obj_X, shiftFunctorObjXIso,
    HomologicalComplex.XIsoOfEq_rfl, Iso.refl_inv, comp_id, Preadditive.comp_neg, inr_f_fst_v, neg_zero]

Похожие утверждения