toGradedObjectMap — Mathlib

English

A morphism of bicomplexes induces a morphism of their graded objects via mapping on each bi-index.

Русский

Гомоморфизм би-комплексов индуцирует гомоморфизм градационных объектов по каждому би-индексу.

LaTeX

$$$\varphi: K \to L \Rightarrow K.\text{toGradedObject} \to L.\text{toGradedObject}$$$

Lean4

/-- The morphism of graded objects induced by a morphism of bicomplexes. -/
def toGradedObjectMap {K L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) : K.toGradedObject ⟶ L.toGradedObject :=
  fun ⟨i₁, i₂⟩ => (φ.f i₁).f i₂

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