d_comp_d — Mathlib

English

The differential composed with itself is zero in truncGE'.

Русский

Дифференциал, композиция с самим собой, равен нулю в truncGE'.

LaTeX

$$$d_{K,e}(i,j) \circ d_{K,e}(j,k) = 0$ for all i,j,k with $c.Rel(i,j)$ and $c.Rel(j,k)$$$

Lean4

@[reassoc (attr := simp)]
theorem d_comp_d (i j k : ι) : d K e i j ≫ d K e j k = 0 :=
  by
  dsimp [d]
  by_cases hij : c.Rel i j
  · by_cases hjk : c.Rel j k
    · rw [dif_pos hij, dif_pos hjk, dif_neg (e.not_boundaryGE_next hij)]
      split_ifs <;> simp
    · rw [dif_neg hjk, comp_zero]
  · rw [dif_neg hij, zero_comp]

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