exact_succ — Mathlib

English

If P is a ProjectiveResolution of Z, then the tail of the complex is exact, i.e., at succ index.

Русский

Если P — проективное разрешение Z, хвост комплекса точен, то есть в индексе succ.

LaTeX

$$$ \\mathrm{ProjectiveResolution}.\\mathrm{complex}.\\mathrm{ExactAt}(\\text{succ}). $$$

Lean4

theorem exact_succ (n : ℕ) : (ShortComplex.mk _ _ (P.complex.d_comp_d (n + 2) (n + 1) n)).Exact :=
  ((HomologicalComplex.exactAt_iff' _ (n + 2) (n + 1) n) (by simp only [prev]; rfl) (by simp)).1
    (P.complex_exactAt_succ n)

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