The cohomology of a graded piece of the index filtration #
The p-th graded piece ⊕_{ind x = p} ℳ ⊗ ⟨x⟩ of the index filtration of a twisted complex is
the twisted complex of the zero cocycle on the generators of index p
(TauCeti.indexGradedPieceComplex). It carries the differential dM on every component, so its
cohomology splits as a product over the generators of index p of the cohomology of ℳ, shifted
by p: in total degree n, the component of a generator x lies in ℳ (n + p).
The shifted complex is TauCeti.shiftedModuleComplex hM p, whose degree-n term is ℳ (n + p),
lifted to the universe of the twisted complex. The splitting is assembled from the chain maps
evaluating a family at a generator (TauCeti.indexGradedPieceEval) and inserting an element at a
generator (TauCeti.indexGradedPieceSingle), which are inverse to each other up to the sum over
the generators.
Main definitions #
TauCeti.shiftedModuleComplex hM p: the complexℳ, reindexed so that its degree-nterm isℳ (n + p).TauCeti.indexGradedPieceComplex hM ind p: the twisted complex of the zero cocycle on the generators of indexp.TauCeti.indexGradedPieceHomologyIso: the cohomology of thep-th graded piece is the product over the generators of indexpof the cohomology ofshiftedModuleComplex hM p.
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.shiftedModuleComplex
{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)
(p : ℤ)
:
CochainComplex (ModuleCat R) ℤ
The complex of a differential graded right module, reindexed so that its degree-n term is
ℳ (n + p), and lifted to a universe containing uP.
Instances For
noncomputable def
TauCeti.shiftedModuleComplexXEquiv
{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)
(p n : ℤ)
:
The degree-n term of shiftedModuleComplex hM p is ℳ (n + p).
Instances For
theorem
TauCeti.shiftedModuleComplexXEquiv_d
{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)
(p n : ℤ)
(x : ↑((shiftedModuleComplex hM p).X n))
:
↑((shiftedModuleComplexXEquiv hM p (n + 1)) ((ModuleCat.Hom.hom ((shiftedModuleComplex hM p).d n (n + 1))) x)) = dM ↑((shiftedModuleComplexXEquiv hM p n) x)
The differential of shiftedModuleComplex hM p is dM.
theorem
TauCeti.shiftedModuleComplexXEquiv_mem
{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)
{p n j : ℤ}
(hj : j = n + p)
(α : ↑((shiftedModuleComplex hM p).X n))
:
The value of an element of degree n of shiftedModuleComplex hM p lies in ℳ j for every
j = n + p.
theorem
TauCeti.shiftedModuleComplexXEquiv_XIsoOfEq_hom
{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)
(p i j : ℤ)
(hij : i = j)
(z : ↑((shiftedModuleComplex hM p).X i))
:
↑((shiftedModuleComplexXEquiv hM p j)
((ModuleCat.Hom.hom (HomologicalComplex.XIsoOfEq (shiftedModuleComplex hM p) hij).hom) z)) = ↑((shiftedModuleComplexXEquiv hM p i) z)
Transport along an equality of degrees does not change the underlying element of ℳ.
theorem
TauCeti.shiftedModuleComplexXEquiv_d_eq_zero_iff
{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)
(p n : ℤ)
(α : ↑((shiftedModuleComplex hM p).X n))
:
(ModuleCat.Hom.hom ((shiftedModuleComplex hM p).d n (n + 1))) α = 0 ↔ dM ↑((shiftedModuleComplexXEquiv hM p n) α) = 0
A cycle of shiftedModuleComplex hM p is a cycle of ℳ.
theorem
TauCeti.shiftedModuleComplex_homologyπ_eq_zero
{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)
(p n : ℤ)
(α : ↑((shiftedModuleComplex hM p).X n))
(hα : (ModuleCat.Hom.hom ((shiftedModuleComplex hM p).d n (n + 1))) α = 0)
(b : ↑((shiftedModuleComplex hM p).X (n - 1)))
(hb : ↑((shiftedModuleComplexXEquiv hM p n) α) = dM ↑((shiftedModuleComplexXEquiv hM p (n - 1)) b))
:
(ModuleCat.Hom.hom (HomologicalComplex.homologyπ (shiftedModuleComplex hM p) n))
(HomologicalComplex.moduleCatCyclesMk (shiftedModuleComplex hM p) α (n + 1) ⋯ hα) = 0
The class of an element of shiftedModuleComplex hM p whose value is dM of a value of the
previous degree vanishes.
@[reducible, inline]
noncomputable abbrev
TauCeti.indexGradedPieceComplex
{R : Type uR}
{A : Type uA}
{M : Type uM}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
{P : Type uP}
[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 ℤ) ℳ]
(hM : IsDGRightModule h ℳ dM)
(ind : P → ℤ)
(p : ℤ)
:
CochainComplex (ModuleCat R) ℤ
The twisted complex of the zero cocycle on the generators of index p, that is
⊕_{ind x = p} ℳ ⊗ ⟨x⟩ with the differential dM applied to every component. It is the graded
piece F_p / F_{p-1} of the index filtration.
Instances For
@[reducible, inline]
noncomputable abbrev
TauCeti.indexGradedPieceComplexXEquiv
{R : Type uR}
{A : Type uA}
{M : Type uM}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
{P : Type uP}
[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 ℤ) ℳ]
(hM : IsDGRightModule h ℳ dM)
(ind : P → ℤ)
(p n : ℤ)
:
↑((indexGradedPieceComplex hM ind p).X n) ≃ₗ[R] ↥(twistedTotalGrading ℳ (fun (x : { x : P // ind x = p }) => ind ↑x) n)
The degree-n term of indexGradedPieceComplex hM ind p is the module of families of total
degree n indexed by the generators of index p.
Instances For
theorem
TauCeti.indexGradedPieceComplexXEquiv_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}
[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 ℤ) ℳ]
(hM : IsDGRightModule h ℳ dM)
(ind : P → ℤ)
(p n : ℤ)
(f : ↑((indexGradedPieceComplex hM ind p).X n))
(x : { x : P // ind x = p })
:
↑((indexGradedPieceComplexXEquiv hM ind p (n + 1))
((ModuleCat.Hom.hom ((indexGradedPieceComplex hM ind p).d n (n + 1))) f))
x = dM (↑((indexGradedPieceComplexXEquiv hM ind p n) f) x)
The differential of indexGradedPieceComplex hM ind p is dM, applied to every component.
noncomputable def
TauCeti.indexGradedPieceEvalX
{R : Type uR}
{A : Type uA}
{M : Type uM}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
{P : Type uP}
[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 ℤ) ℳ]
(hM : IsDGRightModule h ℳ dM)
(ind : P → ℤ)
{p : ℤ}
(x : { x : P // ind x = p })
(n : ℤ)
:
The evaluation at a generator x of index p, from the degree-n term of the p-th graded
piece to ℳ (n + p).
Instances For
@[simp]
theorem
TauCeti.shiftedModuleComplexXEquiv_indexGradedPieceEvalX
{R : Type uR}
{A : Type uA}
{M : Type uM}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
{P : Type uP}
[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 ℤ) ℳ]
(hM : IsDGRightModule h ℳ dM)
(ind : P → ℤ)
{p : ℤ}
(x : { x : P // ind x = p })
(n : ℤ)
(f : ↑((indexGradedPieceComplex hM ind p).X n))
:
↑((shiftedModuleComplexXEquiv hM p n) ((indexGradedPieceEvalX hM ind x n) f)) = ↑((indexGradedPieceComplexXEquiv hM ind p n) f) x
indexGradedPieceEvalX evaluates the underlying family at x.
noncomputable def
TauCeti.indexGradedPieceEval
{R : Type uR}
{A : Type uA}
{M : Type uM}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
{P : Type uP}
[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 ℤ) ℳ]
(hM : IsDGRightModule h ℳ dM)
(ind : P → ℤ)
{p : ℤ}
(x : { x : P // ind x = p })
:
The evaluation at a generator x of index p, as a morphism of complexes from the p-th
graded piece to shiftedModuleComplex hM p.
Instances For
@[simp]
theorem
TauCeti.shiftedModuleComplexXEquiv_indexGradedPieceEval_f
{R : Type uR}
{A : Type uA}
{M : Type uM}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
{P : Type uP}
[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 ℤ) ℳ]
(hM : IsDGRightModule h ℳ dM)
(ind : P → ℤ)
{p : ℤ}
(x : { x : P // ind x = p })
(n : ℤ)
(f : ↑((indexGradedPieceComplex hM ind p).X n))
:
↑((shiftedModuleComplexXEquiv hM p n) ((ModuleCat.Hom.hom ((indexGradedPieceEval hM ind x).f n)) f)) = ↑((indexGradedPieceComplexXEquiv hM ind p n) f) x
indexGradedPieceEval evaluates the underlying family at x.
noncomputable def
TauCeti.indexGradedPieceSingleX
{R : Type uR}
{A : Type uA}
{M : Type uM}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
{P : Type uP}
[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 ℤ) ℳ]
(hM : IsDGRightModule h ℳ dM)
(ind : P → ℤ)
{p : ℤ}
[DecidableEq P]
(x : { x : P // ind x = p })
(n : ℤ)
:
The insertion at a generator x of index p, from ℳ (n + p) to the degree-n term of the
p-th graded piece.
Instances For
@[simp]
theorem
TauCeti.indexGradedPieceComplexXEquiv_indexGradedPieceSingleX
{R : Type uR}
{A : Type uA}
{M : Type uM}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
{P : Type uP}
[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 ℤ) ℳ]
(hM : IsDGRightModule h ℳ dM)
(ind : P → ℤ)
{p : ℤ}
[DecidableEq P]
(x : { x : P // ind x = p })
(n : ℤ)
(α : ↑((shiftedModuleComplex hM p).X n))
:
↑((indexGradedPieceComplexXEquiv hM ind p n) ((indexGradedPieceSingleX hM ind x n) α)) = Pi.single x ↑((shiftedModuleComplexXEquiv hM p n) α)
indexGradedPieceSingleX inserts an element at x.
noncomputable def
TauCeti.indexGradedPieceSingle
{R : Type uR}
{A : Type uA}
{M : Type uM}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
{P : Type uP}
[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 ℤ) ℳ]
(hM : IsDGRightModule h ℳ dM)
(ind : P → ℤ)
{p : ℤ}
[DecidableEq P]
(x : { x : P // ind x = p })
:
The insertion at a generator x of index p, as a morphism of complexes from
shiftedModuleComplex hM p to the p-th graded piece.
Instances For
@[simp]
theorem
TauCeti.indexGradedPieceComplexXEquiv_indexGradedPieceSingle_f
{R : Type uR}
{A : Type uA}
{M : Type uM}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
{P : Type uP}
[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 ℤ) ℳ]
(hM : IsDGRightModule h ℳ dM)
(ind : P → ℤ)
{p : ℤ}
[DecidableEq P]
(x : { x : P // ind x = p })
(n : ℤ)
(α : ↑((shiftedModuleComplex hM p).X n))
:
↑((indexGradedPieceComplexXEquiv hM ind p n) ((ModuleCat.Hom.hom ((indexGradedPieceSingle hM ind x).f n)) α)) = Pi.single x ↑((shiftedModuleComplexXEquiv hM p n) α)
indexGradedPieceSingle inserts an element at x.
@[simp]
theorem
TauCeti.indexGradedPieceSingle_comp_eval
{R : Type uR}
{A : Type uA}
{M : Type uM}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
{P : Type uP}
[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 ℤ) ℳ]
(hM : IsDGRightModule h ℳ dM)
(ind : P → ℤ)
{p : ℤ}
[DecidableEq P]
(x y : { x : P // ind x = p })
:
CategoryTheory.CategoryStruct.comp (indexGradedPieceSingle hM ind x) (indexGradedPieceEval hM ind y) = if x = y then CategoryTheory.CategoryStruct.id (shiftedModuleComplex hM p) else 0
Inserting at x and evaluating at y is the identity when x = y and zero otherwise.
@[simp]
theorem
TauCeti.indexGradedPieceSingle_comp_eval_assoc
{R : Type uR}
{A : Type uA}
{M : Type uM}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
{P : Type uP}
[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 ℤ) ℳ]
(hM : IsDGRightModule h ℳ dM)
(ind : P → ℤ)
{p : ℤ}
[DecidableEq P]
(x y : { x : P // ind x = p })
{Z : CochainComplex (ModuleCat R) ℤ}
(h✝ : shiftedModuleComplex hM p ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (indexGradedPieceSingle hM ind x)
(CategoryTheory.CategoryStruct.comp (indexGradedPieceEval hM ind y) h✝) = CategoryTheory.CategoryStruct.comp (if x = y then CategoryTheory.CategoryStruct.id (shiftedModuleComplex hM p) else 0)
h✝
Inserting at x and evaluating at y is the identity when x = y and zero otherwise.
@[simp]
theorem
TauCeti.sum_indexGradedPieceEval_comp_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}
[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 ℤ) ℳ]
(hM : IsDGRightModule h ℳ dM)
(ind : P → ℤ)
{p : ℤ}
[DecidableEq P]
:
∑ x : { x : P // ind x = p },
CategoryTheory.CategoryStruct.comp (indexGradedPieceEval hM ind x) (indexGradedPieceSingle hM ind x) = CategoryTheory.CategoryStruct.id (indexGradedPieceComplex hM ind p)
The sum over the generators of index p of evaluating and inserting is the identity of the
p-th graded piece.
noncomputable def
TauCeti.indexGradedPieceHomologyIso
{R : Type uR}
{A : Type uA}
{M : Type uM}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
{P : Type uP}
[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 ℤ) ℳ]
(hM : IsDGRightModule h ℳ dM)
(ind : P → ℤ)
{p : ℤ}
[DecidableEq P]
(n : ℤ)
:
HomologicalComplex.homology (indexGradedPieceComplex hM ind p) n ≅ ∏ᶜ fun (x : { x : P // ind x = p }) => HomologicalComplex.homology (shiftedModuleComplex hM p) n
The cohomology of a graded piece of the index filtration: the cohomology of
⊕_{ind x = p} ℳ ⊗ ⟨x⟩ in total degree n is the product over the generators x of index p
of the cohomology of shiftedModuleComplex hM p in degree n, that is of ℳ in degree
n + p, through the evaluations and insertions at the generators.
Instances For
@[simp]
theorem
TauCeti.indexGradedPieceHomologyIso_hom_π
{R : Type uR}
{A : Type uA}
{M : Type uM}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
{P : Type uP}
[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 ℤ) ℳ]
(hM : IsDGRightModule h ℳ dM)
(ind : P → ℤ)
{p : ℤ}
[DecidableEq P]
(n : ℤ)
(x : { x : P // ind x = p })
:
CategoryTheory.CategoryStruct.comp (indexGradedPieceHomologyIso hM ind n).hom
(CategoryTheory.Limits.Pi.π
(fun (x : { x : P // ind x = p }) => HomologicalComplex.homology (shiftedModuleComplex hM p) n) x) = HomologicalComplex.homologyMap (indexGradedPieceEval hM ind x) n
The component at a generator x of indexGradedPieceHomologyIso is the map in cohomology of
the evaluation at x.
@[simp]
theorem
TauCeti.indexGradedPieceHomologyIso_hom_π_assoc
{R : Type uR}
{A : Type uA}
{M : Type uM}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
{P : Type uP}
[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 ℤ) ℳ]
(hM : IsDGRightModule h ℳ dM)
(ind : P → ℤ)
{p : ℤ}
[DecidableEq P]
(n : ℤ)
(x : { x : P // ind x = p })
{Z : ModuleCat R}
(h✝ : HomologicalComplex.homology (shiftedModuleComplex hM p) n ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (indexGradedPieceHomologyIso hM ind n).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.Pi.π
(fun (x : { x : P // ind x = p }) => HomologicalComplex.homology (shiftedModuleComplex hM p) n) x)
h✝) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (indexGradedPieceEval hM ind x) n) h✝
The component at a generator x of indexGradedPieceHomologyIso is the map in cohomology of
the evaluation at x.
theorem
TauCeti.indexGradedPieceHomologyIso_inv
{R : Type uR}
{A : Type uA}
{M : Type uM}
[CommRing R]
[Ring A]
[Algebra R A]
[AddCommGroup M]
[Module R M]
{P : Type uP}
[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 ℤ) ℳ]
(hM : IsDGRightModule h ℳ dM)
(ind : P → ℤ)
{p : ℤ}
[DecidableEq P]
(n : ℤ)
:
(indexGradedPieceHomologyIso hM ind n).inv = ∑ x : { x : P // ind x = p },
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.Pi.π
(fun (x : { x : P // ind x = p }) => HomologicalComplex.homology (shiftedModuleComplex hM p) n) x)
(HomologicalComplex.homologyMap (indexGradedPieceSingle hM ind x) n)
The inverse of indexGradedPieceHomologyIso is the sum of the maps in cohomology of the
insertions at the generators.