exactAt_succ_single_obj — Mathlib

English

Similarly, for the cochain counterpart, the chain complex concentrated at degree zero is exact at every positive degree, i.e., at degree instHAdd(n) + 1.

Русский

Аналогично для коцеподобного случая: коцепной комплекс, сконцентрированный в нулевой степени, точен на всех положительных степенях, т.е. на степени instHAdd(n) + 1.

LaTeX

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

Lean4

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

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