Spectral sequences

In this file, we define the category SpectralSequence C c r₀ of spectral sequences in an abelian category C with Eᵣ-pages defined from r₀ : ℤ having differentials given by complex shapes c : ℤ → ComplexShape κ, where κ is the index type for the objects on each page (e.g. κ := ℤ × ℤ or κ := ℕ × ℕ). A spectral sequence is defined as the data of a sequence of homological complexes (the pages) and a sequence of isomorphisms between the homology of a page and the next page.

structure CategoryTheory.SpectralSequence (C : Type u_1) [Category.{u_3, u_1} C] [Abelian C] {κ : Type u_2} (c : ℤ → ComplexShape κ) (r₀ : ℤ) : Type (max (max u_1 u_2) u_3)

Given an abelian category C, a sequence of complex shapes c : ℤ → ComplexShape κ and a starting page r₀ : ℤ, a spectral sequence involves pages which are homological complexes and isomorphisms saying that the homology of a page identifies to the next page.

• page (r : ℤ) (hr : r₀ ≤ r := by lia) : HomologicalComplex C (c r)

  the rth page of a spectral sequence is an homological complex

• iso (r r' : ℤ) (pq : κ) (hrr' : r + 1 = r' := by lia) (hr : r₀ ≤ r := by lia) : (self.page r ⋯).homology pq ≅ (self.page r' ⋯).X pq

  the isomorphism between the homology of the r-th page at an object pq : κ and the corresponding object on the next page

structure CategoryTheory.SpectralSequence.Hom {C : Type u_1} [Category.{u_3, u_1} C] [Abelian C] {κ : Type u_2} {c : ℤ → ComplexShape κ} {r₀ : ℤ} (E E' : SpectralSequence C c r₀) : Type (max u_2 u_3)

A morphism of spectral sequences is a sequence of morphisms between the pages which commutes with the isomorphisms in homology.

• hom (r : ℤ) (hr : r₀ ≤ r := by lia) : E.page r ⋯ ⟶ E'.page r ⋯

  the morphism of homological complexes between the rth pages

• comm (r r' : ℤ) (pq : κ) (hrr' : r + 1 = r' := by lia) (hr : r₀ ≤ r := by lia) : CategoryStruct.comp (HomologicalComplex.homologyMap (self.hom r ⋯) pq) (E'.iso r r' pq ⋯ ⋯).hom = CategoryStruct.comp (E.iso r r' pq ⋯ ⋯).hom ((self.hom r' ⋯).f pq)

theorem CategoryTheory.SpectralSequence.Hom.ext_iff {C : Type u_1} {inst✝ : Category.{u_3, u_1} C} {inst✝¹ : Abelian C} {κ : Type u_2} {c : ℤ → ComplexShape κ} {r₀ : ℤ} {E E' : SpectralSequence C c r₀} {x y : E.Hom E'} : x = y ↔ @hom C inst✝ inst✝¹ κ c r₀ E E' x = @hom C inst✝ inst✝¹ κ c r₀ E E' y

theorem CategoryTheory.SpectralSequence.Hom.ext {C : Type u_1} {inst✝ : Category.{u_3, u_1} C} {inst✝¹ : Abelian C} {κ : Type u_2} {c : ℤ → ComplexShape κ} {r₀ : ℤ} {E E' : SpectralSequence C c r₀} {x y : E.Hom E'} (hom : @hom C inst✝ inst✝¹ κ c r₀ E E' x = @hom C inst✝ inst✝¹ κ c r₀ E E' y) : x = y

def CategoryTheory.SpectralSequence.pageXIsoOfEq {C : Type u_1} [Category.{u_3, u_1} C] [Abelian C] {κ : Type u_2} {c : ℤ → ComplexShape κ} {r₀ : ℤ} (E : SpectralSequence C c r₀) (pq : κ) (r r' : ℤ) (h : r = r' := by lia) (hr : r₀ ≤ r := by lia) : (E.page r ⋯).X pq ≅ (E.page r' ⋯).X pq

If E is a spectral sequence, and r = r', this is the isomorphism (E.page r).X pq ≅ (E.page r').X pq.

Equations

• E.pageXIsoOfEq pq r r' h hr = CategoryTheory.eqToIso ⋯

@[simp]

theorem CategoryTheory.SpectralSequence.Hom.comm_assoc {C : Type u_1} [Category.{u_3, u_1} C] [Abelian C] {κ : Type u_2} {c : ℤ → ComplexShape κ} {r₀ : ℤ} {E E' : SpectralSequence C c r₀} (self : E.Hom E') (r r' : ℤ) (pq : κ) (hrr' : r + 1 = r' := by lia) (hr : r₀ ≤ r := by lia) {Z : C} (h : (E'.page r' ⋯).X pq ⟶ Z) : CategoryStruct.comp (HomologicalComplex.homologyMap (self.hom r ⋯) pq) (CategoryStruct.comp (E'.iso r r' pq ⋯ ⋯).hom h) = CategoryStruct.comp (E.iso r r' pq ⋯ ⋯).hom (CategoryStruct.comp ((self.hom r' ⋯).f pq) h)

@[implicit_reducible]

instance CategoryTheory.SpectralSequence.instCategory {C : Type u_1} [Category.{u_3, u_1} C] [Abelian C] {κ : Type u_2} {c : ℤ → ComplexShape κ} {r₀ : ℤ} : Category.{max u_2 u_3, max (max u_3 u_2) u_1} (SpectralSequence C c r₀)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.SpectralSequence.id_hom {C : Type u_1} [Category.{u_3, u_1} C] [Abelian C] {κ : Type u_2} {c : ℤ → ComplexShape κ} {r₀ : ℤ} (x✝ : SpectralSequence C c r₀) (x✝¹ : ℤ) (x✝² : r₀ ≤ x✝¹) : (CategoryStruct.id x✝).hom x✝¹ x✝² = CategoryStruct.id (x✝.page x✝¹ ⋯)

@[simp]

theorem CategoryTheory.SpectralSequence.comp_hom {C : Type u_1} [Category.{u_3, u_1} C] [Abelian C] {κ : Type u_2} {c : ℤ → ComplexShape κ} {r₀ : ℤ} {X✝ Y✝ Z✝ : SpectralSequence C c r₀} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) (r : ℤ) (hr : r₀ ≤ r) : (CategoryStruct.comp f g).hom r hr = CategoryStruct.comp (f.hom r ⋯) (g.hom r ⋯)

theorem CategoryTheory.SpectralSequence.hom_ext {C : Type u_1} [Category.{u_3, u_1} C] [Abelian C] {κ : Type u_2} {c : ℤ → ComplexShape κ} {r₀ : ℤ} {E E' : SpectralSequence C c r₀} {f f' : E ⟶ E'} (h : ∀ (r : ℤ) (hr : r₀ ≤ r), f.hom r ⋯ = f'.hom r ⋯) : f = f'

theorem CategoryTheory.SpectralSequence.hom_ext_iff {C : Type u_1} [Category.{u_3, u_1} C] [Abelian C] {κ : Type u_2} {c : ℤ → ComplexShape κ} {r₀ : ℤ} {E E' : SpectralSequence C c r₀} {f f' : E ⟶ E'} : f = f' ↔ ∀ (r : ℤ) (hr : r₀ ≤ r), f.hom r ⋯ = f'.hom r ⋯

theorem CategoryTheory.SpectralSequence.comp_hom_assoc {C : Type u_1} [Category.{u_3, u_1} C] [Abelian C] {κ : Type u_2} {c : ℤ → ComplexShape κ} {r₀ : ℤ} {X✝ Y✝ Z✝ : SpectralSequence C c r₀} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) (r : ℤ) (hr : r₀ ≤ r) {Z : HomologicalComplex C (c r)} (h : Z✝.page r ⋯ ⟶ Z) : CategoryStruct.comp ((CategoryStruct.comp f g).hom r hr) h = CategoryStruct.comp (f.hom r ⋯) (CategoryStruct.comp (g.hom r ⋯) h)

def CategoryTheory.SpectralSequence.pageFunctor (C : Type u_1) [Category.{u_3, u_1} C] [Abelian C] {κ : Type u_2} (c : ℤ → ComplexShape κ) (r₀ r : ℤ) (hr : r₀ ≤ r := by lia) : Functor (SpectralSequence C c r₀) (HomologicalComplex C (c r))

The functor SpectralSequence C c r₀ ⥤ HomologicalComplex C (c r) which sends a spectral sequence to its rth page.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.SpectralSequence.pageFunctor_obj (C : Type u_1) [Category.{u_3, u_1} C] [Abelian C] {κ : Type u_2} (c : ℤ → ComplexShape κ) (r₀ r : ℤ) (hr : r₀ ≤ r := by lia) (E : SpectralSequence C c r₀) : (pageFunctor C c r₀ r hr).obj E = E.page r ⋯

@[simp]

theorem CategoryTheory.SpectralSequence.pageFunctor_map (C : Type u_1) [Category.{u_3, u_1} C] [Abelian C] {κ : Type u_2} (c : ℤ → ComplexShape κ) (r₀ r : ℤ) (hr : r₀ ≤ r := by lia) {X✝ Y✝ : SpectralSequence C c r₀} (f : X✝ ⟶ Y✝) : (pageFunctor C c r₀ r hr).map f = f.hom r ⋯

noncomputable def CategoryTheory.SpectralSequence.pageHomologyNatIso (C : Type u_1) [Category.{u_3, u_1} C] [Abelian C] {κ : Type u_2} (c : ℤ → ComplexShape κ) (r₀ r r' : ℤ) (pq : κ) (hrr' : r + 1 = r' := by lia) (hr : r₀ ≤ r := by lia) : (pageFunctor C c r₀ r ⋯).comp (HomologicalComplex.homologyFunctor C (c r) pq) ≅ (pageFunctor C c r₀ r' ⋯).comp (HomologicalComplex.eval C (c r') pq)

The natural isomorphism between the homology of a spectral sequence on the object pq : κ of the rth page and the corresponding object on the next page.

Equations

• CategoryTheory.SpectralSequence.pageHomologyNatIso C c r₀ r r' pq hrr' hr = CategoryTheory.NatIso.ofComponents (fun (E : CategoryTheory.SpectralSequence C c r₀) => E.iso r r' pq ⋯ ⋯) ⋯

@[simp]

theorem CategoryTheory.SpectralSequence.pageHomologyNatIso_hom_app (C : Type u_1) [Category.{u_3, u_1} C] [Abelian C] {κ : Type u_2} (c : ℤ → ComplexShape κ) (r₀ r r' : ℤ) (pq : κ) (hrr' : r + 1 = r' := by lia) (hr : r₀ ≤ r := by lia) (X : SpectralSequence C c r₀) : (pageHomologyNatIso C c r₀ r r' pq hrr' hr).hom.app X = (X.iso r r' pq ⋯ ⋯).hom

@[simp]

theorem CategoryTheory.SpectralSequence.pageHomologyNatIso_inv_app (C : Type u_1) [Category.{u_3, u_1} C] [Abelian C] {κ : Type u_2} (c : ℤ → ComplexShape κ) (r₀ r r' : ℤ) (pq : κ) (hrr' : r + 1 = r' := by lia) (hr : r₀ ≤ r := by lia) (X : SpectralSequence C c r₀) : (pageHomologyNatIso C c r₀ r r' pq hrr' hr).inv.app X = (X.iso r r' pq ⋯ ⋯).inv

@[reducible, inline]

abbrev CategoryTheory.CohomologicalSpectralSequence (C : Type u_1) [Category.{u_3, u_1} C] [Abelian C] (r₀ : ℤ) : Type (max u_1 u_3)

A cohomological spectral sequence has differentials given by the vector (r, 1 - r) on the rth page.

Equations

• CategoryTheory.CohomologicalSpectralSequence C = CategoryTheory.SpectralSequence C fun (r : ℤ) => ComplexShape.up' (r, 1 - r)

@[reducible, inline]

abbrev CategoryTheory.E₂CohomologicalSpectralSequence (C : Type u_1) [Category.{u_3, u_1} C] [Abelian C] : Type (max u_1 u_3)

A E₂-cohomological spectral sequence has differentials given by the vector (r, 1 - r) on the rth page for 2 ≤ r.

Equations

• CategoryTheory.E₂CohomologicalSpectralSequence C = CategoryTheory.CohomologicalSpectralSequence C 2

@[reducible, inline]

abbrev CategoryTheory.CohomologicalSpectralSequenceNat (C : Type u_1) [Category.{u_3, u_1} C] [Abelian C] (r₀ : ℤ) : Type (max u_1 u_3)

A first quadrant cohomological spectral sequence has differentials given by the vector (r, 1 - r) on the rth page.

Equations

• CategoryTheory.CohomologicalSpectralSequenceNat C = CategoryTheory.SpectralSequence C fun (r : ℤ) => ComplexShape.spectralSequenceNat (r, 1 - r)

@[reducible, inline]

abbrev CategoryTheory.E₂CohomologicalSpectralSequenceNat (C : Type u_1) [Category.{u_3, u_1} C] [Abelian C] : Type (max u_1 u_3)

A first quadrant E₂-cohomological spectral sequence has differentials given by the vector (r, 1 - r) on the rth page for 2 ≤ r.

Equations

• CategoryTheory.E₂CohomologicalSpectralSequenceNat C = CategoryTheory.CohomologicalSpectralSequenceNat C 2

@[reducible, inline]

abbrev CategoryTheory.CohomologicalSpectralSequenceFin (C : Type u_1) [Category.{u_3, u_1} C] [Abelian C] (l : ℕ) (r₀ : ℤ) : Type (max u_1 u_3)

A cohomological spectral sequence lying on finitely many rows has differentials given by the vector (r, 1 - r) on the rth page.

Equations

• CategoryTheory.CohomologicalSpectralSequenceFin C l = CategoryTheory.SpectralSequence C fun (r : ℤ) => ComplexShape.spectralSequenceFin l (r, 1 - r)

@[reducible, inline]

abbrev CategoryTheory.E₂CohomologicalSpectralSequenceFin (C : Type u_1) [Category.{u_3, u_1} C] [Abelian C] (l : ℕ) : Type (max u_1 u_3)

A E₂-cohomological spectral sequence lying on finitely many rows has differentials given by the vector (r, 1 - r) on the rth page for 2 ≤ r.

Equations

• CategoryTheory.E₂CohomologicalSpectralSequenceFin C l = CategoryTheory.CohomologicalSpectralSequenceFin C 2 ↑l