extend_d_from_eq_zero — Mathlib

English

If a target index j' has a predecessor mapped via e, the differential from i' to j' vanishes when the related relation prevents a nonzero connection.

Русский

Если предшественник j' расширенного индекса связан через e и не существует ненулевого перехода, дифференциал от i' к j' равен нулю.

LaTeX

$$$(K.extend e).d i' j' = 0$ under appropriate non-relations$$

Lean4

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

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