The differential between two graded pieces of the index filtration

The twisted differential of a family supported on the generators of index p has components at the generators of index at most p: at index p it is dM, and only the twisting contribution strictly lowers the index, because the twisting cocycle is one-sided. Restricting it to the generators of index q gives a map from the graded piece of index p to that of index q (TauCeti.TwistingCocycle.indexGradedPieceD1X). For q + 1 = p it sends cycles to cycles: on a cycle of the graded piece of index p the component at index p vanishes, so the full differential lies in the filtration stage of index q. Its component between a generator x of index b + 1 and a generator y of index b is α ↦ α · m x y, up to the Koszul sign.

Main definitions

• TauCeti.TwistingCocycle.indexGradedPieceD1X: the restriction of the twisted differential from the graded piece of index p to that of index q.

Main results

• TauCeti.TwistingCocycle.d_indexGradedPieceD1X: for q + 1 = p, it sends cycles to cycles.
• TauCeti.TwistingCocycle.shiftedModuleComplexXEquiv_indexGradedPieceEval_D1X_single: its entries under the splitting of TauCeti.indexGradedPieceHomologyIso.

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.

noncomputable def TauCeti.TwistingCocycle.indexGradedPieceD1X {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) (q p n : ℤ) : ↑((indexGradedPieceComplex hM ind p).X n) →ₗ[R] ↑((indexGradedPieceComplex hM ind q).X (n + 1))

The restriction to the generators of index q of the twisted differential, from the degree-n term of the graded piece of index p to the degree-(n + 1) term of that of index q.

@[simp]

theorem TauCeti.TwistingCocycle.indexGradedPieceComplexXEquiv_indexGradedPieceD1X {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) (q p n : ℤ) (f : ↑((indexGradedPieceComplex hM ind p).X n)) : ↑((indexGradedPieceComplexXEquiv hM ind q (n + 1)) ((m.indexGradedPieceD1X hM q p n) f)) = (LinearMap.funLeft R M Subtype.val) ((twistedDifferential m.m ℳ dM) ((indexExtend R M ind p) ↑((indexGradedPieceComplexXEquiv hM ind p n) f)))

indexGradedPieceD1X restricts the twisted differential of the family extended by zero to the generators of index q.

theorem TauCeti.TwistingCocycle.twistedDifferential_indexExtend_eq_zero {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) (q p : ℤ) (hqp : q + 1 = p) (n : ℤ) (f : ↑((indexGradedPieceComplex hM ind p).X n)) (hf : (ModuleCat.Hom.hom ((indexGradedPieceComplex hM ind p).d n (n + 1))) f = 0) (y : P) : q < ind y → (twistedDifferential m.m ℳ dM) ((indexExtend R M ind p) ↑((indexGradedPieceComplexXEquiv hM ind p n) f)) y = 0

The twisted differential of a cycle of the graded piece of index p = q + 1, extended by zero, vanishes at the generators of index greater than q.

theorem TauCeti.TwistingCocycle.d_indexGradedPieceD1X {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) (q p : ℤ) (hqp : q + 1 = p) (n : ℤ) (f : ↑((indexGradedPieceComplex hM ind p).X n)) (hf : (ModuleCat.Hom.hom ((indexGradedPieceComplex hM ind p).d n (n + 1))) f = 0) : (ModuleCat.Hom.hom ((indexGradedPieceComplex hM ind q).d (n + 1) (n + 1 + 1))) ((m.indexGradedPieceD1X hM q p n) f) = 0

The restriction of the twisted differential sends the cycles of the graded piece of index p = q + 1 to cycles of the graded piece of index q.

theorem TauCeti.TwistingCocycle.shiftedModuleComplexXEquiv_indexGradedPieceEval_D1X_single {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 }) (n : ℤ) (α : ↑((shiftedModuleComplex hM (b + 1)).X n)) : ↑((shiftedModuleComplexXEquiv hM b (n + 1)) ((ModuleCat.Hom.hom ((indexGradedPieceEval hM ind y).f (n + 1))) ((m.indexGradedPieceD1X hM b (b + 1) n) ((ModuleCat.Hom.hom ((indexGradedPieceSingle hM ind x).f n)) α)))) = MulOpposite.op (m.m ↑x ↑y) • ((InternalGrading.ofDecomposition ℳ).koszulTwist 1) ↑((shiftedModuleComplexXEquiv hM (b + 1) n) α)

The entries of the first differential, on chains: inserting α at a generator x of index b + 1, restricting the twisted differential to the generators of index b and evaluating at such a generator y gives α · m x y, up to the Koszul sign.