Column-filtered total complexes

For a cohomological bicomplex, the stupid truncations in the first degree form the usual decreasing column filtration. Reindexing the truncation bound by p ↦ -p makes this an increasing filtration indexed by ℤ.

The canonical inclusion and maps between nested degree-at-least truncations live in Embedding/StupidTruncGE.lean. This module reindexes that filtration and totalizes its stages.

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

The usual E₂ cohomological spectral-sequence data, with filtration indices in ℤ rather than EInt.

Equations

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

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalInt_i₂ (pq : ℤ × ℤ) : coreE₂CohomologicalInt.i₂ pq = pq.2 + 1

@[simp]

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

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalInt_i₃ (r : ℤ) (pq : ℤ × ℤ) (hr : 2 ≤ r) : coreE₂CohomologicalInt.i₃ r pq hr = pq.2 + r - 1

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalInt_i₁ (pq : ℤ × ℤ) : coreE₂CohomologicalInt.i₁ pq = pq.2

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalInt_i₀ (r : ℤ) (pq : ℤ × ℤ) (hr : 2 ≤ r) : coreE₂CohomologicalInt.i₀ r pq hr = pq.2 - r + 2

instance CategoryTheory.Abelian.SpectralObject.instHasFirstPageComputationIntProdCoreE₂CohomologicalInt : coreE₂CohomologicalInt.HasFirstPageComputation

instance CategoryTheory.Abelian.SpectralObject.instHasSpectralSequenceIntProdCoreE₂CohomologicalInt {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (E : SpectralObject C ℤ) : E.HasSpectralSequence coreE₂CohomologicalInt

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

The cohomological spectral-sequence coordinates for the increasing reindexing of a decreasing column filtration. At the initial page, (p, q) uses the adjacent filtration stages -p-1 ≤ -p; their quotient is column p, and total degree p+q leaves vertical degree q.

Equations

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

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂ColumnFilteredCohomologicalInt_i₃ (r : ℤ) (pq : ℤ × ℤ) (hr : 2 ≤ r) : coreE₂ColumnFilteredCohomologicalInt.i₃ r pq hr = -pq.1 + r - 2

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂ColumnFilteredCohomologicalInt_i₁ (pq : ℤ × ℤ) : coreE₂ColumnFilteredCohomologicalInt.i₁ pq = -pq.1 - 1

@[simp]

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

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂ColumnFilteredCohomologicalInt_i₂ (pq : ℤ × ℤ) : coreE₂ColumnFilteredCohomologicalInt.i₂ pq = -pq.1

@[simp]

theorem CategoryTheory.Abelian.SpectralObject.coreE₂ColumnFilteredCohomologicalInt_i₀ (r : ℤ) (pq : ℤ × ℤ) (hr : 2 ≤ r) : coreE₂ColumnFilteredCohomologicalInt.i₀ r pq hr = -pq.1 - r + 1

instance CategoryTheory.Abelian.SpectralObject.instHasFirstPageComputationIntProdCoreE₂ColumnFilteredCohomologicalInt : coreE₂ColumnFilteredCohomologicalInt.HasFirstPageComputation

instance CategoryTheory.Abelian.SpectralObject.instHasSpectralSequenceIntProdCoreE₂ColumnFilteredCohomologicalInt {C : Type u_1} [Category.{v_1, u_1} C] [Abelian C] (E : SpectralObject C ℤ) : E.HasSpectralSequence coreE₂ColumnFilteredCohomologicalInt

def HomologicalComplex₂.columnFiltrationIndex (p : ℤ) : ℤ

Filtration index at which column p is added in the increasing reindexing of the decreasing column filtration.

Equations

• HomologicalComplex₂.columnFiltrationIndex p = -p

noncomputable def HomologicalComplex₂.columnFiltrationBicomplex {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) : CategoryTheory.Functor ℤ (HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ))

The increasing ℤ-filtration of a cohomological bicomplex obtained by retaining the columns in first degrees at least -p at filtration index p.

Equations

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

noncomputable def HomologicalComplex₂.columnFilteredTotalComplex {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) [∀ (p : ℤ), (K.columnFiltrationBicomplex.obj p).HasTotal (ComplexShape.up ℤ)] : CategoryTheory.Functor ℤ (CochainComplex C ℤ)

Totalize the column filtration of a cohomological bicomplex.

Equations

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

noncomputable def HomologicalComplex₂.columnFilteredTotalι {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) [K.HasTotal (ComplexShape.up ℤ)] [∀ (p : ℤ), (K.columnFiltrationBicomplex.obj p).HasTotal (ComplexShape.up ℤ)] (p : ℤ) : K.columnFilteredTotalComplex.obj p ⟶ K.total (ComplexShape.up ℤ)

The canonical map from a stage of the column-filtered total complex to the total complex of the whole bicomplex. These maps name the intended abutment target even though the pinned SpectralSequence structure itself has no convergence or abutment field.

Equations

• K.columnFilteredTotalι p = HomologicalComplex₂.total.map (HomologicalComplex.stupidTruncGEι K (-p)) (ComplexShape.up ℤ)

theorem HomologicalComplex₂.columnFilteredTotal_map_comp_ι {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) [K.HasTotal (ComplexShape.up ℤ)] [∀ (p : ℤ), (K.columnFiltrationBicomplex.obj p).HasTotal (ComplexShape.up ℤ)] {p q : ℤ} (f : p ⟶ q) : CategoryTheory.CategoryStruct.comp (K.columnFilteredTotalComplex.map f) (K.columnFilteredTotalι q) = K.columnFilteredTotalι p

The filtration-stage maps to the total complex are compatible with the filtration maps.

theorem HomologicalComplex₂.columnFilteredTotal_map_comp_ι_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) [K.HasTotal (ComplexShape.up ℤ)] [∀ (p : ℤ), (K.columnFiltrationBicomplex.obj p).HasTotal (ComplexShape.up ℤ)] {p q : ℤ} (f : p ⟶ q) {Z : CochainComplex C ℤ} (h : K.total (ComplexShape.up ℤ) ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.columnFilteredTotalComplex.map f) (CategoryTheory.CategoryStruct.comp (K.columnFilteredTotalι q) h) = CategoryTheory.CategoryStruct.comp (K.columnFilteredTotalι p) h

The filtration-stage maps to the total complex are compatible with the filtration maps.

noncomputable def HomologicalComplex₂.columnFilteredTotalιNat {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) [K.HasTotal (ComplexShape.up ℤ)] [∀ (p : ℤ), (K.columnFiltrationBicomplex.obj p).HasTotal (ComplexShape.up ℤ)] : K.columnFilteredTotalComplex ⟶ (CategoryTheory.Functor.const ℤ).obj (K.total (ComplexShape.up ℤ))

The compatible filtration-stage maps as a natural transformation to the constant total complex.

Equations

• K.columnFilteredTotalιNat = { app := fun (p : ℤ) => K.columnFilteredTotalι p, naturality := ⋯ }

noncomputable def HomologicalComplex₂.columnFilteredTotalSpectralObject {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) [∀ (p : ℤ), (K.columnFiltrationBicomplex.obj p).HasTotal (ComplexShape.up ℤ)] : CategoryTheory.Abelian.SpectralObject C ℤ

The abelian spectral object associated to the column-filtered total complex of a cohomological bicomplex.

Equations

• K.columnFilteredTotalSpectralObject = HomotopyCategory.filteredComplexSpectralObject K.columnFilteredTotalComplex

noncomputable def HomologicalComplex₂.columnFilteredTotalSpectralSequence {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) [∀ (p : ℤ), (K.columnFiltrationBicomplex.obj p).HasTotal (ComplexShape.up ℤ)] : CategoryTheory.SpectralSequence C (fun (r : ℤ) => ComplexShape.up' (r - 1, 2 - r)) 2

The E₂ cohomological spectral sequence of the column-filtered total complex.

Equations

• K.columnFilteredTotalSpectralSequence = K.columnFilteredTotalSpectralObject.spectralSequence CategoryTheory.Abelian.SpectralObject.coreE₂ColumnFilteredCohomologicalInt