Structures · Algebra
CategoryTheory.Abelian.SpectralObject.HasSpectralSequence
Given X : SpectralObject C ι and data : SpectralSequenceDataCore ι c r₀, this is
the property which allows to construct a spectral sequence by using the recipe given
by data. The conditions given allow to show that the homology of a page identifies
to the next page.
- Shape
- 2 explicit arguments · adds isZero_H_obj_mk₁_i₀_le, isZero_H_obj_mk₁_i₃_le
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by54
- CategoryTheory.Abelian.SpectralObject.spectralSequence
- CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData
- CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData
- CategoryTheory.Abelian.SpectralObject.spectralSequencePageXIso
- CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso
- CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.isLimitKf
- CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.isColimitCc
- CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso_inv
- CategoryTheory.Abelian.SpectralObject.HasSpectralSequence.isZero_H_obj_mk₁_i₀_le
- CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso_hom
- CategoryTheory.Abelian.SpectralObject.HasSpectralSequence.isZero_H_obj_mk₁_i₃_le
- CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.isIso_mapFourδ₄Toδ₃'
- CategoryTheory.Abelian.SpectralObject.isZero_spectralSequence_page_X_of_isZero_H
- CategoryTheory.Abelian.SpectralObject.isZero_H_obj_mk₁_i₃_le'
- CategoryTheory.Abelian.SpectralObject.isZero_spectralSequence_page_X_iff
- CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.isIso_mapFourδ₁Toδ₀'
- CategoryTheory.Abelian.SpectralObject.isZero_H_obj_mk₁_i₀_le'
- CategoryTheory.Abelian.SpectralObject.spectralSequence_first_page_d_eq
- CategoryTheory.Abelian.SpectralObject.spectralSequence_page_d_eq
- CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData_iso_hom
- CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData_left_π
- CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData_right_p
- CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData_left_K
- CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData_right_Q
- CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso_hom_assoc
- CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData_right_Q
- CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData_right_p
- CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso.congr_simp
- CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData_left_i
- CategoryTheory.Abelian.SpectralObject.spectralSequencePageSc'Iso
- CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData_right_homologyIso_eq_left_homologyIso
- CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData_right_ι
- CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyIso'
- CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData_right_H
- CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData_iso_hom
- CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData_iso_inv
- CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc_exact
- CategoryTheory.Abelian.SpectralObject.isZero_H_obj_mk₁_i₃_le
- CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData_right_ι
- CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData_iso_inv
- CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData_left_i
- CategoryTheory.Abelian.SpectralObject.spectralSequence_iso
- CategoryTheory.Abelian.SpectralObject.spectralSequenceHomologyData_right_H
- CategoryTheory.Abelian.SpectralObject.isZero_spectralSequence_page_X_of_isZero_H'
- CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData_left_π
- CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyIso
- CategoryTheory.Abelian.SpectralObject.spectralSequence_first_page_d_eq_assoc
- CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso_inv_assoc
- CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData_left_H
- CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc_exact
Ancestors0
No ancestors.