English
The composition of successive differentials is zero: d n m ≫ d m p = 0 whenever the indices form a composable chain.
Русский
Составные дифференциалы образуют нулевую композицию: d n m ≫ d m p = 0 при допустимой последовательности индексов.
LaTeX
$$d_comp_d (n m p : \mathbb{Z}) : h.d n m ≫ h.d m p = 0$$
Lean4
@[reassoc (attr := simp)]
theorem d_comp_d (n m p : ℤ) : h.d n m ≫ h.d m p = 0 :=
by
by_cases hnm : n + 1 = m; swap
· rw [h.shape n m hnm, zero_comp]
by_cases hmp : m + 1 = p; swap
· rw [h.shape m p hmp, comp_zero]
obtain n | (_ | _ | n) := n
· obtain rfl : m = .ofNat (n + 1) := by simp [← hnm]
obtain rfl : p = .ofNat (n + 2) := by simp [← hmp]; cutsat
simp only [Int.ofNat_eq_coe, X_ofNat, d_ofNat, HomologicalComplex.d_comp_d]
· obtain rfl : m = 0 := by cutsat
obtain rfl : p = 1 := by cutsat
simp
· obtain rfl : m = -1 := by cutsat
obtain rfl : p = 0 := by cutsat
simp
· obtain rfl : m = .negSucc (n + 1) := by cutsat
obtain rfl : p = .negSucc n := by cutsat
simp
