The first differential of the index spectral sequence

On the first page of the index spectral sequence of a twisted complex (page 2 in Mathlib's numbering), the object at (p, q) is the cohomology in degree p + q of the graded piece ⊕_{ind x = q + 1} ℳ ⊗ ⟨x⟩ (TauCeti.TwistingCocycle.indexSpectralSequenceFirstPageXIso). This file computes the differential of that page: it sends the class of a cycle f to the class of TauCeti.TwistingCocycle.indexGradedPieceD1X f, that is of the restriction of its twisted differential to the generators of index q, the entries m x y with ind x - ind y = 1 of the twisting cocycle.

The entries m x y with ind x - ind y = 1 are cycles of degree zero of the algebra (the twisting equation has no intermediate generators), so this is the action of their classes on the cohomology of ℳ. The identification of the cohomology of TauCeti.shiftedModuleComplex with the graded pieces of TauCeti.IsDGRightModule.Cohomology, through which this action is the module structure of H(ℳ) over H(𝒜), is not made here.

Main definitions

• TauCeti.TwistingCocycle.twistedIndexCokernelIsoOfEq and TauCeti.TwistingCocycle.indexSpectralSequenceFirstPageXIsoOfEq: the identification of the first page with the cohomology of the graded pieces, with the indices given by equations.

Main results

• TauCeti.TwistingCocycle.indexSpectralSequence_page_two_d_apply: the differential of the first page of the index spectral sequence.
• TauCeti.TwistingCocycle.homologyMap_indexGradedPieceEval_page_two_d: its entries under the splitting of TauCeti.indexGradedPieceHomologyIso, between a generator x of index b + 1 and a generator y of index b, are induced by α ↦ α · m x y up to the Koszul sign.

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.

theorem TauCeti.TwistingCocycle.indexSpectralSequence_page_two_d_apply {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {P : Type uP} {ind : P → ℤ} [Fintype P] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] {dM : M →ₗ[R] M} {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) (hM : IsDGRightModule h ℳ dM) (a b : ℤ) (f : ↑((indexGradedPieceComplex hM ind (b + 1)).X (a + b))) (hf : (ModuleCat.Hom.hom ((indexGradedPieceComplex hM ind (b + 1)).d (a + b) (a + b + 1))) f = 0) : (CategoryTheory.ConcreteCategory.hom (m.indexSpectralSequenceFirstPageXIsoOfEq dM hM (a + 2, b - 1) (b - 1) b ⋯ ⋯ (a + b + 1) ⋯).hom) ((ModuleCat.Hom.hom (((indexSpectralSequence dM m hM).page 2 indexSpectralSequence_page_two_d_apply._proof_3).d (a, b) (a + 2, b - 1))) ((CategoryTheory.ConcreteCategory.hom (m.indexSpectralSequenceFirstPageXIsoOfEq dM hM (a, b) b (b + 1) ⋯ ⋯ (a + b) ⋯).inv) ((ModuleCat.Hom.hom (HomologicalComplex.homologyπ (indexGradedPieceComplex hM ind (b + 1)) (a + b))) (HomologicalComplex.moduleCatCyclesMk (indexGradedPieceComplex hM ind (b + 1)) f (a + b + 1) ⋯ hf)))) = (ModuleCat.Hom.hom (HomologicalComplex.homologyπ (indexGradedPieceComplex hM ind b) (a + b + 1))) (HomologicalComplex.moduleCatCyclesMk (indexGradedPieceComplex hM ind b) ((m.indexGradedPieceD1X hM b (b + 1) (a + b)) f) (a + b + 1 + 1) ⋯ ⋯)

The first differential of the index spectral sequence. On the first page (page 2 in Mathlib's numbering), the differential from (a, b) to (a + 2, b - 1) sends the class of a cycle f of the graded piece of the generators of index b + 1 to the class of the restriction of the twisted differential of f, extended by zero, to the generators of index b.

theorem TauCeti.TwistingCocycle.homologyMap_indexGradedPieceEval_page_two_d {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] {P : Type uP} {ind : P → ℤ} [Fintype P] [Module Aᵐᵒᵖ M] [IsScalarTower R Aᵐᵒᵖ M] [SMulCommClass R Aᵐᵒᵖ M] {ℳ : ℤ → Submodule R M} [DirectSum.Decomposition ℳ] {dM : M →ₗ[R] M} {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} [SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ] (m : TwistingCocycle 𝒜 d P ind) (hM : IsDGRightModule h ℳ dM) [DecidableEq P] {b : ℤ} (x : { x : P // ind x = b + 1 }) (y : { y : P // ind y = b }) (a : ℤ) (α : ↑((shiftedModuleComplex hM (b + 1)).X (a + b))) (hα : (ModuleCat.Hom.hom ((shiftedModuleComplex hM (b + 1)).d (a + b) (a + b + 1))) α = 0) : (ModuleCat.Hom.hom (HomologicalComplex.homologyMap (indexGradedPieceEval hM ind y) (a + b + 1))) ((CategoryTheory.ConcreteCategory.hom (m.indexSpectralSequenceFirstPageXIsoOfEq dM hM (a + 2, b - 1) (b - 1) b ⋯ ⋯ (a + b + 1) ⋯).hom) ((ModuleCat.Hom.hom (((indexSpectralSequence dM m hM).page 2 indexSpectralSequence_page_two_d_apply._proof_3).d (a, b) (a + 2, b - 1))) ((CategoryTheory.ConcreteCategory.hom (m.indexSpectralSequenceFirstPageXIsoOfEq dM hM (a, b) b (b + 1) ⋯ ⋯ (a + b) ⋯).inv) ((ModuleCat.Hom.hom (HomologicalComplex.homologyMap (indexGradedPieceSingle hM ind x) (a + b))) ((ModuleCat.Hom.hom (HomologicalComplex.homologyπ (shiftedModuleComplex hM (b + 1)) (a + b))) (HomologicalComplex.moduleCatCyclesMk (shiftedModuleComplex hM (b + 1)) α (a + b + 1) ⋯ hα)))))) = (ModuleCat.Hom.hom (HomologicalComplex.homologyπ (shiftedModuleComplex hM b) (a + b + 1))) (HomologicalComplex.moduleCatCyclesMk (shiftedModuleComplex hM b) ((ModuleCat.Hom.hom ((indexGradedPieceEval hM ind y).f (a + b + 1))) ((m.indexGradedPieceD1X hM b (b + 1) (a + b)) ((ModuleCat.Hom.hom ((indexGradedPieceSingle hM ind x).f (a + b))) α))) (a + b + 1 + 1) ⋯ ⋯)

The entries of the first differential of the index spectral sequence. Under the splitting of the first page into the cohomology of ℳ (indexGradedPieceHomologyIso), the entry of the differential from (a, b) to (a + 2, b - 1) between a generator x of index b + 1 and a generator y of index b sends the class of a cycle α to the class of α · m x y, up to the Koszul sign (shiftedModuleComplexXEquiv_indexGradedPieceEval_D1X_single).