ofCocomplex_exactAt_succ — Mathlib

English

For each n, the (n+1)-th object of the cocomplex yields an exactness condition at the next degree for the constructed resolution.

Русский

Для каждого n выполняется точность цели на следующем уровне резолюции.

LaTeX

$$theorem ofCocomplex_exactAt_succ (n : ℕ) : (ofCocomplex Z).ExactAt (n + 1)$$

Lean4

theorem ofCocomplex_exactAt_succ (n : ℕ) : (ofCocomplex Z).ExactAt (n + 1) :=
  by
  rw [HomologicalComplex.exactAt_iff' _ n (n + 1) (n + 1 + 1) (by simp) (by simp)]
  dsimp [ofCocomplex, CochainComplex.mk', CochainComplex.mk, HomologicalComplex.sc',
    HomologicalComplex.shortComplexFunctor']
  simp only [CochainComplex.of_d]
  match n with
  | 0 => apply exact_f_d ((CochainComplex.mkAux _ _ _ (d (Injective.ι Z)) (d (d (Injective.ι Z))) _ _ 0).f)
  | n + 1 => apply exact_f_d ((CochainComplex.mkAux _ _ _ (d (Injective.ι Z)) (d (d (Injective.ι Z))) _ _ (n + 1)).f)

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