The action of a cycle of degree zero on the cohomology of a shifted module complex #
A cycle a of degree zero of the algebra acts on a differential graded right module ℳ by
x ↦ x · a, which commutes with the differential. Composed with the Koszul sign, it is a
morphism of complexes from shiftedModuleComplex hM (q + 1) to the shift by one of
shiftedModuleComplex hM q (TauCeti.shiftedModuleComplexAct), hence induces a map on cohomology
(TauCeti.shiftedModuleComplexActHomology), which sends the class of α to the class of
op a • ε α, with ε the Koszul sign.
Main definitions #
TauCeti.shiftedModuleComplexAct: the action of a cycle of degree zero, as a morphism of complexes.TauCeti.shiftedModuleComplexActHomology: the induced map on cohomology.
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.shiftedModuleComplexActX
{R : Type uR}
{A : Type uA}
{M : Type uM}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower 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 ℤ) ℳ]
(hM : IsDGRightModule h ℳ dM)
{a : A}
(ha : a ∈ 𝒜 0)
(q n : ℤ)
:
The right action of an element a of degree zero of the algebra, twisted by the Koszul sign,
from the degree-n term of shiftedModuleComplex hM (q + 1) to the degree-(n + 1) term of
shiftedModuleComplex hM q: both are the piece of ℳ of degree n + q + 1.
Instances For
@[simp]
theorem
TauCeti.shiftedModuleComplexXEquiv_shiftedModuleComplexActX
{R : Type uR}
{A : Type uA}
{M : Type uM}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower 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 ℤ) ℳ]
(hM : IsDGRightModule h ℳ dM)
{a : A}
(ha : a ∈ 𝒜 0)
(q n : ℤ)
(α : ↑((shiftedModuleComplex hM (q + 1)).X n))
:
↑((shiftedModuleComplexXEquiv hM q (n + 1)) ((shiftedModuleComplexActX hM ha q n) α)) = MulOpposite.op a • ((InternalGrading.ofDecomposition ℳ).koszulTwist 1) ↑((shiftedModuleComplexXEquiv hM (q + 1) n) α)
noncomputable def
TauCeti.shiftedModuleComplexAct
{R : Type uR}
{A : Type uA}
{M : Type uM}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower 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 ℤ) ℳ]
(hM : IsDGRightModule h ℳ dM)
{a : A}
(ha : a ∈ 𝒜 0)
(hda : d a = 0)
(q : ℤ)
:
The right action of a cycle of degree zero, twisted by the Koszul sign, as a morphism of
complexes from shiftedModuleComplex hM (q + 1) to the shift by one of
shiftedModuleComplex hM q: it anticommutes with dM, as the shift requires.
Instances For
@[simp]
theorem
TauCeti.shiftedModuleComplexAct_f
{R : Type uR}
{A : Type uA}
{M : Type uM}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower 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 ℤ) ℳ]
(hM : IsDGRightModule h ℳ dM)
{a : A}
(ha : a ∈ 𝒜 0)
(hda : d a = 0)
(q n : ℤ)
:
The components of shiftedModuleComplexAct are the linear maps shiftedModuleComplexActX.
noncomputable def
TauCeti.shiftedModuleComplexActHomology
{R : Type uR}
{A : Type uA}
{M : Type uM}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower 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 ℤ) ℳ]
(hM : IsDGRightModule h ℳ dM)
{a : A}
(ha : a ∈ 𝒜 0)
(hda : d a = 0)
(q n n' : ℤ)
(hn : 1 + n = n')
:
HomologicalComplex.homology (shiftedModuleComplex hM (q + 1)) n ⟶ HomologicalComplex.homology (shiftedModuleComplex hM q) n'
The action of a cycle of degree zero on cohomology: the map
H^n(shiftedModuleComplex hM (q + 1)) ⟶ H^{n + 1}(shiftedModuleComplex hM q) induced by
shiftedModuleComplexAct, both being the cohomology of ℳ in degree n + q + 1.
Instances For
theorem
TauCeti.shiftedModuleComplexActHomology_homologyπ
{R : Type uR}
{A : Type uA}
{M : Type uM}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower 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 ℤ) ℳ]
(hM : IsDGRightModule h ℳ dM)
{a : A}
(ha : a ∈ 𝒜 0)
(hda : d a = 0)
(q n n' : ℤ)
(hn : 1 + n = n')
(α : ↑((shiftedModuleComplex hM (q + 1)).X n))
(hα : (ModuleCat.Hom.hom ((shiftedModuleComplex hM (q + 1)).d n (n + 1))) α = 0)
(β : ↑((shiftedModuleComplex hM q).X n'))
(hβ :
↑((shiftedModuleComplexXEquiv hM q n') β) = MulOpposite.op a • ((InternalGrading.ofDecomposition ℳ).koszulTwist 1) ↑((shiftedModuleComplexXEquiv hM (q + 1) n) α))
(hβ' : (ModuleCat.Hom.hom ((shiftedModuleComplex hM q).d n' (n' + 1))) β = 0)
:
(ModuleCat.Hom.hom (shiftedModuleComplexActHomology hM ha hda q n n' hn))
((ModuleCat.Hom.hom (HomologicalComplex.homologyπ (shiftedModuleComplex hM (q + 1)) n))
(HomologicalComplex.moduleCatCyclesMk (shiftedModuleComplex hM (q + 1)) α (n + 1) ⋯ hα)) = (ModuleCat.Hom.hom (HomologicalComplex.homologyπ (shiftedModuleComplex hM q) n'))
(HomologicalComplex.moduleCatCyclesMk (shiftedModuleComplex hM q) β (n' + 1) ⋯ hβ')
The action of a cycle of degree zero on cohomology, on classes: it sends the class of α to
the class of op a • ε α, with ε the Koszul sign.
theorem
TauCeti.exists_shiftedModuleComplexActHomology_homologyπ
{R : Type uR}
{A : Type uA}
{M : Type uM}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
[Module Aᵐᵒᵖ M]
[IsScalarTower 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 ℤ) ℳ]
(hM : IsDGRightModule h ℳ dM)
{a : A}
(ha : a ∈ 𝒜 0)
(hda : d a = 0)
(q n n' : ℤ)
(hn : 1 + n = n')
(α : ↑((shiftedModuleComplex hM (q + 1)).X n))
(hα : (ModuleCat.Hom.hom ((shiftedModuleComplex hM (q + 1)).d n (n + 1))) α = 0)
:
∃ (β : ↑((shiftedModuleComplex hM q).X n')) (hβ' :
(ModuleCat.Hom.hom ((shiftedModuleComplex hM q).d n' (n' + 1))) β = 0),
↑((shiftedModuleComplexXEquiv hM q n') β) = MulOpposite.op a • ((InternalGrading.ofDecomposition ℳ).koszulTwist 1) ↑((shiftedModuleComplexXEquiv hM (q + 1) n) α) ∧ (ModuleCat.Hom.hom (shiftedModuleComplexActHomology hM ha hda q n n' hn))
((ModuleCat.Hom.hom (HomologicalComplex.homologyπ (shiftedModuleComplex hM (q + 1)) n))
(HomologicalComplex.moduleCatCyclesMk (shiftedModuleComplex hM (q + 1)) α (n + 1) ⋯ hα)) = (ModuleCat.Hom.hom (HomologicalComplex.homologyπ (shiftedModuleComplex hM q) n'))
(HomologicalComplex.moduleCatCyclesMk (shiftedModuleComplex hM q) β (n' + 1) ⋯ hβ')
The action of a cycle of degree zero on cohomology sends the class of α to the class of an
element whose value is op a • ε α, with ε the Koszul sign.