The first page of the spectral sequence of a spectral object

Let ι be a preordered type, X a spectral object in an abelian category indexed by ι. Let data : SpectralSequenceDataCore ι c r₀. Assume that X.HasSpectralSequence data holds. In this file, we introduce a property data.HasFirstPageComputation which allows to "compute" the objects of the r₀th page of the spectral sequence attached to X in terms of objects of the form X.H, and we compute the differential on the first page in terms of X.δ, see spectralSequence_first_page_d_eq.

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

Given data : SpectralSequenceDataCore ι c r₀, this is the property that on the page r₀, indices i₀ and i₁ are equal, and indices i₂ and i₃ are equal. This condition allows to express the objects of the r₀th page of the spectral sequences obtained using a spectral object X indexed by ι and data as objects of the form X.H, see SpectralObject.spectralSequenceFirstPageXIso.

• hi₀₁ (pq : κ) : data.i₀ r₀ pq ⋯ = data.i₁ pq
• hi₂₃ (pq : κ) : data.i₂ pq = data.i₃ r₀ pq ⋯

instance CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.instHasFirstPageComputationEIntProdIntCoreE₂Cohomological : coreE₂Cohomological.HasFirstPageComputation

instance CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.instHasFirstPageComputationEIntProdNatCoreE₂CohomologicalNat : coreE₂CohomologicalNat.HasFirstPageComputation

instance CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.instHasFirstPageComputationEIntProdNatCoreE₂HomologicalNat : coreE₂HomologicalNat.HasFirstPageComputation

noncomputable def CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [Category.{u_4, u_1} C] [Abelian C] [Preorder ι] (X : SpectralObject C ι) {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : SpectralSequenceDataCore ι c r₀) [data.HasFirstPageComputation] [X.HasSpectralSequence data] (pq : κ) (i₁ i₂ : ι) (hi₁ : i₁ = data.i₁ pq) (hi₂ : i₂ = data.i₂ pq) (n : ℤ) (hn : n = data.deg pq) : ((X.spectralSequence data).page r₀ ⋯).X pq ≅ (X.H n).obj (ComposableArrows.mk₁ (homOfLE ⋯))

If data : SpectralSequenceDataCore ι c r₀ is such that data.HasFirstPageComputation holds, this is an isomorphism which allows to "compute" the objects on the r₀th page of the spectral sequence obtained from a spectral object X indexed by ι using data as objects of the form X.H. See also spectralSequence_first_page_d_eq for the relation between the differentials of the first page of the spectral sequence and X.δ.

Equations

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

theorem CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso_hom {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [Category.{u_4, u_1} C] [Abelian C] [Preorder ι] (X : SpectralObject C ι) {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : SpectralSequenceDataCore ι c r₀) [data.HasFirstPageComputation] [X.HasSpectralSequence data] (pq : κ) (i₁ i₂ : ι) (hi₁ : i₁ = data.i₁ pq) (hi₂ : i₂ = data.i₂ pq) (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁').hom = CategoryStruct.comp (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ n₀ n₁ n₂ hn₁' ⋯ ⋯).hom (X.EIsoH (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂).hom

theorem CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso_hom_assoc {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [Category.{u_4, u_1} C] [Abelian C] [Preorder ι] (X : SpectralObject C ι) {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : SpectralSequenceDataCore ι c r₀) [data.HasFirstPageComputation] [X.HasSpectralSequence data] (pq : κ) (i₁ i₂ : ι) (hi₁ : i₁ = data.i₁ pq) (hi₂ : i₂ = data.i₂ pq) (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : (X.H n₁).obj (ComposableArrows.mk₁ (homOfLE ⋯)) ⟶ Z) : CategoryStruct.comp (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁').hom h = CategoryStruct.comp (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ n₀ n₁ n₂ hn₁' ⋯ ⋯).hom (CategoryStruct.comp (X.EIsoH (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂).hom h)

theorem CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso_inv {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [Category.{u_4, u_1} C] [Abelian C] [Preorder ι] (X : SpectralObject C ι) {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : SpectralSequenceDataCore ι c r₀) [data.HasFirstPageComputation] [X.HasSpectralSequence data] (pq : κ) (i₁ i₂ : ι) (hi₁ : i₁ = data.i₁ pq) (hi₂ : i₂ = data.i₂ pq) (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) : (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁').inv = CategoryStruct.comp (X.EIsoH (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂).inv (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ n₀ n₁ n₂ hn₁' ⋯ ⋯).inv

theorem CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso_inv_assoc {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [Category.{u_4, u_1} C] [Abelian C] [Preorder ι] (X : SpectralObject C ι) {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : SpectralSequenceDataCore ι c r₀) [data.HasFirstPageComputation] [X.HasSpectralSequence data] (pq : κ) (i₁ i₂ : ι) (hi₁ : i₁ = data.i₁ pq) (hi₂ : i₂ = data.i₂ pq) (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq) (hn₁ : n₀ + 1 = n₁ := by lia) (hn₂ : n₁ + 1 = n₂ := by lia) {Z : C} (h : ((X.spectralSequence data).page r₀ ⋯).X pq ⟶ Z) : CategoryStruct.comp (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁').inv h = CategoryStruct.comp (X.EIsoH (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂).inv (CategoryStruct.comp (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ n₀ n₁ n₂ hn₁' ⋯ ⋯).inv h)

theorem CategoryTheory.Abelian.SpectralObject.spectralSequence_first_page_d_eq {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [Category.{u_4, u_1} C] [Abelian C] [Preorder ι] (X : SpectralObject C ι) {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : SpectralSequenceDataCore ι c r₀) [data.HasFirstPageComputation] [X.HasSpectralSequence data] (pq pq' : κ) (hpq : (c r₀).Rel pq pq') (i j k : ι) (hi : i = data.i₁ pq') (hj : j = data.i₁ pq) (hk : k = data.i₂ pq) (n n' : ℤ) (hn : n = data.deg pq) (hn' : n + 1 = n' := by lia) : ((X.spectralSequence data).page r₀ ⋯).d pq pq' = CategoryStruct.comp (X.spectralSequenceFirstPageXIso data pq j k hj hk n hn).hom (CategoryStruct.comp (X.δ (homOfLE ⋯) (homOfLE ⋯) n n' hn') (X.spectralSequenceFirstPageXIso data pq' i j hi ⋯ n' ⋯).inv)

theorem CategoryTheory.Abelian.SpectralObject.spectralSequence_first_page_d_eq_assoc {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [Category.{u_4, u_1} C] [Abelian C] [Preorder ι] (X : SpectralObject C ι) {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : SpectralSequenceDataCore ι c r₀) [data.HasFirstPageComputation] [X.HasSpectralSequence data] (pq pq' : κ) (hpq : (c r₀).Rel pq pq') (i j k : ι) (hi : i = data.i₁ pq') (hj : j = data.i₁ pq) (hk : k = data.i₂ pq) (n n' : ℤ) (hn : n = data.deg pq) (hn' : n + 1 = n' := by lia) {Z : C} (h : ((X.spectralSequence data).page r₀ ⋯).X pq' ⟶ Z) : CategoryStruct.comp (((X.spectralSequence data).page r₀ ⋯).d pq pq') h = CategoryStruct.comp (X.spectralSequenceFirstPageXIso data pq j k hj hk n hn).hom (CategoryStruct.comp (X.δ (homOfLE ⋯) (homOfLE ⋯) n n' hn') (CategoryStruct.comp (X.spectralSequenceFirstPageXIso data pq' i j hi ⋯ n' ⋯).inv h))