ιTruncLE — Mathlib

English

There is a natural inclusion map from the ≤ n truncation back into the original complex K.

Русский

Существует естественное включение из усечения ≤ n обратно в исходный комплекс K.

LaTeX

$$$\iota_{\le n}: K_{\le n} \to K$$$

Lean4

/-- The canonical map `K.truncLE n ⟶ K` for `K : CochainComplex C ℤ`. -/
noncomputable def ιTruncLE (n : ℤ) : K.truncLE n ⟶ K :=
  HomologicalComplex.ιTruncLE K (embeddingUpIntLE n)

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