The morphism of spectral sequences induced by a morphism of spectral objects #
Let φ : X ⟶ Y be a morphism of spectral objects indexed by a preorder ι, and data a recipe
for spectral sequences such that X.HasSpectralSequence data and Y.HasSpectralSequence data.
On each page, φ induces a morphism of homological complexes
CategoryTheory.Abelian.SpectralObject.spectralSequencePageMap data φ r, given on the object at
pq by EMap through Mathlib's identifications spectralSequencePageXIso, and these morphisms
are compatible with the isomorphisms between the homology of a page and the next page. They form
the morphism of spectral sequences CategoryTheory.Abelian.SpectralObject.spectralSequenceMap,
which is functorial in φ.
Main definitions #
CategoryTheory.Abelian.SpectralObject.spectralSequencePageMap data φ r: the morphism of pages.CategoryTheory.Abelian.SpectralObject.spectralSequenceMap data φ: the morphism of spectral sequences.
Main results #
CategoryTheory.Abelian.SpectralObject.homologyMap_spectralSequencePageMap_comp_iso_hom: the morphisms of pages are compatible with the identification of the homology of a page with the next page.CategoryTheory.Abelian.SpectralObject.spectralSequenceMap_id,CategoryTheory.Abelian.SpectralObject.spectralSequenceMap_comp: functoriality.
Implementation notes #
The explicit description SpectralObject.spectralSequence_iso of the isomorphisms between the
homology of a page and the next page refers to private auxiliary proofs of its file, so that this
file imports all of Mathlib.Algebra.Homology.SpectralObject.SpectralSequence. The comparison
with spectralSequenceHomologyData uses unseal spectralSequence, like the proofs of Mathlib's
spectralSequenceHomologyData_left_i and _left_π.
noncomputable def
CategoryTheory.Abelian.SpectralObject.spectralSequencePageXMap
{C : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Category.{v_1, u_1} C]
[Abelian C]
[Preorder ι]
{c : ℤ → ComplexShape κ}
{r₀ : ℤ}
(data : SpectralSequenceDataCore ι c r₀)
{X Y : SpectralObject C ι}
(φ : X ⟶ Y)
[X.HasSpectralSequence data]
[Y.HasSpectralSequence data]
(r : ℤ)
(hr : r₀ ≤ r)
(pq : κ)
:
The morphism between the objects at pq on the rth pages of the spectral sequences of X
and Y, through Mathlib's identifications of these objects with objects E.
Instances For
theorem
CategoryTheory.Abelian.SpectralObject.spectralSequencePageXMap_eq
{C : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Category.{v_1, u_1} C]
[Abelian C]
[Preorder ι]
{c : ℤ → ComplexShape κ}
{r₀ : ℤ}
(data : SpectralSequenceDataCore ι c r₀)
{X Y : SpectralObject C ι}
(φ : X ⟶ Y)
[X.HasSpectralSequence data]
[Y.HasSpectralSequence data]
(r : ℤ)
(hr : r₀ ≤ r)
(pq : κ)
(i₀ i₁ i₂ i₃ : ι)
(h₀ : i₀ = data.i₀ r pq ⋯)
(h₁ : i₁ = data.i₁ pq)
(h₂ : i₂ = data.i₂ pq)
(h₃ : i₃ = data.i₃ r pq ⋯)
(n₀ n₁ n₂ : ℤ)
(h : n₁ = data.deg pq)
(hn₁ : n₀ + 1 = n₁)
(hn₂ : n₁ + 1 = n₂)
:
spectralSequencePageXMap data φ r hr pq = CategoryStruct.comp (X.spectralSequencePageXIso data r hr pq i₀ i₁ i₂ i₃ h₀ h₁ h₂ h₃ n₀ n₁ n₂ h hn₁ hn₂).hom
(CategoryStruct.comp (EMap φ (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂)
(Y.spectralSequencePageXIso data r hr pq i₀ i₁ i₂ i₃ h₀ h₁ h₂ h₃ n₀ n₁ n₂ h hn₁ hn₂).inv)
The morphism spectralSequencePageXMap may be computed through any choice of indices
equal to those of the recipe data.
theorem
CategoryTheory.Abelian.SpectralObject.spectralSequencePageXIso_hom_comp_EMap
{C : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Category.{v_1, u_1} C]
[Abelian C]
[Preorder ι]
{c : ℤ → ComplexShape κ}
{r₀ : ℤ}
(data : SpectralSequenceDataCore ι c r₀)
{X Y : SpectralObject C ι}
(φ : X ⟶ Y)
[X.HasSpectralSequence data]
[Y.HasSpectralSequence data]
(r : ℤ)
(hr : r₀ ≤ r)
(pq : κ)
(i₀ i₁ i₂ i₃ : ι)
(h₀ : i₀ = data.i₀ r pq ⋯)
(h₁ : i₁ = data.i₁ pq)
(h₂ : i₂ = data.i₂ pq)
(h₃ : i₃ = data.i₃ r pq ⋯)
(n₀ n₁ n₂ : ℤ)
(h : n₁ = data.deg pq)
(hn₁ : n₀ + 1 = n₁)
(hn₂ : n₁ + 1 = n₂)
:
CategoryStruct.comp (X.spectralSequencePageXIso data r hr pq i₀ i₁ i₂ i₃ h₀ h₁ h₂ h₃ n₀ n₁ n₂ h hn₁ hn₂).hom
(EMap φ (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂) = CategoryStruct.comp (spectralSequencePageXMap data φ r hr pq)
(Y.spectralSequencePageXIso data r hr pq i₀ i₁ i₂ i₃ h₀ h₁ h₂ h₃ n₀ n₁ n₂ h hn₁ hn₂).hom
theorem
CategoryTheory.Abelian.SpectralObject.spectralSequencePageXIso_hom_comp_EMap_assoc
{C : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Category.{v_1, u_1} C]
[Abelian C]
[Preorder ι]
{c : ℤ → ComplexShape κ}
{r₀ : ℤ}
(data : SpectralSequenceDataCore ι c r₀)
{X Y : SpectralObject C ι}
(φ : X ⟶ Y)
[X.HasSpectralSequence data]
[Y.HasSpectralSequence data]
(r : ℤ)
(hr : r₀ ≤ r)
(pq : κ)
(i₀ i₁ i₂ i₃ : ι)
(h₀ : i₀ = data.i₀ r pq ⋯)
(h₁ : i₁ = data.i₁ pq)
(h₂ : i₂ = data.i₂ pq)
(h₃ : i₃ = data.i₃ r pq ⋯)
(n₀ n₁ n₂ : ℤ)
(h : n₁ = data.deg pq)
(hn₁ : n₀ + 1 = n₁)
(hn₂ : n₁ + 1 = n₂)
{Z : C}
(h✝ : Y.E (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂ ⟶ Z)
:
CategoryStruct.comp (X.spectralSequencePageXIso data r hr pq i₀ i₁ i₂ i₃ h₀ h₁ h₂ h₃ n₀ n₁ n₂ h hn₁ hn₂).hom
(CategoryStruct.comp (EMap φ (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂) h✝) = CategoryStruct.comp (spectralSequencePageXMap data φ r hr pq)
(CategoryStruct.comp (Y.spectralSequencePageXIso data r hr pq i₀ i₁ i₂ i₃ h₀ h₁ h₂ h₃ n₀ n₁ n₂ h hn₁ hn₂).hom h✝)
theorem
CategoryTheory.Abelian.SpectralObject.EMap_comp_spectralSequencePageXIso_inv
{C : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Category.{v_1, u_1} C]
[Abelian C]
[Preorder ι]
{c : ℤ → ComplexShape κ}
{r₀ : ℤ}
(data : SpectralSequenceDataCore ι c r₀)
{X Y : SpectralObject C ι}
(φ : X ⟶ Y)
[X.HasSpectralSequence data]
[Y.HasSpectralSequence data]
(r : ℤ)
(hr : r₀ ≤ r)
(pq : κ)
(i₀ i₁ i₂ i₃ : ι)
(h₀ : i₀ = data.i₀ r pq ⋯)
(h₁ : i₁ = data.i₁ pq)
(h₂ : i₂ = data.i₂ pq)
(h₃ : i₃ = data.i₃ r pq ⋯)
(n₀ n₁ n₂ : ℤ)
(h : n₁ = data.deg pq)
(hn₁ : n₀ + 1 = n₁)
(hn₂ : n₁ + 1 = n₂)
:
CategoryStruct.comp (EMap φ (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂)
(Y.spectralSequencePageXIso data r hr pq i₀ i₁ i₂ i₃ h₀ h₁ h₂ h₃ n₀ n₁ n₂ h hn₁ hn₂).inv = CategoryStruct.comp (X.spectralSequencePageXIso data r hr pq i₀ i₁ i₂ i₃ h₀ h₁ h₂ h₃ n₀ n₁ n₂ h hn₁ hn₂).inv
(spectralSequencePageXMap data φ r hr pq)
theorem
CategoryTheory.Abelian.SpectralObject.EMap_comp_spectralSequencePageXIso_inv_assoc
{C : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Category.{v_1, u_1} C]
[Abelian C]
[Preorder ι]
{c : ℤ → ComplexShape κ}
{r₀ : ℤ}
(data : SpectralSequenceDataCore ι c r₀)
{X Y : SpectralObject C ι}
(φ : X ⟶ Y)
[X.HasSpectralSequence data]
[Y.HasSpectralSequence data]
(r : ℤ)
(hr : r₀ ≤ r)
(pq : κ)
(i₀ i₁ i₂ i₃ : ι)
(h₀ : i₀ = data.i₀ r pq ⋯)
(h₁ : i₁ = data.i₁ pq)
(h₂ : i₂ = data.i₂ pq)
(h₃ : i₃ = data.i₃ r pq ⋯)
(n₀ n₁ n₂ : ℤ)
(h : n₁ = data.deg pq)
(hn₁ : n₀ + 1 = n₁)
(hn₂ : n₁ + 1 = n₂)
{Z : C}
(h✝ : ((Y.spectralSequence data).page r ⋯).X pq ⟶ Z)
:
CategoryStruct.comp (EMap φ (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂)
(CategoryStruct.comp (Y.spectralSequencePageXIso data r hr pq i₀ i₁ i₂ i₃ h₀ h₁ h₂ h₃ n₀ n₁ n₂ h hn₁ hn₂).inv h✝) = CategoryStruct.comp (X.spectralSequencePageXIso data r hr pq i₀ i₁ i₂ i₃ h₀ h₁ h₂ h₃ n₀ n₁ n₂ h hn₁ hn₂).inv
(CategoryStruct.comp (spectralSequencePageXMap data φ r hr pq) h✝)
theorem
CategoryTheory.Abelian.SpectralObject.spectralSequence_page_d_comp_spectralSequencePageXMap
{C : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Category.{v_1, u_1} C]
[Abelian C]
[Preorder ι]
{c : ℤ → ComplexShape κ}
{r₀ : ℤ}
(data : SpectralSequenceDataCore ι c r₀)
{X Y : SpectralObject C ι}
(φ : X ⟶ Y)
[X.HasSpectralSequence data]
[Y.HasSpectralSequence data]
(r : ℤ)
(hr : r₀ ≤ r)
(pq pq' : κ)
:
CategoryStruct.comp (((X.spectralSequence data).page r ⋯).d pq pq') (spectralSequencePageXMap data φ r hr pq') = CategoryStruct.comp (spectralSequencePageXMap data φ r hr pq) (((Y.spectralSequence data).page r ⋯).d pq pq')
The morphisms spectralSequencePageXMap commute with the differentials of the pages.
theorem
CategoryTheory.Abelian.SpectralObject.spectralSequence_page_d_comp_spectralSequencePageXMap_assoc
{C : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Category.{v_1, u_1} C]
[Abelian C]
[Preorder ι]
{c : ℤ → ComplexShape κ}
{r₀ : ℤ}
(data : SpectralSequenceDataCore ι c r₀)
{X Y : SpectralObject C ι}
(φ : X ⟶ Y)
[X.HasSpectralSequence data]
[Y.HasSpectralSequence data]
(r : ℤ)
(hr : r₀ ≤ r)
(pq pq' : κ)
{Z : C}
(h : ((Y.spectralSequence data).page r ⋯).X pq' ⟶ Z)
:
CategoryStruct.comp (((X.spectralSequence data).page r ⋯).d pq pq')
(CategoryStruct.comp (spectralSequencePageXMap data φ r hr pq') h) = CategoryStruct.comp (spectralSequencePageXMap data φ r hr pq)
(CategoryStruct.comp (((Y.spectralSequence data).page r ⋯).d pq pq') h)
The morphisms spectralSequencePageXMap commute with the differentials of the pages.
noncomputable def
CategoryTheory.Abelian.SpectralObject.spectralSequencePageMap
{C : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Category.{v_1, u_1} C]
[Abelian C]
[Preorder ι]
{c : ℤ → ComplexShape κ}
{r₀ : ℤ}
(data : SpectralSequenceDataCore ι c r₀)
{X Y : SpectralObject C ι}
(φ : X ⟶ Y)
[X.HasSpectralSequence data]
[Y.HasSpectralSequence data]
(r : ℤ)
(hr : r₀ ≤ r)
:
The morphism between the rth pages of the spectral sequences of X and Y induced by a
morphism φ : X ⟶ Y of spectral objects.
Instances For
@[simp]
theorem
CategoryTheory.Abelian.SpectralObject.spectralSequencePageMap_f
{C : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Category.{v_1, u_1} C]
[Abelian C]
[Preorder ι]
{c : ℤ → ComplexShape κ}
{r₀ : ℤ}
(data : SpectralSequenceDataCore ι c r₀)
{X Y : SpectralObject C ι}
(φ : X ⟶ Y)
[X.HasSpectralSequence data]
[Y.HasSpectralSequence data]
(r : ℤ)
(hr : r₀ ≤ r)
(pq : κ)
:
theorem
CategoryTheory.Abelian.SpectralObject.homologyMap_spectralSequencePageMap_comp_iso_hom
{C : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Category.{v_1, u_1} C]
[Abelian C]
[Preorder ι]
{c : ℤ → ComplexShape κ}
{r₀ : ℤ}
(data : SpectralSequenceDataCore ι c r₀)
{X Y : SpectralObject C ι}
(φ : X ⟶ Y)
[X.HasSpectralSequence data]
[Y.HasSpectralSequence data]
(r r' : ℤ)
(hrr' : r + 1 = r')
(hr : r₀ ≤ r)
(hr' : r₀ ≤ r')
(pq : κ)
:
CategoryStruct.comp (HomologicalComplex.homologyMap (spectralSequencePageMap data φ r hr) pq)
((Y.spectralSequence data).iso r r' pq hrr' hr).hom = CategoryStruct.comp ((X.spectralSequence data).iso r r' pq hrr' hr).hom ((spectralSequencePageMap data φ r' hr').f pq)
The morphisms of pages spectralSequencePageMap are compatible with the isomorphisms between
the homology of a page and the next page.
theorem
CategoryTheory.Abelian.SpectralObject.homologyMap_spectralSequencePageMap_comp_iso_hom_assoc
{C : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Category.{v_1, u_1} C]
[Abelian C]
[Preorder ι]
{c : ℤ → ComplexShape κ}
{r₀ : ℤ}
(data : SpectralSequenceDataCore ι c r₀)
{X Y : SpectralObject C ι}
(φ : X ⟶ Y)
[X.HasSpectralSequence data]
[Y.HasSpectralSequence data]
(r r' : ℤ)
(hrr' : r + 1 = r')
(hr : r₀ ≤ r)
(hr' : r₀ ≤ r')
(pq : κ)
{Z : C}
(h : ((Y.spectralSequence data).page r' ⋯).X pq ⟶ Z)
:
CategoryStruct.comp (HomologicalComplex.homologyMap (spectralSequencePageMap data φ r hr) pq)
(CategoryStruct.comp ((Y.spectralSequence data).iso r r' pq hrr' hr).hom h) = CategoryStruct.comp ((X.spectralSequence data).iso r r' pq hrr' hr).hom
(CategoryStruct.comp ((spectralSequencePageMap data φ r' hr').f pq) h)
The morphisms of pages spectralSequencePageMap are compatible with the isomorphisms between
the homology of a page and the next page.
noncomputable def
CategoryTheory.Abelian.SpectralObject.spectralSequenceMap
{C : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Category.{v_1, u_1} C]
[Abelian C]
[Preorder ι]
{c : ℤ → ComplexShape κ}
{r₀ : ℤ}
(data : SpectralSequenceDataCore ι c r₀)
{X Y : SpectralObject C ι}
(φ : X ⟶ Y)
[X.HasSpectralSequence data]
[Y.HasSpectralSequence data]
:
The morphism of spectral sequences induced by a morphism of spectral objects.
Instances For
@[simp]
theorem
CategoryTheory.Abelian.SpectralObject.spectralSequenceMap_hom
{C : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Category.{v_1, u_1} C]
[Abelian C]
[Preorder ι]
{c : ℤ → ComplexShape κ}
{r₀ : ℤ}
(data : SpectralSequenceDataCore ι c r₀)
{X Y : SpectralObject C ι}
(φ : X ⟶ Y)
[X.HasSpectralSequence data]
[Y.HasSpectralSequence data]
(r : ℤ)
(hr : r₀ ≤ r)
:
@[simp]
theorem
CategoryTheory.Abelian.SpectralObject.spectralSequencePageXMap_id
{C : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Category.{v_1, u_1} C]
[Abelian C]
[Preorder ι]
{c : ℤ → ComplexShape κ}
{r₀ : ℤ}
(data : SpectralSequenceDataCore ι c r₀)
{X : SpectralObject C ι}
[X.HasSpectralSequence data]
(r : ℤ)
(hr : r₀ ≤ r)
(pq : κ)
:
spectralSequencePageXMap data (CategoryStruct.id X) r hr pq = CategoryStruct.id (((X.spectralSequence data).page r ⋯).X pq)
@[simp]
theorem
CategoryTheory.Abelian.SpectralObject.spectralSequencePageXMap_comp
{C : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Category.{v_1, u_1} C]
[Abelian C]
[Preorder ι]
{c : ℤ → ComplexShape κ}
{r₀ : ℤ}
(data : SpectralSequenceDataCore ι c r₀)
{X Y Z : SpectralObject C ι}
(φ : X ⟶ Y)
(ψ : Y ⟶ Z)
[X.HasSpectralSequence data]
[Y.HasSpectralSequence data]
[Z.HasSpectralSequence data]
(r : ℤ)
(hr : r₀ ≤ r)
(pq : κ)
:
spectralSequencePageXMap data (CategoryStruct.comp φ ψ) r hr pq = CategoryStruct.comp (spectralSequencePageXMap data φ r hr pq) (spectralSequencePageXMap data ψ r hr pq)
theorem
CategoryTheory.Abelian.SpectralObject.spectralSequencePageXMap_comp_assoc
{C : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Category.{v_1, u_1} C]
[Abelian C]
[Preorder ι]
{c : ℤ → ComplexShape κ}
{r₀ : ℤ}
(data : SpectralSequenceDataCore ι c r₀)
{X Y Z : SpectralObject C ι}
(φ : X ⟶ Y)
(ψ : Y ⟶ Z)
[X.HasSpectralSequence data]
[Y.HasSpectralSequence data]
[Z.HasSpectralSequence data]
(r : ℤ)
(hr : r₀ ≤ r)
(pq : κ)
{Z✝ : C}
(h : ((Z.spectralSequence data).page r ⋯).X pq ⟶ Z✝)
:
CategoryStruct.comp (spectralSequencePageXMap data (CategoryStruct.comp φ ψ) r hr pq) h = CategoryStruct.comp (spectralSequencePageXMap data φ r hr pq)
(CategoryStruct.comp (spectralSequencePageXMap data ψ r hr pq) h)
@[simp]
theorem
CategoryTheory.Abelian.SpectralObject.spectralSequencePageMap_id
{C : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Category.{v_1, u_1} C]
[Abelian C]
[Preorder ι]
{c : ℤ → ComplexShape κ}
{r₀ : ℤ}
(data : SpectralSequenceDataCore ι c r₀)
{X : SpectralObject C ι}
[X.HasSpectralSequence data]
(r : ℤ)
(hr : r₀ ≤ r)
:
spectralSequencePageMap data (CategoryStruct.id X) r hr = CategoryStruct.id ((X.spectralSequence data).page r ⋯)
@[simp]
theorem
CategoryTheory.Abelian.SpectralObject.spectralSequencePageMap_comp
{C : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Category.{v_1, u_1} C]
[Abelian C]
[Preorder ι]
{c : ℤ → ComplexShape κ}
{r₀ : ℤ}
(data : SpectralSequenceDataCore ι c r₀)
{X Y Z : SpectralObject C ι}
(φ : X ⟶ Y)
(ψ : Y ⟶ Z)
[X.HasSpectralSequence data]
[Y.HasSpectralSequence data]
[Z.HasSpectralSequence data]
(r : ℤ)
(hr : r₀ ≤ r)
:
spectralSequencePageMap data (CategoryStruct.comp φ ψ) r hr = CategoryStruct.comp (spectralSequencePageMap data φ r hr) (spectralSequencePageMap data ψ r hr)
theorem
CategoryTheory.Abelian.SpectralObject.spectralSequencePageMap_comp_assoc
{C : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Category.{v_1, u_1} C]
[Abelian C]
[Preorder ι]
{c : ℤ → ComplexShape κ}
{r₀ : ℤ}
(data : SpectralSequenceDataCore ι c r₀)
{X Y Z : SpectralObject C ι}
(φ : X ⟶ Y)
(ψ : Y ⟶ Z)
[X.HasSpectralSequence data]
[Y.HasSpectralSequence data]
[Z.HasSpectralSequence data]
(r : ℤ)
(hr : r₀ ≤ r)
{Z✝ : HomologicalComplex C (c r)}
(h : (Z.spectralSequence data).page r ⋯ ⟶ Z✝)
:
CategoryStruct.comp (spectralSequencePageMap data (CategoryStruct.comp φ ψ) r hr) h = CategoryStruct.comp (spectralSequencePageMap data φ r hr)
(CategoryStruct.comp (spectralSequencePageMap data ψ r hr) h)
@[simp]
theorem
CategoryTheory.Abelian.SpectralObject.spectralSequenceMap_id
{C : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Category.{v_1, u_1} C]
[Abelian C]
[Preorder ι]
{c : ℤ → ComplexShape κ}
{r₀ : ℤ}
(data : SpectralSequenceDataCore ι c r₀)
{X : SpectralObject C ι}
[X.HasSpectralSequence data]
:
@[simp]
theorem
CategoryTheory.Abelian.SpectralObject.spectralSequenceMap_comp
{C : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Category.{v_1, u_1} C]
[Abelian C]
[Preorder ι]
{c : ℤ → ComplexShape κ}
{r₀ : ℤ}
(data : SpectralSequenceDataCore ι c r₀)
{X Y Z : SpectralObject C ι}
(φ : X ⟶ Y)
(ψ : Y ⟶ Z)
[X.HasSpectralSequence data]
[Y.HasSpectralSequence data]
[Z.HasSpectralSequence data]
:
spectralSequenceMap data (CategoryStruct.comp φ ψ) = CategoryStruct.comp (spectralSequenceMap data φ) (spectralSequenceMap data ψ)
theorem
CategoryTheory.Abelian.SpectralObject.spectralSequenceMap_comp_assoc
{C : Type u_1}
{ι : Type u_2}
{κ : Type u_3}
[Category.{v_1, u_1} C]
[Abelian C]
[Preorder ι]
{c : ℤ → ComplexShape κ}
{r₀ : ℤ}
(data : SpectralSequenceDataCore ι c r₀)
{X Y Z : SpectralObject C ι}
(φ : X ⟶ Y)
(ψ : Y ⟶ Z)
[X.HasSpectralSequence data]
[Y.HasSpectralSequence data]
[Z.HasSpectralSequence data]
{Z✝ : SpectralSequence C c r₀}
(h : Z.spectralSequence data ⟶ Z✝)
:
CategoryStruct.comp (spectralSequenceMap data (CategoryStruct.comp φ ψ)) h = CategoryStruct.comp (spectralSequenceMap data φ) (CategoryStruct.comp (spectralSequenceMap data ψ) h)