Basic

📁 Source: Mathlib/Algebra/Homology/SpectralSequence/Basic.lean

Statistics

Metric	Count
Definitions CohomologicalSpectralSequence, CohomologicalSpectralSequenceFin, CohomologicalSpectralSequenceNat, E₂CohomologicalSpectralSequence, E₂CohomologicalSpectralSequenceFin, E₂CohomologicalSpectralSequenceNat, hom, instCategory, iso, page, pageFunctor, pageHomologyNatIso, pageXIsoOfEq	13
Theorems comm, comm_assoc, ext, ext_iff, comp_hom, comp_hom_assoc, hom_ext, hom_ext_iff, id_hom, pageFunctor_map, pageFunctor_obj, pageHomologyNatIso_hom_app, pageHomologyNatIso_inv_app	13
Total	26

CategoryTheory

Definitions

Name	Category	Theorems
CohomologicalSpectralSequence 📖	CompOp	—
CohomologicalSpectralSequenceFin 📖	CompOp	—
CohomologicalSpectralSequenceNat 📖	CompOp	—
E₂CohomologicalSpectralSequence 📖	CompOp	—
E₂CohomologicalSpectralSequenceFin 📖	CompOp	—
E₂CohomologicalSpectralSequenceNat 📖	CompOp	—

CategoryTheory.SpectralSequence

Definitions

Name	Category	Theorems
instCategory 📖	CompOp	7 math math: pageFunctor_map, pageHomologyNatIso_hom_app, pageFunctor_obj, pageHomologyNatIso_inv_app, comp_hom_assoc, comp_hom, id_hom
iso 📖	CompOp	4 math math: pageHomologyNatIso_hom_app, pageHomologyNatIso_inv_app, Hom.comm_assoc, Hom.comm
page 📖	CompOp	8 math math: pageHomologyNatIso_hom_app, pageFunctor_obj, pageHomologyNatIso_inv_app, comp_hom_assoc, Hom.comm_assoc, Hom.comm, comp_hom, id_hom
pageFunctor 📖	CompOp	4 math math: pageFunctor_map, pageHomologyNatIso_hom_app, pageFunctor_obj, pageHomologyNatIso_inv_app
pageHomologyNatIso 📖	CompOp	2 math math: pageHomologyNatIso_hom_app, pageHomologyNatIso_inv_app
pageXIsoOfEq 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_hom 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp CategoryTheory.SpectralSequence CategoryTheory.Category.toCategoryStruct instCategory HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory page	—	—
comp_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory page Hom.hom CategoryTheory.SpectralSequence instCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_hom
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
id_hom 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id CategoryTheory.SpectralSequence CategoryTheory.Category.toCategoryStruct instCategory HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory page	—	—
pageFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.SpectralSequence instCategory HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory pageFunctor Hom.hom	—	—
pageFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.SpectralSequence instCategory HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory pageFunctor page	—	—
pageHomologyNatIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.SpectralSequence instCategory CategoryTheory.Functor.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory pageFunctor HomologicalComplex.homologyFunctor CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.eval CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category pageHomologyNatIso HomologicalComplex.homology page HomologicalComplex.X iso	—	CategoryTheory.categoryWithHomology_of_abelian
pageHomologyNatIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.SpectralSequence instCategory CategoryTheory.Functor.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive HomologicalComplex.instCategory pageFunctor HomologicalComplex.eval HomologicalComplex.homologyFunctor CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category pageHomologyNatIso HomologicalComplex.homology page HomologicalComplex.X iso	—	CategoryTheory.categoryWithHomology_of_abelian

CategoryTheory.SpectralSequence.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	8 math math: CategoryTheory.SpectralSequence.pageFunctor_map, CategoryTheory.SpectralSequence.hom_ext_iff, CategoryTheory.SpectralSequence.comp_hom_assoc, comm_assoc, comm, ext_iff, CategoryTheory.SpectralSequence.comp_hom, CategoryTheory.SpectralSequence.id_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.homology CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.SpectralSequence.page CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc HomologicalComplex.X HomologicalComplex.homologyMap hom CategoryTheory.Iso.hom CategoryTheory.SpectralSequence.iso HomologicalComplex.Hom.f	—	—
comm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.homology CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.SpectralSequence.page CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc HomologicalComplex.homologyMap hom HomologicalComplex.X CategoryTheory.Iso.hom CategoryTheory.SpectralSequence.iso HomologicalComplex.Hom.f	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm
ext 📖	—	hom	—	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian
ext_iff 📖	mathematical	—	hom	—	ext

---

← Back to Index