truncGE — Mathlib

English

For a cochain complex K, there is a canonical truncation from below at level n, denoted truncGE n, which is the subcomplex of K consisting of components in degrees ≥ n.

Русский

Для коцепного комплекса K существует каноническое усечение снизу на уровне n, обозначаемое truncGE n, которое является подкомплексом K, состоящим из компонент по степеням не ниже n.

LaTeX

$$$K_{\ge n} \coloneqq \mathrm{trunc}_{\ge n}(K)$$$

Lean4

/-- If `K : CochainComplex C ℤ`, this is the canonical truncation `≥ n` of `K`. -/
noncomputable abbrev truncGE (n : ℤ) : CochainComplex C ℤ :=
  HomologicalComplex.truncGE K (embeddingUpIntGE n)

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