English
Let C be a category with zero morphisms and I1, I2 be index sets with complex shapes c1, c2. There exists a functor from the bicomplexes over C with shapes c1, c2 to the category of graded objects indexed by I1 × I2, sending each bicomplex K to its associated graded object, and sending a morphism φ to the induced graded-object morphism.
Русский
Пусть C — категория с нулевыми морфизмами, и пусть c1, c2 — формы комплексностей. Существует функтор от би-комплексoв над C с формами c1, c2 в категорию градуированных объектов, индексируемых по I1 × I2, который отправляет бикомплекс K в соответствующий градуированный объект K.toGradedObject, а морфизм φ — в индуцированный морфизм градуированного объекта.
LaTeX
$$$F : \mathrm{HomologicalComplex}_2(C;c_1,c_2) \to \mathrm{GradedObject}(I_1 \times I_2) C$, \\ F(K) = K^{\mathrm{toGradedObject}}, \quad F(\varphi) = \mathrm{toGradedObjectMap}(\varphi).$$
Lean4
/-- The functor which sends a bicomplex to its associated graded object. -/
@[simps]
def toGradedObjectFunctor : HomologicalComplex₂ C c₁ c₂ ⥤ GradedObject (I₁ × I₂) C
where
obj K := K.toGradedObject
map φ := toGradedObjectMap φ
