πTruncGE — Mathlib

English

There is a canonical map from the original complex K to its ≥ n truncation K.truncGE n.

Русский

Существует каноническое отображение из исходного комплекса K к его усечению ≥ n: K → K.truncGE n.

LaTeX

$$$\pi_{\ge n}: K \to K_{\ge n}$$$

Lean4

/-- The canonical map `K ⟶ K.truncGE n` for `K : CochainComplex C ℤ`. -/
noncomputable def πTruncGE (n : ℤ) : K ⟶ K.truncGE n :=
  HomologicalComplex.πTruncGE K (embeddingUpIntGE n)

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