d_squared — Mathlib

English

For every n, the composition of successive differentials is zero: d_n ∘ d_{n+1} = 0 in the normalized Moore complex.

Русский

Для каждого n композиция последовательных дифференциалов равна нулю: d_n ∘ d_{n+1} = 0 в нормализованном Moore-комплексе.

LaTeX

$$$\forall n \in \mathbb{N},\; d_n \circ d_{n+1} = 0$$$

Lean4

theorem d_squared (n : ℕ) : objD X (n + 1) ≫ objD X n = 0 := by
  -- It's a pity we need to do a case split here;
      -- after the first rw the proofs are almost identical

  rcases n with _ | n <;> dsimp [objD]
  ·
    rw [Subobject.factorThru_arrow_assoc, Category.assoc, ← Fin.castSucc_zero, ←
      X.δ_comp_δ_assoc (Fin.zero_le (0 : Fin 2)), ←
      factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ (0 : Fin 2) (by simp)), Category.assoc,
      kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]
  ·
    rw [factorThru_right, factorThru_eq_zero, factorThru_arrow_assoc, Category.assoc, ← Fin.castSucc_zero, ←
      X.δ_comp_δ (Fin.zero_le (0 : Fin (n + 3))), ←
      factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ (0 : Fin (n + 3)) (by simp)), Category.assoc,
      kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]

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