Theorems · Theorem · category theory

CategoryTheory.Abelian.SpectralObject.spectralSequence_first_page_d_eq

∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{u_4, 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 : data.HasFirstPageComputation] [inst_4 : 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' : autoParam (n + 1 = n') CategoryTheory.Abelian.SpectralObject.spectralSequence_first_page_d_eq._auto_1),
  ((X.spectralSequence data).page r₀ ⋯).d pq pq' =
    CategoryTheory.CategoryStruct.comp (X.spectralSequenceFirstPageXIso data pq j k hj hk n hn).hom
      (CategoryTheory.CategoryStruct.comp (X.δ (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) n n' hn')
        (X.spectralSequenceFirstPageXIso data pq' i j hi ⋯ n' ⋯).inv)

Defined in

Mathlib.Algebra.Homology.SpectralObject.FirstPage

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianPreorderCategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.HasFirstPageComputationCategoryTheory.Abelian.SpectralObject.HasSpectralSequence