Theorems · Theorem · category theory

CategoryTheory.SpectralSequence.pageHomologyNatIso_inv_app

∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C] {κ : Type u_2}
  (c : ℤ → ComplexShape κ) (r₀ r r' : ℤ) (pq : κ)
  (hrr' : autoParam (r + 1 = r') CategoryTheory.SpectralSequence.pageHomologyNatIso._auto_1)
  (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence.pageHomologyNatIso._auto_3)
  (X : CategoryTheory.SpectralSequence C c r₀),
  (CategoryTheory.SpectralSequence.pageHomologyNatIso C c r₀ r r' pq hrr' hr).inv.app X = (X.iso r r' pq ⋯ ⋯).inv

Defined in

Mathlib.Algebra.Homology.SpectralSequence.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian