shortComplexTruncLE_shortExact_δ_eq_zero

English

In variant, the δ component remains zero in the corresponding short exact segment.

Русский

В варианте δ-компонента остается нулевым в соответствующем отрезке короткой точной последовательности.

LaTeX

$$$ (⋯).δ=0 $$$

Lean4

@[simp]
theorem shortComplexTruncLE_shortExact_δ_eq_zero (i' j' : ι') (hij' : c'.Rel i' j') :
    (K.shortComplexTruncLE_shortExact e).δ i' j' hij' = 0 :=
  by
  by_cases hj : ∃ j, e.f j = j'
  · obtain ⟨j, rfl⟩ := hj
    rw [← cancel_mono (homologyMap (K.ιTruncLE e) (e.f j)), zero_comp]
    exact (K.shortComplexTruncLE_shortExact e).δ_comp i' _ hij'
  · apply ((K.truncLE e).exactAt_of_isSupported e j' (by simpa using hj)).isZero_homology.eq_of_tgt

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