Theorems · Theorem · category theory

CategoryTheory.Abelian.SpectralObject.spectralSequence_page_d_eq

∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : X.HasSpectralSequence data] (r : ℤ) (hr : r₀ ≤ r) (pq pq' : κ) (hpq : (c r).Rel pq pq')
  {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅)
  (h₀ : i₀ = data.i₀ r pq' ⋯) (h₁ : i₁ = data.i₁ pq') (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₂ n₃ : ℤ) (hn₁' : n₁ = data.deg pq)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.spectralSequence_page_d_eq._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.spectralSequence_page_d_eq._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.spectralSequence_page_d_eq._auto_5),
  ((X.spectralSequence data).page r ⋯).d pq pq' =
    CategoryTheory.CategoryStruct.comp
      (X.spectralSequencePageXIso data r hr pq i₂ i₃ i₄ i₅ h₂ h₃ h₄ h₅ n₀ n₁ n₂ hn₁' ⋯ ⋯).hom
      (CategoryTheory.CategoryStruct.comp (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃)
        (X.spectralSequencePageXIso data r hr pq' i₀ i₁ i₂ i₃ h₀ h₁ ⋯ ⋯ n₁ n₂ n₃ ⋯ ⋯ ⋯).inv)

Defined in

Mathlib.Algebra.Homology.SpectralObject.SpectralSequence

Cited by

1 results in Mathlib

Foundations

Depth 131 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianPreorderCategoryTheory.Abelian.SpectralObject.HasSpectralSequence