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)
.
The homology K.homology i
of a homological complex K
in degree i
is defined as
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
.
Equations
- One or more equations did not get rendered due to their size.
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)
.
Equations
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
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The short complex K.X i ⟶ K.X j ⟶ K.X k
for arbitrary indices i
, j
and k
.
Equations
Instances For
The short complex K.X (c.prev i) ⟶ K.X i ⟶ K.X (c.next i)
.
Equations
Instances For
The canonical isomorphism K.sc j ≅ K.sc' i j k
when c.prev j = i
and c.next j = k
.
Equations
- K.isoSc' i j k hi hk = (HomologicalComplex.natIsoSc' C c i j k hi hk).app K
Instances For
A homological complex K
has homology in degree i
if the associated
short complex K.sc i
has.
Instances For
The homology in degree i
of a homological complex.
Equations
Instances For
The cycles in degree i
of a homological complex.
Equations
Instances For
The inclusion of the cycles of a homological complex.
Equations
Instances For
The homology class map from cycles to the homology of a homological complex.
Equations
Instances For
The morphism to K.cycles i
that is induced by a "cycle", i.e. a morphism
to K.X i
whose postcomposition with the differential is zero.
Equations
Instances For
The morphism to K.cycles i
that is induced by a "cycle", i.e. a morphism
to K.X i
whose postcomposition with the differential is zero.
Instances For
The map K.X i ⟶ K.cycles j
induced by the differential K.d i j
.
Equations
- K.toCycles i j = K.liftCycles (K.d i j) (c.next j) ⋯ ⋯
Instances For
K.cycles i
is the kernel of K.d i j
when c.next i = j
.
Instances For
K.homology j
is the cokernel of K.toCycles i j : K.X i ⟶ K.cycles j
when c.prev j = i
.
Instances For
The opcycles in degree i
of a homological complex.
Equations
Instances For
The projection to the opcycles of a homological complex.
Equations
Instances For
The inclusion map of the homology of a homological complex into its opcycles.
Equations
Instances For
The morphism from K.opcycles i
that is induced by an "opcycle", i.e. a morphism
from K.X i
whose precomposition with the differential is zero.
Instances For
The morphism from K.opcycles i
that is induced by an "opcycle", i.e. a morphism
from K.X i
whose precomposition with the differential is zero.
Instances For
The map K.opcycles i ⟶ K.X j
induced by the differential K.d i j
.
Equations
- K.fromOpcycles i j = K.descOpcycles (K.d i j) (c.prev i) ⋯ ⋯
Instances For
K.opcycles j
is the cokernel of K.d i j
when c.prev j = i
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
K.homology i
is the kernel of K.fromOpcycles i j : K.opcycles i ⟶ K.X j
when c.next i = j
.
Instances For
The map K.homology i ⟶ L.homology i
induced by a morphism in HomologicalComplex
.
Equations
Instances For
The map K.cycles i ⟶ L.cycles i
induced by a morphism in HomologicalComplex
.
Equations
Instances For
The map K.opcycles i ⟶ L.opcycles i
induced by a morphism in HomologicalComplex
.
Equations
Instances For
The i
th homology functor HomologicalComplex C c ⥤ C
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The homology functor to graded objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The i
th cycles functor HomologicalComplex C c ⥤ C
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The i
th opcycles functor HomologicalComplex C c ⥤ C
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The natural transformation K.homologyπ i : K.cycles i ⟶ K.homology i
for all K : HomologicalComplex C c
.
Equations
Instances For
The natural transformation K.homologyι i : K.homology i ⟶ K.opcycles i
for all K : HomologicalComplex C c
.
Equations
Instances For
The natural isomorphism K.homology i ≅ (K.sc i).homology
for all homological complexes K
.
Equations
Instances For
The natural isomorphism K.homology j ≅ (K.sc' i j k).homology
for all homological complexes K
when c.prev j = i
and c.next j = k
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical isomorphism K.cycles i ≅ K.X i
when the differential from i
is zero.
Instances For
The canonical isomorphism K.homology i ≅ K.opcycles i
when the differential from i
is zero.
Instances For
The canonical isomorphism K.X j ≅ K.opCycles j
when the differential to j
is zero.
Instances For
The canonical isomorphism K.cycles j ≅ K.homology j
when the differential to j
is zero.
Instances For
A homological complex K
is exact at i
if the short complex K.sc i
is exact.
Equations
Instances For
A homological complex K
is acyclic if it is exact at i
for any i
.
Instances For
The canonical isomorphism K.homology 0 ≅ K.opcycles 0
for a chain complex K
indexed by ℕ
.
Equations
Instances For
The canonical isomorphism K.cycles 0 ≅ K.homology 0
for a cochain complex K
indexed by ℕ
.
Equations
Instances For
The cycles of a homological complex in degree j
can be computed
by specifying a choice of c.prev j
and c.next j
.
Equations
Instances For
The homology of a homological complex in degree j
can be computed
by specifying a choice of c.prev j
and c.next j
.
Equations
Instances For
The opcycles of a homological complex in degree j
can be computed
by specifying a choice of c.prev j
and c.next j
.