exactAt_succ_single_obj — Mathlib

English

For any object A of C and any natural number n, the chain complex obtained by placing A in degree 0 is exact at degree n+1:

Русский

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

LaTeX

$$$\\operatorname{ExactAt}\\left((\\mathrm{single}_0 C).\\mathrm{obj}(A)\\right)\\left(n+1\\right)$$$

Lean4

theorem exactAt_succ_single_obj (A : C) (n : ℕ) : ExactAt ((single₀ C).obj A) (n + 1) :=
  exactAt_single_obj _ _ _ _ (by simp)

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