truncLEMap — Mathlib

English

The morphism between truncLE of K and truncLE of L induced by a morphism φ: K → L yields a natural map K.truncLE n → L.truncLE n.

Русский

Гомоморфизм между усечениями ≤ n комплексами K и L, индуцированный морфизмом φ: K → L, задаёт отображение K.truncLE n → L.truncLE n.

LaTeX

$$$\mathrm{truncLEMap}_n(\varphi): K_{\le n} \to L_{\le n}$$$

Lean4

/-- The morphism `K.truncLE n ⟶ L.truncLE n` induced by a morphism `K ⟶ L`. -/
noncomputable abbrev truncLEMap (n : ℤ) : K.truncLE n ⟶ L.truncLE n :=
  HomologicalComplex.truncLEMap φ (embeddingUpIntLE n)

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