English
The category of differential graded objects is equivalent to the category of homological complexes.
Русский
Категория дифференциально-градуированных объектов эквивалентна категории гомологической последовательности.
LaTeX
$$$\text{dgoEquivHomologicalComplex } : \text{DifferentialObject } \mathbb{Z} (\text{GradedObjectWithShift } b V) \simeq \text{HomologicalComplex } V (\text{ComplexShape.up' } b)$$$
Lean4
/-- The category of differential graded objects in `V` is equivalent
to the category of homological complexes in `V`.
-/
@[simps]
def dgoEquivHomologicalComplex :
DifferentialObject ℤ (GradedObjectWithShift b V) ≌ HomologicalComplex V (ComplexShape.up' b)
where
functor := dgoToHomologicalComplex b V
inverse := homologicalComplexToDGO b V
unitIso := dgoEquivHomologicalComplexUnitIso b V
counitIso := dgoEquivHomologicalComplexCounitIso b V
