truncGEMap — Mathlib

English

There is a morphism between truncGE of K and truncGE of L induced by φ: K.truncGE n → L.truncGE n.

Русский

Существует морфизм между TruncGE(K) и TruncGE(L), индуцируемый φ: K.truncGE n → L.truncGE n.

LaTeX

$$$\mathrm{truncGEMap}_n(\varphi): K_{\ge n} \to L_{\ge n}$$$

Lean4

/-- The morphism `K.truncGE n ⟶ L.truncGE n` induced by a morphism `K ⟶ L`. -/
noncomputable abbrev truncGEMap (n : ℤ) : K.truncGE n ⟶ L.truncGE n :=
  HomologicalComplex.truncGEMap φ (embeddingUpIntGE n)

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