The short complexes attached to homological complexes #
In this file, we define a functor
shortComplexFunctor C c i : HomologicalComplex C c ⥤ ShortComplex C
.
By definition, the image of a homological complex K
by this functor
is the short complex K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i)
.
When the homology refactor is completed (TODO @joelriou), the homology
of a homological complex K
in degree i
shall be the homology
of the short complex (shortComplexFunctor C c i).obj K
, which can be
abbreviated as K.sc i
.
The functor HomologicalComplex C c ⥤ ShortComplex C
which sends a homological
complex K
to the short complex K.X i ⟶ K.X j ⟶ K.X k
for arbitrary indices i
, j
and k
.
Instances For
The functor HomologicalComplex C c ⥤ ShortComplex C
which sends a homological
complex K
to the short complex K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i)
.
Instances For
The natural isomorphism shortComplexFunctor C c j ≅ shortComplexFunctor' C c i j k
when c.prev j = i
and c.next j = k
.
Instances For
The short complex K.X i ⟶ K.X j ⟶ K.X k
for arbitrary indices i
, j
and k
.
Instances For
The short complex K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i)
.
Instances For
The canonical isomorphism K.sc j ≅ K.sc' i j k
when c.prev j = i
and c.next j = k
.