toGradedObject — Mathlib

English

There is a graded object indexed by the product I1 × I2 given bicomplex K, defined by K.X i1.X i2.

Русский

Существует градуированный объект, индексируемый произведением I1 × I2, задаваемый bicomplex K: K.X(i1).X(i2).

LaTeX

$$$K: \mathrm{HomologicalComplex}_{C}(c_1,c_2) \Rightarrow \mathrm{GradedObject}(I_1\!\times\!I_2)\, C$ with $(K.toGradedObject)(i_1,i_2) = K.X(i_1).X(i_2)$$$

Lean4

/-- The graded object indexed by `I₁ × I₂` induced by a bicomplex. -/
def toGradedObject (K : HomologicalComplex₂ C c₁ c₂) : GradedObject (I₁ × I₂) C := fun ⟨i₁, i₂⟩ => (K.X i₁).X i₂

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