English
There is a natural isomorphism in the opposite direction, the counit of the equivalence between differential objects and homological complexes.
Русский
Существует естественный изоморфизм противостоящий единице эквивалентности — counit эквивалентности между дифференциальными объектами и гомологическими комплексами.
LaTeX
$$$\mathrm{dgoToHomologicalComplex} \circ \mathrm{homologicalComplexToDGO} \cong \mathrm{Id}$$$
Lean4
/-- The functor from differential graded objects to homological complexes.
-/
@[simps]
def dgoToHomologicalComplex :
DifferentialObject ℤ (GradedObjectWithShift b V) ⥤ HomologicalComplex V (ComplexShape.up' b)
where
obj
X :=
{ X := fun i => X.obj i
d := fun i j => if h : i + b = j then X.d i ≫ X.objEqToHom (show i + (1 : ℤ) • b = j by simp [h]) else 0
shape := fun i j w => by dsimp at w; convert dif_neg w
d_comp_d' := fun i j k hij hjk => by
dsimp at hij hjk; substs hij hjk
simp [objEqToHom_d_assoc] }
map {X Y}
f :=
{ f := f.f
comm' := fun i j h => by
dsimp at h ⊢
subst h
have : f.f i ≫ Y.d i = X.d i ≫ f.f _ := (congr_fun f.comm i).symm
simp only [dite_true, Category.assoc, eqToHom_f', reassoc_of% this] }
