extend_d_to_eq_zero — Mathlib

English

If no relation exists between i and its predecessor in the original complex, the extended differential from i' to j' is zero.

Русский

Если между i и его предшественником в исходном комплексе не существует отношения, расширенный дифференциал равен нулю.

LaTeX

$$$c.Rel (c.prev i) i \\Rightarrow (K.extend e).d i' j' = 0$$$

Lean4

theorem extend_d_to_eq_zero (i' j' : ι') (j : ι) (hj : e.f j = j') (hj' : ¬c.Rel (c.prev j) j) :
    (K.extend e).d i' j' = 0 := by
  obtain hi' | ⟨i, hi⟩ := (e.r i').eq_none_or_eq_some
  · exact extend.d_none_eq_zero _ _ _ hi'
  · rw [extend_d_eq K e (e.f_eq_of_r_eq_some hi) hj, K.shape, zero_comp, comp_zero]
    intro hij
    obtain rfl := c.prev_eq' hij
    exact hj' hij

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