truncLE — Mathlib

English

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

Русский

Для когепрямого комплекса K существует каноническое усечение сверху на уровне n, обозначаемое truncLE n, которое является подкомплексом K, состоящим из компонент по степеням не выше n.

LaTeX

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

Lean4

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

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