The second page of the index spectral sequence #
Let m be a twisting cocycle over the generators P with values in a DG algebra A, and let
ℳ be a DG right A-module. The entries m x y between generators whose indices differ by one
are cycles of degree zero (TauCeti.TwistingCocycle.m_mem_zero_of_eq_add_one,
TauCeti.TwistingCocycle.d_m_eq_zero_of_eq_add_one), so they act on the cohomology of ℳ. The
classical complex in coefficient degree k has in degree q the product over the generators
of index q of the cohomology H^k(ℳ), and as differential the matrix of these actions, twisted
by the Koszul sign. It squares to zero by the twisting equation at index difference two
(TauCeti.TwistingCocycle.sum_subtype_m_mul_m_of_eq_add_two) and the Leibniz rule.
Under the splitting of the first page of the index spectral sequence into the cohomology of ℳ
(TauCeti.indexGradedPieceHomologyIso), the first differential is the classical differential
(TauCeti.TwistingCocycle.indexSpectralSequenceFirstPageXIsoOfEq_comp_indexClassicalD), so the
second page is the cohomology of the classical complex, the E² term of BDHO (Ch. 3, §4.2).
Main definitions #
TauCeti.TwistingCocycle.indexClassicalEntry: the action ofm x yon cohomology.TauCeti.TwistingCocycle.indexClassicalD: the matrix of the entries.TauCeti.TwistingCocycle.indexClassicalComplex: the classical complex in coefficient degreek.
Main results #
TauCeti.TwistingCocycle.indexSpectralSequenceSecondPageXIso: the second page of the index spectral sequence at(a, b)is the homology in degreeb + 1of the classical complex in coefficient degreea + 2 * b + 1.
Implementation notes #
The pages are numbered as in Mathlib's CochainComplex.spectralSequence: the first page E₁ is
page 2 and the second page E₂ is page 3. The object at (a, b) of page 2 is the
cohomology in total degree a + b of the graded piece of index b + 1.
References #
- J.-F. Barraud, M. Damian, V. Humilière, A. Oancea, Floer homology with DG coefficients. Applications to cotangent bundles, arXiv:2404.07953, Definition 3.38.
- J.-F. Barraud, M. Damian, V. Humilière, A. Oancea, Morse homology with differential graded coefficients, Progress in Mathematics 360, Birkhäuser, 2025, Chapter 3 and Section 4.2.
The entry of the classical complex in coefficient degree k between a generator x of index
q + 1 and a generator y of index q: the action of the cycle m x y of degree zero on the
cohomology of ℳ in degree k, twisted by the Koszul sign.
Instances For
The differential of the classical complex in coefficient degree k, from the generators of
index q + 1 to those of index q: the matrix of the entries indexClassicalEntry.
Instances For
The classical differential squares to zero, entrywise: for generators x of index
q + 2 and z of index q, the sum over the generators y of index q + 1 of the composites of
the entries vanishes. On a class [α], the sum is the class of op (∑ y, m x y * m y z) • α,
which is -op (d (m x z)) • α by the twisting equation, a coboundary by the Leibniz rule.
The classical differential squares to zero, by sum_indexClassicalEntry_comp.
The classical complex in coefficient degree k: in degree q, the product over the
generators of index q of the cohomology of ℳ in degree k (as the cohomology of
shiftedModuleComplex hM q in degree k - q), with the differential indexClassicalD, the matrix
of the actions of the entries m x y between generators whose indices differ by one.
Instances For
The degree-q term of the classical complex is the product over the generators of index q
of the cohomology of ℳ in degree k.
Instances For
The differential of the classical complex is indexClassicalD, under the identification
indexClassicalComplexXIso of its terms with products of cohomology. (A plain equation
d = indexClassicalD is not available as a public statement, since the complex is not exposed and
its terms are only propositionally the products.)
The components of the classical differential are the entries indexClassicalEntry.
The components of the classical differential are the entries indexClassicalEntry.
The entries of the classical differential, on classes: the entry between generators x of
index q + 1 and y of index q sends the class of a cycle α of ℳ to the class of
op (m x y) • ε α, with ε the Koszul sign.
The entries of the first differential of the index spectral sequence, on cohomology. Under
the identification of the first page with the cohomology of the graded pieces, the entry of the
differential from pq to pq' between a generator x of index q + 1 and a generator y of
index q is the action of m x y on the cohomology of ℳ. The indices are given with equations,
as in indexSpectralSequenceFirstPageXIsoOfEq.
The first differential of the index spectral sequence is the classical differential: under
the identifications of the first page with the products of the cohomology of ℳ
(indexSpectralSequenceFirstPageXIsoOfEq followed by indexGradedPieceHomologyIso), the
differential from pq to pq' is indexClassicalD.
The short complex of the first page around (a, b) is isomorphic to the short complex of the
classical complex around degree b + 1: the isomorphism is the identification of each first-page
term with a product of cohomology groups, which intertwines the differentials
(secondPage_square).
Instances For
The first component of indexSecondPageShortComplexIso: the first-page term at
(a - 2, b + 1) is identified with the product of cohomology groups of ℳ (the term of the
classical complex being identified by indexClassicalComplexXIso).
The first component of indexSecondPageShortComplexIso: the first-page term at
(a - 2, b + 1) is identified with the product of cohomology groups of ℳ (the term of the
classical complex being identified by indexClassicalComplexXIso).
The second component of indexSecondPageShortComplexIso: the first-page term at (a, b) is
identified with the product of cohomology groups of ℳ (the term of the classical complex being
identified by indexClassicalComplexXIso).
The second component of indexSecondPageShortComplexIso: the first-page term at (a, b) is
identified with the product of cohomology groups of ℳ (the term of the classical complex being
identified by indexClassicalComplexXIso).
The third component of indexSecondPageShortComplexIso: the first-page term at
(a + 2, b - 1) is identified with the product of cohomology groups of ℳ (the term of the
classical complex being identified by indexClassicalComplexXIso).
The third component of indexSecondPageShortComplexIso: the first-page term at
(a + 2, b - 1) is identified with the product of cohomology groups of ℳ (the term of the
classical complex being identified by indexClassicalComplexXIso).
The second page of the index spectral sequence is the cohomology of the classical complex
(BDHO, Definition 3.38 and Ch. 3 §4.2): the object at (a, b) of the page 3 of the index
spectral sequence (the classical E₂ page, in Mathlib's numbering of pages) is the homology in
degree b + 1 of the classical complex in coefficient degree a + 2 * b + 1. It is the
homology of the first page at (a, b), identified with the homology of the classical complex by
indexSecondPageShortComplexIso (see indexSpectralSequenceSecondPageXIso_eq).
Instances For
The second-page isomorphism is the inverse of the identification of the second page with the
homology of the first page, followed by the homology isomorphism of
indexSecondPageShortComplexIso.