Documentation Verification Report

SpectralSequence

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

Statistics

Metric	Count
Definitions `isLimitKf`, `kf`, `kfSc`, `page`, `pageD`, `pageX`, `pageXIso`, `shortComplexIso`, `SpectralSequence`	9
Theorems `instMonoFKfSc`, `isIso_mapFourδ₁Toδ₀'`, `kfSc_X₁`, `kfSc_X₂`, `kfSc_X₃`, `kfSc_exact`, `kfSc_f`, `kfSc_g`, `kf_w`, `pageD_eq`, `pageD_pageD`, `pageD_pageD_assoc`, `page_X`, `page_d`	14
Total	23

CategoryTheory

Definitions

Name	Category	Theorems
`SpectralSequence` 📖	CompData	7 math math: `SpectralSequence.pageFunctor_map`, `SpectralSequence.pageHomologyNatIso_hom_app`, `SpectralSequence.pageFunctor_obj`, `SpectralSequence.pageHomologyNatIso_inv_app`, `SpectralSequence.comp_hom_assoc`, `SpectralSequence.comp_hom`, `SpectralSequence.id_hom`

CategoryTheory.Abelian.SpectralObject.SpectralSequence

Definitions

Name	Category	Theorems
`page` 📖	CompOp	3 math math: `HomologyData.kf_w`, `page_d`, `page_X`
`pageD` 📖	CompOp	5 math math: `HomologyData.kfSc_g`, `page_d`, `pageD_pageD`, `pageD_eq`, `pageD_pageD_assoc`
`pageX` 📖	CompOp	8 math math: `HomologyData.kf_w`, `HomologyData.kfSc_f`, `pageD_pageD`, `HomologyData.kfSc_X₃`, `page_X`, `HomologyData.kfSc_X₂`, `pageD_eq`, `pageD_pageD_assoc`
`pageXIso` 📖	CompOp	3 math math: `HomologyData.kf_w`, `HomologyData.kfSc_f`, `pageD_eq`
`shortComplexIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pageD_eq` 📖	mathematical	`ComplexShape.Rel` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₁` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₂` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₃` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.deg`	`pageD` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pageX` `CategoryTheory.Abelian.SpectralObject.E` `Preorder.smallCategory` `CategoryTheory.homOfLE` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₀₁'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₂₃'` `CategoryTheory.Iso.hom` `pageXIso` `CategoryTheory.Abelian.SpectralObject.d` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₀₁'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₂₃'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂` `CategoryTheory.Category.id_comp`
`pageD_pageD` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pageX` `pageD` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	`CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₀₁'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₂₃'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₂₃` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc₁₃` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc₀₂` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₀₁` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂` `pageD_eq` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_assoc` `CategoryTheory.Abelian.SpectralObject.d_d_assoc` `CategoryTheory.Limits.zero_comp` `CategoryTheory.Limits.comp_zero`
`pageD_pageD_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pageX` `pageD` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `pageD_pageD`
`page_X` 📖	mathematical	—	`HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `page` `pageX`	—	—
`page_d` 📖	mathematical	—	`HomologicalComplex.d` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `page` `pageD`	—	—

CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData

Definitions

Name	Category	Theorems
`isLimitKf` 📖	CompOp	—
`kf` 📖	CompOp	—
`kfSc` 📖	CompOp	7 math math: `kfSc_exact`, `kfSc_g`, `kfSc_f`, `kfSc_X₃`, `kfSc_X₂`, `instMonoFKfSc`, `kfSc_X₁`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instMonoFKfSc` 📖	mathematical	`CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₁` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₂` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₃` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.deg`	`CategoryTheory.Mono` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `kfSc` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.ShortComplex.f`	—	`CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₂₃'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₀₁'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀_le'` `CategoryTheory.mono_comp` `CategoryTheory.Abelian.SpectralObject.instMonoMapFourδ₁Toδ₀` `LE.le.trans` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.Iso.isIso_inv`
`isIso_mapFourδ₁Toδ₀'` 📖	mathematical	`ComplexShape.next` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₁` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₂` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₃` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.deg` `ComplexShape.Rel`	`CategoryTheory.IsIso` `CategoryTheory.Abelian.SpectralObject.E` `Preorder.smallCategory` `CategoryTheory.homOfLE` `LE.le.trans` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀_le'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₀₁'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₂₃'` `CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'`	—	`CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₁Toδ₀_of_isZero` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀_le'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₀₁'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₂₃'` `LE.le.trans` `CategoryTheory.Abelian.SpectralObject.isZero_H_obj_mk₁_i₀_le'` `ComplexShape.next_eq'`
`kfSc_X₁` 📖	mathematical	`CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₁` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₂` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₃` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.deg`	`CategoryTheory.ShortComplex.X₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `kfSc` `CategoryTheory.Abelian.SpectralObject.E` `Preorder.smallCategory` `CategoryTheory.homOfLE` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₂₃'`	—	—
`kfSc_X₂` 📖	mathematical	`CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₁` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₂` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₃` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.deg`	`CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `kfSc` `CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageX`	—	—
`kfSc_X₃` 📖	mathematical	`CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₁` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₂` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₃` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.deg`	`CategoryTheory.ShortComplex.X₃` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `kfSc` `CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageX`	—	—
`kfSc_exact` 📖	mathematical	`ComplexShape.next` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₁` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₂` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₃` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.deg`	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `kfSc`	—	`CategoryTheory.ShortComplex.exact_of_iso` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀_prev` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₀₁` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀_le'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₀₁'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₂₃'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc₀₂` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc₁₃` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc` `LE.le.trans` `CategoryTheory.Category.id_comp` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD_eq` `CategoryTheory.Abelian.SpectralObject.dKernelSequence_exact` `CategoryTheory.ShortComplex.exact_iff_epi` `CategoryTheory.Abelian.hasZeroObject` `HomologicalComplex.shape` `isIso_mapFourδ₁Toδ₀'` `CategoryTheory.epi_comp` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.Iso.isIso_inv`
`kfSc_f` 📖	mathematical	`CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₁` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₂` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₃` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.deg`	`CategoryTheory.ShortComplex.f` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `kfSc` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Abelian.SpectralObject.E` `Preorder.smallCategory` `CategoryTheory.homOfLE` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₂₃'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₀₁'` `CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageX` `CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀_le'` `CategoryTheory.Iso.inv` `CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageXIso`	—	`CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₂₃'`
`kfSc_g` 📖	mathematical	`CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₁` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₂` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₃` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.deg`	`CategoryTheory.ShortComplex.g` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `kfSc` `CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD`	—	—
`kf_w` 📖	mathematical	`CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₁` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₂` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₃` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.deg`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Abelian.SpectralObject.E` `Preorder.smallCategory` `CategoryTheory.homOfLE` `LE.le.trans` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀_le'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₀₁'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₂₃'` `CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageX` `HomologicalComplex.X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Abelian.SpectralObject.SpectralSequence.page` `CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'` `CategoryTheory.Iso.inv` `CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageXIso` `HomologicalComplex.d` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`LE.le.trans` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀_le'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₀₁'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₂₃'` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀_prev` `CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₀₁` `CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD_eq` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_assoc` `CategoryTheory.Abelian.SpectralObject.map_fourδ₁Toδ₀_d_assoc` `CategoryTheory.Limits.zero_comp` `HomologicalComplex.shape` `CategoryTheory.Limits.comp_zero`

---

← Back to Index