Comparison of spectral sequences on later pages #
A morphism f : E ⟶ E' of spectral sequences commutes with the identifications of the homology
of a page with the next page. Hence if f is an isomorphism on every object of the rth page,
it is an isomorphism on the homology of the rth page, so on every object of the (r + 1)st
page, and, by induction, on every object of every page r' ≥ r.
Main results #
CategoryTheory.SpectralSequence.Hom.isIso_hom_f_of_le: the comparison on later pages.
theorem
CategoryTheory.SpectralSequence.Hom.isIso_hom_f_of_le
{C : Type u_1}
{κ : Type u_2}
[Category.{v_1, u_1} C]
[Abelian C]
{c : ℤ → ComplexShape κ}
{r₀ : ℤ}
{E E' : SpectralSequence C c r₀}
(f : E ⟶ E')
(r : ℤ)
(hr : r₀ ≤ r)
(h : ∀ (pq : κ), IsIso ((f.hom r hr).f pq))
(r' : ℤ)
(hrr' : r ≤ r')
(pq : κ)
:
A morphism of spectral sequences which is an isomorphism on every object of the rth page is
an isomorphism on every object of every page r' ≥ r.