Shapes of spectral sequences obtained from a spectral object

This file prepares for the construction of the spectral sequence of a spectral object in an abelian category which shall be conducted in the file Mathlib/Algebra/Homology/SpectralObject/SpectralSequence.lean (TODO).

In this file, we introduce a structure SpectralSequenceDataCore which contains a recipe for the construction of the pages of the spectral sequence. For example, from a spectral object X indexed by EInt the definition coreE₂Cohomological will allow to construct an E₂ cohomological spectral sequence such that the object on position (p, q) on the rth page is E^{p + q}(q - r + 2 ≤ q ≤ q + 1 ≤ q + r - 1). The data (and properties) in the structure SpectralSequenceDataCore allow to define the pages and the differentials directly from the SpectralObject API from the files Mathlib/Algebra/Homology/SpectralObject/Page.lean and Mathlib/Algebra/Homology/SpectralObject/Differentials.lean. However, the computation of the homology of the differentials in Mathlib/Algebra/Homology/SpectralObject/Homology.lean may not directly apply: we introduce a typeclass HasSpectralSequence which puts additional conditions on the spectral object so that the homology of a page identifies to the next page. These conditions are automatically satisfied for coreE₂Cohomological, but this design allows to obtain a spectral sequence with objects of the pages indexed by ℕ × ℕ instead of ℤ × ℤ when suitable conditions are satisfied by a spectral object indexed by EInt (see coreE₂CohomologicalNat and the typeclass IsFirstQuadrant).

structure CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore (ι : Type u_2) {κ : Type u_3} [Preorder ι] (c : ℤ → ComplexShape κ) (r₀ : ℤ) : Type (max u_2 u_3)

This data is a recipe in order to produce a spectral sequence starting on page r₀ (where the rth page is of shape c r) from a spectral object indexed by ι. The object on page r at the position pq : κ shall be E^(deg pq)(i₀ ≤ i₁ ≤ i₂ ≤ i₃), where i₀ ≤ i₁ ≤ i₂ ≤ i₃ are elements in the index type ι of the spectral object and deg pq : ℤ is a cohomological degree. The indices i₀ and i₃ depend on r and pq, but i₁, i₂ only depend on pq. Various conditions are added in order to construct the differentials on the pages and show that the homology of a page identifies to the next page; in certain cases, additional conditions may be required on the spectral object.

• deg : κ → ℤ

  The cohomological degree of objects in the pages

• i₀ (r : ℤ) (pq : κ) (hr : r₀ ≤ r := by lia) : ι

  The zeroth index

• i₁ (pq : κ) : ι

  The first index

• i₂ (pq : κ) : ι

  The second index

• i₃ (r : ℤ) (pq : κ) (hr : r₀ ≤ r := by lia) : ι

  The third index

• le₀₁ (r : ℤ) (pq : κ) (hr : r₀ ≤ r := by lia) : self.i₀ r pq ⋯ ≤ self.i₁ pq
• le₁₂ (pq : κ) : self.i₁ pq ≤ self.i₂ pq
• le₂₃ (r : ℤ) (pq : κ) (hr : r₀ ≤ r := by lia) : self.i₂ pq ≤ self.i₃ r pq ⋯
• hc (r : ℤ) (pq pq' : κ) (hpq : (c r).Rel pq pq') (hr : r₀ ≤ r := by lia) : self.deg pq + 1 = self.deg pq'
• hc₀₂ (r : ℤ) (pq pq' : κ) (hpq : (c r).Rel pq pq') (hr : r₀ ≤ r := by lia) : self.i₀ r pq ⋯ = self.i₂ pq'
• hc₁₃ (r : ℤ) (pq pq' : κ) (hpq : (c r).Rel pq pq') (hr : r₀ ≤ r := by lia) : self.i₁ pq = self.i₃ r pq' ⋯
• antitone_i₀ (r r' : ℤ) (pq : κ) (hr : r₀ ≤ r := by lia) (hrr' : r ≤ r' := by lia) : self.i₀ r' pq ⋯ ≤ self.i₀ r pq ⋯
• monotone_i₃ (r r' : ℤ) (pq : κ) (hr : r₀ ≤ r := by lia) (hrr' : r ≤ r' := by lia) : self.i₃ r pq ⋯ ≤ self.i₃ r' pq ⋯
• i₀_prev (r r' : ℤ) (pq pq' : κ) (hpq : (c r).Rel pq pq') (hrr' : r + 1 = r' := by lia) (hr : r₀ ≤ r := by lia) : self.i₀ r' pq ⋯ = self.i₁ pq'
• i₃_next (r r' : ℤ) (pq pq' : κ) (hpq : (c r).Rel pq pq') (hrr' : r + 1 = r' := by lia) (hr : r₀ ≤ r := by lia) : self.i₃ r' pq' ⋯ = self.i₂ pq

theorem CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀_le {ι : Type u_2} {κ : Type u_3} [Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : SpectralSequenceDataCore ι c r₀) (r r' : ℤ) (pq : κ) (hrr' : r + 1 = r' := by lia) (hr : r₀ ≤ r := by lia) : data.i₀ r' pq ⋯ ≤ data.i₀ r pq ⋯

theorem CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₃_le {ι : Type u_2} {κ : Type u_3} [Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : SpectralSequenceDataCore ι c r₀) (r r' : ℤ) (pq : κ) (hrr' : r + 1 = r' := by lia) (hr : r₀ ≤ r := by lia) : data.i₃ r pq ⋯ ≤ data.i₃ r' pq ⋯

theorem CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀_le' {ι : Type u_2} {κ : Type u_3} [Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : SpectralSequenceDataCore ι c r₀) {r r' : ℤ} (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq' : κ) {i₀' i₀ : ι} (hi₀' : i₀' = data.i₀ r' pq' ⋯) (hi₀ : i₀ = data.i₀ r pq' ⋯) : i₀' ≤ i₀

theorem CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₀₁' {ι : Type u_2} {κ : Type u_3} [Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : SpectralSequenceDataCore ι c r₀) (r : ℤ) (hr : r₀ ≤ r) (pq' : κ) {i₀ i₁ : ι} (hi₀ : i₀ = data.i₀ r pq' ⋯) (hi₁ : i₁ = data.i₁ pq') : i₀ ≤ i₁

theorem CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂' {ι : Type u_2} {κ : Type u_3} [Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : SpectralSequenceDataCore ι c r₀) (pq' : κ) {i₁ i₂ : ι} (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') : i₁ ≤ i₂

theorem CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₂₃' {ι : Type u_2} {κ : Type u_3} [Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : SpectralSequenceDataCore ι c r₀) (r : ℤ) (hr : r₀ ≤ r) (pq' : κ) {i₂ i₃ : ι} (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯) : i₂ ≤ i₃

theorem CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₃₃' {ι : Type u_2} {κ : Type u_3} [Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : SpectralSequenceDataCore ι c r₀) {r r' : ℤ} (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq' : κ) {i₃ i₃' : ι} (hi₃ : i₃ = data.i₃ r pq' ⋯) (hi₃' : i₃' = data.i₃ r' pq' ⋯) : i₃ ≤ i₃'

def CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological : SpectralSequenceDataCore EInt (fun (r : ℤ) => ComplexShape.up' (r, 1 - r)) 2

The data which allows to construct an E₂-cohomological spectral sequence indexed by ℤ × ℤ from a spectral object indexed by EInt.

Equations

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

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_i₀ (r : ℤ) (pq : ℤ × ℤ) (hr : 2 ≤ r) : coreE₂Cohomological.i₀ r pq hr = WithBotTop.coe (pq.2 - r + 2)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_i₁ (pq : ℤ × ℤ) : coreE₂Cohomological.i₁ pq = WithBotTop.coe pq.2

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_deg (pq : ℤ × ℤ) : coreE₂Cohomological.deg pq = pq.1 + pq.2

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_i₃ (r : ℤ) (pq : ℤ × ℤ) (hr : 2 ≤ r) : coreE₂Cohomological.i₃ r pq hr = WithBotTop.coe (pq.2 + r - 1)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_i₂ (pq : ℤ × ℤ) : coreE₂Cohomological.i₂ pq = WithBotTop.coe (pq.2 + 1)

def CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat : SpectralSequenceDataCore EInt (fun (r : ℤ) => ComplexShape.spectralSequenceNat (r, 1 - r)) 2

The data which allows to construct an E₂-cohomological spectral sequence indexed by ℕ × ℕ from a spectral object indexed by EInt. (Note: additional assumptions on the spectral object are required for the construction of the spectral sequence from this.)

Equations

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

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_i₀ (r : ℤ) (pq : ℕ × ℕ) (hr : 2 ≤ r) : coreE₂CohomologicalNat.i₀ r pq hr = WithBotTop.coe (↑pq.2 - r + 2)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_deg (pq : ℕ × ℕ) : coreE₂CohomologicalNat.deg pq = ↑pq.1 + ↑pq.2

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_i₁ (pq : ℕ × ℕ) : coreE₂CohomologicalNat.i₁ pq = WithBotTop.coe ↑pq.2

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_i₂ (pq : ℕ × ℕ) : coreE₂CohomologicalNat.i₂ pq = WithBotTop.coe (↑pq.2 + 1)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_i₃ (r : ℤ) (pq : ℕ × ℕ) (hr : 2 ≤ r) : coreE₂CohomologicalNat.i₃ r pq hr = WithBotTop.coe (↑pq.2 + r - 1)

def CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin (l : ℕ) : SpectralSequenceDataCore (Fin (l + 1)) (fun (r : ℤ) => ComplexShape.spectralSequenceFin l (r, 1 - r)) 2

The data which allows to construct an E₂-cohomological spectral sequence indexed by ℤ × Fin l from a spectral object indexed by Fin (l + 1).

Equations

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

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin_deg (l : ℕ) (pq : ℤ × Fin l) : (coreE₂CohomologicalFin l).deg pq = pq.1 + ↑↑pq.2

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin_i₂ (l : ℕ) (pq : ℤ × Fin l) : (coreE₂CohomologicalFin l).i₂ pq = pq.2.succ

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin_i₃ (l : ℕ) (r : ℤ) (pq : ℤ × Fin l) (hr : 2 ≤ r) : (coreE₂CohomologicalFin l).i₃ r pq hr = Fin.clamp (↑↑pq.2 + (r - 1)).toNat l

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin_i₀ (l : ℕ) (r : ℤ) (pq : ℤ × Fin l) (hr : 2 ≤ r) : (coreE₂CohomologicalFin l).i₀ r pq hr = ⟨(↑↑pq.2 - (r - 2)).toNat, ⋯⟩

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin_i₁ (l : ℕ) (pq : ℤ × Fin l) : (coreE₂CohomologicalFin l).i₁ pq = pq.2.castSucc

def CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat : SpectralSequenceDataCore EInt (fun (r : ℤ) => ComplexShape.spectralSequenceNat (-r, r - 1)) 2

The data which allows to construct an E₂-homological spectral sequence indexed by ℕ × ℕ from a spectral object indexed by EInt. (Note: additional assumptions on the spectral object are required for the construction of the spectral sequence from this.)

Equations

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

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_deg (pq : ℕ × ℕ) : coreE₂HomologicalNat.deg pq = -↑pq.1 - ↑pq.2

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_i₂ (pq : ℕ × ℕ) : coreE₂HomologicalNat.i₂ pq = WithBotTop.coe (-↑pq.2 + 1)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_i₀ (r : ℤ) (pq : ℕ × ℕ) (hr : 2 ≤ r) : coreE₂HomologicalNat.i₀ r pq hr = WithBotTop.coe (-↑pq.2 - r + 2)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_i₃ (r : ℤ) (pq : ℕ × ℕ) (hr : 2 ≤ r) : coreE₂HomologicalNat.i₃ r pq hr = WithBotTop.coe (-↑pq.2 + r - 1)

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_i₁ (pq : ℕ × ℕ) : coreE₂HomologicalNat.i₁ pq = WithBotTop.coe (-↑pq.2)

class CategoryTheory.Abelian.SpectralObject.HasSpectralSequence {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ} (X : SpectralObject C ι) (data : SpectralSequenceDataCore ι c r₀) : Prop

Given X : SpectralObject C ι and data : SpectralSequenceDataCore ι c r₀, this is the property which allows to construct a spectral sequence by using the recipe given by data. The conditions given allow to show that the homology of a page identifies to the next page.

• isZero_H_obj_mk₁_i₀_le (r r' : ℤ) (pq : κ) (hpq : ∀ (pq' : κ), ¬(c r).Rel pq pq') (n : ℤ) (hn : n = data.deg pq + 1) (hrr' : r + 1 = r' := by lia) (hr : r₀ ≤ r := by lia) : Limits.IsZero ((X.H n).obj (ComposableArrows.mk₁ (homOfLE ⋯)))
• isZero_H_obj_mk₁_i₃_le (r r' : ℤ) (pq : κ) (hpq : ∀ (pq' : κ), ¬(c r).Rel pq' pq) (n : ℤ) (hn : n = data.deg pq - 1) (hrr' : r + 1 = r' := by lia) (hr : r₀ ≤ r := by lia) : Limits.IsZero ((X.H n).obj (ComposableArrows.mk₁ (homOfLE ⋯)))

theorem CategoryTheory.Abelian.SpectralObject.isZero_H_obj_mk₁_i₀_le {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ} (X : SpectralObject C ι) (data : SpectralSequenceDataCore ι c r₀) [X.HasSpectralSequence data] (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq : κ) (hpq : ∀ (pq' : κ), ¬(c r).Rel pq pq') (n : ℤ) (hn : n = data.deg pq + 1) : Limits.IsZero ((X.H n).obj (ComposableArrows.mk₁ (homOfLE ⋯)))

theorem CategoryTheory.Abelian.SpectralObject.isZero_H_obj_mk₁_i₀_le' {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ} (X : SpectralObject C ι) (data : SpectralSequenceDataCore ι c r₀) [X.HasSpectralSequence data] (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq : κ) (hpq : ∀ (pq' : κ), ¬(c r).Rel pq pq') (n : ℤ) (hn : n = data.deg pq + 1) (i₀' i₀ : ι) (hi₀' : i₀' = data.i₀ r' pq ⋯) (hi₀ : i₀ = data.i₀ r pq ⋯) : Limits.IsZero ((X.H n).obj (ComposableArrows.mk₁ (homOfLE ⋯)))

theorem CategoryTheory.Abelian.SpectralObject.isZero_H_obj_mk₁_i₃_le {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ} (X : SpectralObject C ι) (data : SpectralSequenceDataCore ι c r₀) [X.HasSpectralSequence data] (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq : κ) (hpq : ∀ (pq' : κ), ¬(c r).Rel pq' pq) (n : ℤ) (hn : n = data.deg pq - 1) : Limits.IsZero ((X.H n).obj (ComposableArrows.mk₁ (homOfLE ⋯)))

theorem CategoryTheory.Abelian.SpectralObject.isZero_H_obj_mk₁_i₃_le' {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [Category.{v_1, u_1} C] [Abelian C] [Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ} (X : SpectralObject C ι) (data : SpectralSequenceDataCore ι c r₀) [X.HasSpectralSequence data] (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq : κ) (hpq : ∀ (pq' : κ), ¬(c r).Rel pq' pq) (n : ℤ) (hn : n = data.deg pq - 1) (i₃ i₃' : ι) (hi₃ : i₃ = data.i₃ r pq ⋯) (hi₃' : i₃' = data.i₃ r' pq ⋯) : Limits.IsZero ((X.H n).obj (ComposableArrows.mk₁ (homOfLE ⋯)))

instance CategoryTheory.Abelian.SpectralObject.instHasSpectralSequenceEIntProdIntCoreE₂Cohomological {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (E : SpectralObject C EInt) : E.HasSpectralSequence coreE₂Cohomological

instance CategoryTheory.Abelian.SpectralObject.instHasSpectralSequenceFinHAddNatOfNatProdIntCoreE₂CohomologicalFin {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] {l : ℕ} (E : SpectralObject C (Fin (l + 1))) : E.HasSpectralSequence (coreE₂CohomologicalFin l)