shortComplexTruncLE_shortExact — Mathlib

English

In any abelian category, for a cochain complex K and every integer n, the truncated short complex K.shortComplexTruncLE(n) is a short exact sequence.

Русский

В абелевой категории для любой комплексной коцепной последовательности K и каждого целого числа n трюсированное короткое комплексное повторение K.shortComplexTruncLE(n) образует короткую точную последовательность.

LaTeX

$$$\forall n \in \mathbb{Z}, \; (K.shortComplexTruncLE(n)).ShortExact, $$$

Lean4

theorem shortComplexTruncLE_shortExact (n : ℤ) : (K.shortComplexTruncLE n).ShortExact := by
  apply HomologicalComplex.shortComplexTruncLE_shortExact

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