The spectral object and the spectral sequence of a filtered complex #
A functor F : ι ⥤ CochainComplex C ℤ to cochain complexes in an abelian category C gives a
spectral object CochainComplex.spectralObject F in C indexed by ι: to f : i ⟶ j and
n : ℤ it attaches the nth cohomology of the mapping cone of F.map f, and its connecting
maps are those of the distinguished triangles of mapping cones in the homotopy category. When
F.map f is a monomorphism, this cohomology is that of the cokernel of F.map f
(CochainComplex.spectralObjectHIsoCokernel). An increasing filtration ℤ → Subobject K of a
cochain complex K, extended by ⊥ and ⊤, is such a functor indexed by EInt
(CochainComplex.filtrationFunctor), whose transition maps are monomorphisms.
The spectral sequence of a functor indexed by EInt is Mathlib's spectral sequence of a spectral
object, for the recipe coreE₂Cohomological
(CochainComplex.spectralSequence): its first page, numbered 2 there, has at (p, q) the
cohomology H^{p+q} of the mapping cone of F_q ⟶ F_{q+1}
(CochainComplex.spectralSequenceFirstPageXIso). When this map is a monomorphism, for instance
for a filtration, this is the cohomology H^{p+q}(F_{q+1}/F_q) of a graded piece
(CochainComplex.spectralSequenceFirstPageXIsoCokernel).
Main definitions #
CochainComplex.spectralObject F: the spectral object ofF : ι ⥤ CochainComplex C ℤ.CochainComplex.spectralObjectMap α: the morphism of spectral objects induced by a natural transformationα : F ⟶ G, functorial inα.CochainComplex.filtrationFunctor F hF: the functorEInt ⥤ CochainComplex C ℤof an increasing filtrationF : ℤ → Subobject K.CochainComplex.spectralSequence F: the spectral sequence ofF : EInt ⥤ CochainComplex C ℤ.
Main results #
CochainComplex.cokernelFiltrationFunctorMapIso: the cokernel of a transition map of the functor of a filtration is the cokernel of the inclusion of subcomplexes.CochainComplex.cokernelFiltrationFunctorMapIsoOfIsColimit: when the pieces of a filtration are represented by monomorphismsX p ⟶ K, that cokernel is any cokernel ofX p ⟶ X (p + 1).CochainComplex.spectralObjectHIso:H^n(f)is the cohomology of the mapping cone ofF.map f.CochainComplex.spectralObjectHIsoCokernel: for a monomorphismF.map f,H^n(f)is the cohomology of the cokernel ofF.map f.CochainComplex.spectralObject_H_map_comp_spectralObjectHIso_homandCochainComplex.spectralObject_H_map_comp_spectralObjectHIsoCokernel_hom: the mapsH^n(f) ⟶ H^n(g)induced by morphisms of arrows are the maps in cohomology of the induced morphisms of mapping cones, respectively cokernels.CochainComplex.spectralSequenceFirstPageXIso: the first page is the cohomology of the mapping cones ofF_q ⟶ F_{q+1}.CochainComplex.spectralSequenceFirstPageXIsoCokernel: whenF_q ⟶ F_{q+1}is a monomorphism, the first page isH^{p+q}(F_{q+1}/F_q).CochainComplex.spectralObject_δ: the connecting maps are those of the triangles of mapping cones.CochainComplex.spectralObjectMap_hom_app_hIso: onH^n(f),spectralObjectMap αis the map in cohomology of the induced morphism of mapping cones.
References #
- J.-L. Verdier, Des catégories dérivées des catégories abéliennes, II.4.
- J. McCleary, A User's Guide to Spectral Sequences, Theorem 2.6.
The connecting maps of the triangulated spectral object
(spectralObjectMappingCone C).precomp F are the third morphisms of the distinguished
triangles of mapping cones attached to F.map f and F.map g.
The morphism of triangulated spectral objects in the homotopy category induced by a natural
transformation α : F ⟶ G: on f : i ⟶ j, the morphism of mapping cones of F.map f and
G.map f given by α.app i and α.app j.
Instances For
The spectral object of a functor F : ι ⥤ CochainComplex C ℤ: its object H^n(f) for
f : i ⟶ j is obtained by applying the cohomology functor of the homotopy category to the mapping
cone of F.map f (see spectralObjectHIso), and its connecting maps are those of the
distinguished triangles of mapping cones (see spectralObject_δ).
Instances For
The objects H^n(f) of the spectral object of F are the cohomology of the mapping cones of
the maps F.map f.
Instances For
The connecting maps of the spectral object of F, read through spectralObjectHIso, are the
maps in cohomology induced by the third morphisms cone (F.map g) ⟶ (cone (F.map f))⟦1⟧ of the
triangles of mapping cones attached to F.map f and F.map g.
The maps H^n(f) ⟶ H^n(g) of the spectral object of F induced by morphisms of arrows
φ : f ⟶ g, read through spectralObjectHIso, are the maps in cohomology of the induced
morphisms of mapping cones.
The maps H^n(f) ⟶ H^n(g) of the spectral object of F induced by morphisms of arrows
φ : f ⟶ g, read through spectralObjectHIso, are the maps in cohomology of the induced
morphisms of mapping cones.
The morphism of spectral objects spectralObject F ⟶ spectralObject G induced by a natural
transformation α : F ⟶ G.
Instances For
On H^n(f), the morphism of spectral objects induced by α is the map in cohomology of the
morphism of mapping cones of F.map f and G.map f.
When F.map f is a monomorphism, H^n(f) is the nth cohomology of the cokernel of
F.map f, through the quasi-isomorphism mappingCone.descShortComplex from the mapping cone of
F.map f to its cokernel.
Instances For
The maps H^n(f) ⟶ H^n(g) of the spectral object of F induced by morphisms of arrows
φ : f ⟶ g such that F.map f and F.map g are monomorphisms, read through
spectralObjectHIsoCokernel, are the maps in cohomology of the induced morphisms of cokernels.
The maps H^n(f) ⟶ H^n(g) of the spectral object of F induced by morphisms of arrows
φ : f ⟶ g such that F.map f and F.map g are monomorphisms, read through
spectralObjectHIsoCokernel, are the maps in cohomology of the induced morphisms of cokernels.
An increasing filtration F : ℤ → Subobject K extended to EInt, by ⊥ at ⊥ and ⊤ at
⊤.
Instances For
The functor EInt ⥤ CochainComplex C ℤ of an increasing filtration F : ℤ → Subobject K:
it sends n : ℤ to the subcomplex F n, ⊥ to the zero subcomplex and ⊤ to K.
Instances For
The object of the functor of a filtration at a : EInt is the subcomplex filtrationEInt F a
of K.
Instances For
The transition maps of the functor of a filtration are the inclusions of subcomplexes.
The maps F_⊥ ⟶ F_a of the functor of a filtration vanish, their source being zero.
The cokernel of a transition map of the functor of a filtration is the cokernel of the corresponding inclusion of subcomplexes.
Instances For
The isomorphism CochainComplex.cokernelFiltrationFunctorMapIso is induced by the identity of
the subcomplex.
The isomorphism CochainComplex.cokernelFiltrationFunctorMapIso is induced by the identity of
the subcomplex.
The inclusion of the object at a : EInt of the functor of a filtration into the filtered
complex.
Instances For
The inclusions into the filtered complex are natural in the object of the functor of a filtration.
The inclusions into the filtered complex are natural in the object of the functor of a filtration.
At an integer q, the inclusion filtrationFunctorArrow F hF q is the inclusion of the
subcomplex F_q.
A morphism of complexes sending each piece of a filtration into the corresponding piece of
another one does so for the extensions of the filtrations to EInt.
The spectral sequence of a functor F : EInt ⥤ CochainComplex C ℤ, starting on page 2
(the first page in Mathlib's numbering for coreE₂Cohomological).
Instances For
The objects on the first page of the spectral sequence of F: at pq = (p, q), the
(p + q)th cohomology of the mapping cone of F_q ⟶ F_{q+1}. The indices q, q + 1 and
p + q are given as i₁, i₂ and n together with equations, for flexibility.
Instances For
The objects on the first page of the spectral sequence of F when the transition maps of
F are monomorphisms: at pq = (p, q), the (p + q)th cohomology of the graded piece
F_{q+1}/F_q.
Instances For
When each piece F p of a filtration is represented by a monomorphism ι p : X p ⟶ K, the
object of the functor of the filtration at p is X p.
Instances For
The identification CochainComplex.filtrationFunctorObjIsoOfEqMk is compatible with the
inclusions into the filtered complex.
The identification CochainComplex.filtrationFunctorObjIsoOfEqMk is compatible with the
inclusions into the filtered complex.
Under CochainComplex.filtrationFunctorObjIsoOfEqMk, the transition map F_p ⟶ F_{p+1} of
the functor of the filtration is any map X p ⟶ X (p + 1) compatible with the inclusions.
Under CochainComplex.filtrationFunctorObjIsoOfEqMk, the transition map F_p ⟶ F_{p+1} of
the functor of the filtration is any map X p ⟶ X (p + 1) compatible with the inclusions.
When each piece F p of a filtration is represented by a monomorphism ι p : X p ⟶ K, the
graded piece F_{p+1}/F_p, the cokernel of the transition map of the functor of the filtration,
is the target of any cokernel g of a map X p ⟶ X (p + 1) compatible with the inclusions.
Instances For
The isomorphism CochainComplex.cokernelFiltrationFunctorMapIsoOfIsColimit identifies the
cokernel projection with g.
The isomorphism CochainComplex.cokernelFiltrationFunctorMapIsoOfIsColimit identifies the
cokernel projection with g.