ofComplex_exactAt_succ — Mathlib

English

For every natural number n, the projective resolution of Z is exact at degree n+1.

Русский

Для всякого натурального числа n резолюция по З является точной в степени n+1.

LaTeX

$$$\\mathrm{ofComplex}(Z).\\mathrm{ExactAt}(n+1)$$$

Lean4

theorem ofComplex_exactAt_succ (n : ℕ) : (ofComplex Z).ExactAt (n + 1) :=
  by
  rw [HomologicalComplex.exactAt_iff' _ (n + 1 + 1) (n + 1) n (by simp) (by simp)]
  dsimp [ofComplex, HomologicalComplex.sc', HomologicalComplex.shortComplexFunctor', ChainComplex.mk', ChainComplex.mk]
  simp only [ChainComplex.of_d]
    -- TODO: this should just be apply exact_d_f so something is missing

  match n with
  | 0 => apply exact_d_f
  | n + 1 => apply exact_d_f

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