The first page of the twisted index filtration #
The canonical index filtration of the twisted cochain complex has graded pieces given by the
zero twisting cocycle on generators of a fixed index. The projection and short exact sequence
are constructed in Twisted.Filtration. Their cokernel identifies the first page of the filtered
spectral sequence with the cohomology of that zero-cocycle complex.
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 4.
@[reducible, inline]
noncomputable abbrev
TauCeti.TwistingCocycle.twistedIndexFiltrationFunctor
{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]
{ind : P → ℤ}
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[SMulCommClass R Aᵐᵒᵖ M]
{ℳ : ℤ → Submodule R M}
[DirectSum.Decomposition ℳ]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
[SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ]
(m : TwistingCocycle 𝒜 d P ind)
(dM : M →ₗ[R] M)
(hM : IsDGRightModule h ℳ dM)
:
The canonical index filtration, extended to EInt by zero and the whole complex.
Instances For
The first page of the index spectral sequence #
noncomputable def
TauCeti.TwistingCocycle.twistedIndexFiltrationFunctorObjIso
{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]
{ind : P → ℤ}
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[SMulCommClass R Aᵐᵒᵖ M]
{ℳ : ℤ → Submodule R M}
[DirectSum.Decomposition ℳ]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
[SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ]
(m : TwistingCocycle 𝒜 d P ind)
(dM : M →ₗ[R] M)
(hM : IsDGRightModule h ℳ dM)
(p : ℤ)
:
The step p of twistedIndexFiltrationFunctor is the subcomplex F_p.
Instances For
@[simp]
theorem
TauCeti.TwistingCocycle.twistedIndexFiltrationFunctorObjIso_hom_comp_indexFiltrationι
{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]
{ind : P → ℤ}
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[SMulCommClass R Aᵐᵒᵖ M]
{ℳ : ℤ → Submodule R M}
[DirectSum.Decomposition ℳ]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
[SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ]
(m : TwistingCocycle 𝒜 d P ind)
(dM : M →ₗ[R] M)
(hM : IsDGRightModule h ℳ dM)
(p : ℤ)
:
CategoryTheory.CategoryStruct.comp (m.twistedIndexFiltrationFunctorObjIso dM hM p).hom
(m.twistedIndexCochainComplexι hM p) = CategoryTheory.CategoryStruct.comp
(CochainComplex.filtrationFunctorObjIso (m.twistedIndexSubobject hM) ⋯ (WithBotTop.coe p)).hom
(CochainComplex.filtrationEInt (m.twistedIndexSubobject hM) (WithBotTop.coe p)).arrow
The identification of a step of twistedIndexFiltrationFunctor with F_p is compatible with
the inclusions into the twisted complex.
@[simp]
theorem
TauCeti.TwistingCocycle.twistedIndexFiltrationFunctorObjIso_hom_comp_indexFiltrationι_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]
{ind : P → ℤ}
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[SMulCommClass R Aᵐᵒᵖ M]
{ℳ : ℤ → Submodule R M}
[DirectSum.Decomposition ℳ]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
[SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ]
(m : TwistingCocycle 𝒜 d P ind)
(dM : M →ₗ[R] M)
(hM : IsDGRightModule h ℳ dM)
(p : ℤ)
{Z : CochainComplex (ModuleCat R) ℤ}
(h✝ : m.twistedCochainComplex dM hM ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (m.twistedIndexFiltrationFunctorObjIso dM hM p).hom
(CategoryTheory.CategoryStruct.comp (m.twistedIndexCochainComplexι hM p) h✝) = CategoryTheory.CategoryStruct.comp
(CochainComplex.filtrationFunctorObjIso (m.twistedIndexSubobject hM) ⋯ (WithBotTop.coe p)).hom
(CategoryTheory.CategoryStruct.comp
(CochainComplex.filtrationEInt (m.twistedIndexSubobject hM) (WithBotTop.coe p)).arrow h✝)
The identification of a step of twistedIndexFiltrationFunctor with F_p is compatible with
the inclusions into the twisted complex.
theorem
TauCeti.TwistingCocycle.twistedIndexFiltrationFunctor_map_objIso_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]
{ind : P → ℤ}
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[SMulCommClass R Aᵐᵒᵖ M]
{ℳ : ℤ → Submodule R M}
[DirectSum.Decomposition ℳ]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
[SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ]
(m : TwistingCocycle 𝒜 d P ind)
(dM : M →ₗ[R] M)
(hM : IsDGRightModule h ℳ dM)
(p : ℤ)
:
CategoryTheory.CategoryStruct.comp ((m.twistedIndexFiltrationFunctor dM hM).map (CategoryTheory.homOfLE ⋯))
(m.twistedIndexFiltrationFunctorObjIso dM hM (p + 1)).hom = CategoryTheory.CategoryStruct.comp (m.twistedIndexFiltrationFunctorObjIso dM hM p).hom
(m.twistedIndexCochainComplexMap hM ⋯)
The transition map F_p ⟶ F_{p+1} of twistedIndexFiltrationFunctor is the inclusion of
subcomplexes twistedIndexCochainComplexMap.
theorem
TauCeti.TwistingCocycle.twistedIndexFiltrationFunctor_map_objIso_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]
{ind : P → ℤ}
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[SMulCommClass R Aᵐᵒᵖ M]
{ℳ : ℤ → Submodule R M}
[DirectSum.Decomposition ℳ]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
[SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ]
(m : TwistingCocycle 𝒜 d P ind)
(dM : M →ₗ[R] M)
(hM : IsDGRightModule h ℳ dM)
(p : ℤ)
{Z : CochainComplex (ModuleCat R) ℤ}
(h✝ : m.twistedIndexCochainComplex hM (p + 1) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((m.twistedIndexFiltrationFunctor dM hM).map (CategoryTheory.homOfLE ⋯))
(CategoryTheory.CategoryStruct.comp (m.twistedIndexFiltrationFunctorObjIso dM hM (p + 1)).hom h✝) = CategoryTheory.CategoryStruct.comp (m.twistedIndexFiltrationFunctorObjIso dM hM p).hom
(CategoryTheory.CategoryStruct.comp (m.twistedIndexCochainComplexMap hM ⋯) h✝)
The transition map F_p ⟶ F_{p+1} of twistedIndexFiltrationFunctor is the inclusion of
subcomplexes twistedIndexCochainComplexMap.
noncomputable def
TauCeti.TwistingCocycle.twistedIndexCokernelIso
{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]
{ind : P → ℤ}
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[SMulCommClass R Aᵐᵒᵖ M]
{ℳ : ℤ → Submodule R M}
[DirectSum.Decomposition ℳ]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
[SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ]
(m : TwistingCocycle 𝒜 d P ind)
(dM : M →ₗ[R] M)
(hM : IsDGRightModule h ℳ dM)
(p : ℤ)
:
CategoryTheory.Limits.cokernel ((m.twistedIndexFiltrationFunctor dM hM).map (CategoryTheory.homOfLE ⋯)) ≅ twistedCochainComplex 0 dM hM
The graded piece F_{p+1} / F_p of the index filtration, the cokernel of the transition map of
twistedIndexFiltrationFunctor, is the twisted complex of the zero cocycle on generators of
index p + 1.
Instances For
@[simp]
theorem
TauCeti.TwistingCocycle.cokernel_π_comp_twistedIndexCokernelIso_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]
{ind : P → ℤ}
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[SMulCommClass R Aᵐᵒᵖ M]
{ℳ : ℤ → Submodule R M}
[DirectSum.Decomposition ℳ]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
[SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ]
(m : TwistingCocycle 𝒜 d P ind)
(dM : M →ₗ[R] M)
(hM : IsDGRightModule h ℳ dM)
(p : ℤ)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.cokernel.π ((m.twistedIndexFiltrationFunctor dM hM).map (CategoryTheory.homOfLE ⋯)))
(m.twistedIndexCokernelIso dM hM p).hom = CategoryTheory.CategoryStruct.comp (m.twistedIndexFiltrationFunctorObjIso dM hM (p + 1)).hom
(m.twistedIndexCochainComplexProj dM hM (p + 1))
The graded-piece isomorphism identifies the cokernel projection with restriction to the
generators of index p + 1.
@[simp]
theorem
TauCeti.TwistingCocycle.cokernel_π_comp_twistedIndexCokernelIso_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]
{ind : P → ℤ}
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[SMulCommClass R Aᵐᵒᵖ M]
{ℳ : ℤ → Submodule R M}
[DirectSum.Decomposition ℳ]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
[SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ]
(m : TwistingCocycle 𝒜 d P ind)
(dM : M →ₗ[R] M)
(hM : IsDGRightModule h ℳ dM)
(p : ℤ)
{Z : CochainComplex (ModuleCat R) ℤ}
(h✝ : twistedCochainComplex 0 dM hM ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.cokernel.π ((m.twistedIndexFiltrationFunctor dM hM).map (CategoryTheory.homOfLE ⋯)))
(CategoryTheory.CategoryStruct.comp (m.twistedIndexCokernelIso dM hM p).hom h✝) = CategoryTheory.CategoryStruct.comp (m.twistedIndexFiltrationFunctorObjIso dM hM (p + 1)).hom
(CategoryTheory.CategoryStruct.comp (m.twistedIndexCochainComplexProj dM hM (p + 1)) h✝)
The graded-piece isomorphism identifies the cokernel projection with restriction to the
generators of index p + 1.
noncomputable def
TauCeti.TwistingCocycle.indexSpectralSequenceFirstPageXIso
{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]
{ind : P → ℤ}
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[SMulCommClass R Aᵐᵒᵖ M]
{ℳ : ℤ → Submodule R M}
[DirectSum.Decomposition ℳ]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
[SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ]
(m : TwistingCocycle 𝒜 d P ind)
(dM : M →ₗ[R] M)
(hM : IsDGRightModule h ℳ dM)
(pq : ℤ × ℤ)
:
((CochainComplex.spectralSequence (m.twistedIndexFiltrationFunctor dM hM)).page 2
indexSpectralSequenceFirstPageXIso._proof_3).X
pq ≅ HomologicalComplex.homology (twistedCochainComplex 0 dM hM) (pq.1 + pq.2)
The first page of the index spectral sequence. Its object at (p, q), on page 2 in
Mathlib's numbering, is the cohomology H^{p+q} of the twisted complex ℳ ⊗ ⟨P_{q+1}⟩ of the zero
cocycle on the generators of index q + 1.
Instances For
theorem
TauCeti.TwistingCocycle.indexSpectralSequenceFirstPageXIso_eq
{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]
{ind : P → ℤ}
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[SMulCommClass R Aᵐᵒᵖ M]
{ℳ : ℤ → Submodule R M}
[DirectSum.Decomposition ℳ]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
[SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ]
(m : TwistingCocycle 𝒜 d P ind)
(dM : M →ₗ[R] M)
(hM : IsDGRightModule h ℳ dM)
(pq : ℤ × ℤ)
:
m.indexSpectralSequenceFirstPageXIso dM hM pq = CochainComplex.spectralSequenceFirstPageXIsoCokernel (m.twistedIndexFiltrationFunctor dM hM) pq pq.2 (pq.2 + 1) ⋯ ⋯
(pq.1 + pq.2) ⋯ ≪≫ (HomologicalComplex.homologyFunctor (ModuleCat R) (ComplexShape.up ℤ) (pq.1 + pq.2)).mapIso
(m.twistedIndexCokernelIso dM hM pq.2)
The first-page isomorphism is the generic identification with the cokernel, followed by the
isomorphism on cohomology induced by twistedIndexCokernelIso.
noncomputable def
TauCeti.TwistingCocycle.twistedIndexCokernelIsoOfEq
{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]
{ind : P → ℤ}
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[SMulCommClass R Aᵐᵒᵖ M]
{ℳ : ℤ → Submodule R M}
[DirectSum.Decomposition ℳ]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
[SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ]
(m : TwistingCocycle 𝒜 d P ind)
(dM : M →ₗ[R] M)
(hM : IsDGRightModule h ℳ dM)
(q p : ℤ)
(hqp : q + 1 = p)
:
CategoryTheory.Limits.cokernel ((m.twistedIndexFiltrationFunctor dM hM).map (CategoryTheory.homOfLE ⋯)) ≅ twistedCochainComplex 0 dM hM
The graded piece F_p / F_q, for q + 1 = p, with the indices given by an equation: the
cokernel of the transition map F_q ⟶ F_p of the functor of the index filtration is the
graded piece of index p.
Instances For
theorem
TauCeti.TwistingCocycle.twistedIndexCokernelIsoOfEq_self
{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]
{ind : P → ℤ}
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[SMulCommClass R Aᵐᵒᵖ M]
{ℳ : ℤ → Submodule R M}
[DirectSum.Decomposition ℳ]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
[SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ]
(m : TwistingCocycle 𝒜 d P ind)
(dM : M →ₗ[R] M)
(hM : IsDGRightModule h ℳ dM)
(q : ℤ)
:
With the standard indices, twistedIndexCokernelIsoOfEq is twistedIndexCokernelIso.
@[simp]
theorem
TauCeti.TwistingCocycle.cokernel_π_comp_twistedIndexCokernelIsoOfEq_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]
{ind : P → ℤ}
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[SMulCommClass R Aᵐᵒᵖ M]
{ℳ : ℤ → Submodule R M}
[DirectSum.Decomposition ℳ]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
[SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ]
(m : TwistingCocycle 𝒜 d P ind)
(dM : M →ₗ[R] M)
(hM : IsDGRightModule h ℳ dM)
(q p : ℤ)
(hqp : q + 1 = p)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.cokernel.π ((m.twistedIndexFiltrationFunctor dM hM).map (CategoryTheory.homOfLE ⋯)))
(m.twistedIndexCokernelIsoOfEq dM hM q p hqp).hom = CategoryTheory.CategoryStruct.comp (m.twistedIndexFiltrationFunctorObjIso dM hM p).hom
(m.twistedIndexCochainComplexProj dM hM p)
The graded-piece isomorphism identifies the cokernel projection with restriction to the
generators of index p.
@[simp]
theorem
TauCeti.TwistingCocycle.cokernel_π_comp_twistedIndexCokernelIsoOfEq_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]
{ind : P → ℤ}
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[SMulCommClass R Aᵐᵒᵖ M]
{ℳ : ℤ → Submodule R M}
[DirectSum.Decomposition ℳ]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
[SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ]
(m : TwistingCocycle 𝒜 d P ind)
(dM : M →ₗ[R] M)
(hM : IsDGRightModule h ℳ dM)
(q p : ℤ)
(hqp : q + 1 = p)
{Z : CochainComplex (ModuleCat R) ℤ}
(h✝ : twistedCochainComplex 0 dM hM ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.cokernel.π ((m.twistedIndexFiltrationFunctor dM hM).map (CategoryTheory.homOfLE ⋯)))
(CategoryTheory.CategoryStruct.comp (m.twistedIndexCokernelIsoOfEq dM hM q p hqp).hom h✝) = CategoryTheory.CategoryStruct.comp (m.twistedIndexFiltrationFunctorObjIso dM hM p).hom
(CategoryTheory.CategoryStruct.comp (m.twistedIndexCochainComplexProj dM hM p) h✝)
The graded-piece isomorphism identifies the cokernel projection with restriction to the
generators of index p.
noncomputable def
TauCeti.TwistingCocycle.indexSpectralSequenceFirstPageXIsoOfEq
{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]
{ind : P → ℤ}
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[SMulCommClass R Aᵐᵒᵖ M]
{ℳ : ℤ → Submodule R M}
[DirectSum.Decomposition ℳ]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
[SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ]
(m : TwistingCocycle 𝒜 d P ind)
(dM : M →ₗ[R] M)
(hM : IsDGRightModule h ℳ dM)
(pq : ℤ × ℤ)
(i₁ i₂ : ℤ)
(hi₁ : i₁ = pq.2)
(hi₂ : i₂ = pq.2 + 1)
(n : ℤ)
(hn : n = pq.1 + pq.2)
:
The first page of the index spectral sequence, with the indices q, q + 1 and p + q
given by equations, as in CochainComplex.spectralSequenceFirstPageXIsoCokernel: the object at
(p, q) is the cohomology in degree p + q of the graded piece of index q + 1.
Instances For
theorem
TauCeti.TwistingCocycle.indexSpectralSequenceFirstPageXIsoOfEq_eq
{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]
{ind : P → ℤ}
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[SMulCommClass R Aᵐᵒᵖ M]
{ℳ : ℤ → Submodule R M}
[DirectSum.Decomposition ℳ]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
[SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ]
(m : TwistingCocycle 𝒜 d P ind)
(dM : M →ₗ[R] M)
(hM : IsDGRightModule h ℳ dM)
(pq : ℤ × ℤ)
(i₁ i₂ : ℤ)
(hi₁ : i₁ = pq.2)
(hi₂ : i₂ = pq.2 + 1)
(n : ℤ)
(hn : n = pq.1 + pq.2)
:
m.indexSpectralSequenceFirstPageXIsoOfEq dM hM pq i₁ i₂ hi₁ hi₂ n hn = CochainComplex.spectralSequenceFirstPageXIsoCokernel (m.twistedIndexFiltrationFunctor dM hM) pq i₁ i₂ hi₁ hi₂ n hn ≪≫ HomologicalComplex.homologyMapIso (m.twistedIndexCokernelIsoOfEq dM hM i₁ i₂ ⋯) n
indexSpectralSequenceFirstPageXIsoOfEq is the generic identification with the cokernel,
followed by the isomorphism on cohomology induced by twistedIndexCokernelIsoOfEq.
theorem
TauCeti.TwistingCocycle.indexSpectralSequenceFirstPageXIsoOfEq_self
{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]
{ind : P → ℤ}
[Module Aᵐᵒᵖ M]
[IsScalarTower R Aᵐᵒᵖ M]
[SMulCommClass R Aᵐᵒᵖ M]
{ℳ : ℤ → Submodule R M}
[DirectSum.Decomposition ℳ]
{𝒜 : ℤ → Submodule R A}
[GradedAlgebra 𝒜]
{d : A →ₗ[R] A}
{h : IsDGAlgebra 𝒜 d}
[SetLike.GradedSMul ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ) ℳ]
(m : TwistingCocycle 𝒜 d P ind)
(dM : M →ₗ[R] M)
(hM : IsDGRightModule h ℳ dM)
(pq : ℤ × ℤ)
:
m.indexSpectralSequenceFirstPageXIsoOfEq dM hM pq pq.2 (pq.2 + 1) ⋯ ⋯ (pq.1 + pq.2) ⋯ = m.indexSpectralSequenceFirstPageXIso dM hM pq
With the standard indices, indexSpectralSequenceFirstPageXIsoOfEq is
indexSpectralSequenceFirstPageXIso.