Documentation Verification Report

HomologySequence

📁 Source: Mathlib/Algebra/Homology/DerivedCategory/HomologySequence.lean

Statistics

Metric	Count
Definitions `δ`, `homologyFunctor`, `homologyFunctorFactors`, `homologyFunctorFactorsh`, `instShiftSequenceHomologyFunctorOfNatInt`	5
Theorems `comp_δ`, `comp_δ_assoc`, `epi_homologyMap_mor₁_iff`, `epi_homologyMap_mor₂_iff`, `exact₁`, `exact₂`, `exact₃`, `mono_homologyMap_mor₁_iff`, `mono_homologyMap_mor₂_iff`, `δ_comp`, `δ_comp_assoc`, `instIsHomologicalHomologyFunctor`, `isIso_Qh_map_iff`	13
Total	18

DerivedCategory

Definitions

Name	Category	Theorems
`homologyFunctor` 📖	CompOp	16 math math: `HomologySequence.comp_δ`, `isLE_iff`, `isZero_of_isGE`, `HomologySequence.exact₂`, `HomologySequence.mono_homologyMap_mor₁_iff`, `isZero_of_isLE`, `HomologySequence.comp_δ_assoc`, `HomologySequence.epi_homologyMap_mor₁_iff`, `HomologySequence.mono_homologyMap_mor₂_iff`, `isGE_iff`, `HomologySequence.exact₁`, `instIsHomologicalHomologyFunctor`, `HomologySequence.δ_comp_assoc`, `HomologySequence.δ_comp`, `HomologySequence.exact₃`, `HomologySequence.epi_homologyMap_mor₂_iff`
`homologyFunctorFactors` 📖	CompOp	—
`homologyFunctorFactorsh` 📖	CompOp	—
`instShiftSequenceHomologyFunctorOfNatInt` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsHomologicalHomologyFunctor` 📖	mathematical	—	`CategoryTheory.Functor.IsHomological` `DerivedCategory` `instCategory` `instHasShiftInt` `homologyFunctor` `instHasZeroObject` `instPreadditive` `instAdditiveShiftFunctorInt` `instPretriangulated`	—	`CategoryTheory.Functor.isHomological_of_localization` `AddRightCancelSemigroup.toIsRightCancelAdd` `instHasZeroObject` `instAdditiveShiftFunctorInt` `HomotopyCategory.instHasZeroObject` `CategoryTheory.Abelian.hasZeroObject` `HomotopyCategory.instAdditiveIntUpShiftFunctor` `CategoryTheory.Abelian.hasBinaryBiproducts` `instIsTriangulatedHomotopyCategoryIntUpQh` `instEssSurjArrowHomotopyCategoryIntUpMapArrowQh` `CategoryTheory.categoryWithHomology_of_abelian` `HomotopyCategory.instIsHomologicalIntUpHomologyFunctor`
`isIso_Qh_map_iff` 📖	mathematical	—	`CategoryTheory.IsIso` `DerivedCategory` `instCategory` `CategoryTheory.Functor.obj` `HomotopyCategory` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `instCategoryHomotopyCategory` `Qh` `CategoryTheory.Functor.map` `HomotopyCategory.quasiIso` `CategoryTheory.categoryWithHomology_of_abelian`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.categoryWithHomology_of_abelian` `HomotopyCategory.mem_quasiIso_iff` `CategoryTheory.NatIso.isIso_map_iff` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Localization.inverts` `instIsLocalizationHomotopyCategoryIntUpQhQuasiIso`

DerivedCategory.HomologySequence

Definitions

Name	Category	Theorems
`δ` 📖	CompOp	8 math math: `comp_δ`, `mono_homologyMap_mor₁_iff`, `comp_δ_assoc`, `exact₁`, `δ_comp_assoc`, `δ_comp`, `exact₃`, `epi_homologyMap_mor₂_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_δ` 📖	mathematical	`CategoryTheory.Pretriangulated.Triangle` `DerivedCategory` `DerivedCategory.instCategory` `DerivedCategory.instHasShiftInt` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `DerivedCategory.instHasZeroObject` `DerivedCategory.instPreadditive` `DerivedCategory.instAdditiveShiftFunctorInt` `DerivedCategory.instPretriangulated`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `DerivedCategory.homologyFunctor` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.Functor.map` `CategoryTheory.Pretriangulated.Triangle.mor₂` `δ` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	`DerivedCategory.instHasZeroObject` `DerivedCategory.instAdditiveShiftFunctorInt` `CategoryTheory.Functor.comp_homologySequenceδ` `DerivedCategory.instIsHomologicalHomologyFunctor`
`comp_δ_assoc` 📖	mathematical	`CategoryTheory.Pretriangulated.Triangle` `DerivedCategory` `DerivedCategory.instCategory` `DerivedCategory.instHasShiftInt` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `DerivedCategory.instHasZeroObject` `DerivedCategory.instPreadditive` `DerivedCategory.instAdditiveShiftFunctorInt` `DerivedCategory.instPretriangulated`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `DerivedCategory.homologyFunctor` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Functor.map` `CategoryTheory.Pretriangulated.Triangle.mor₂` `CategoryTheory.Pretriangulated.Triangle.obj₁` `δ` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	`DerivedCategory.instHasZeroObject` `DerivedCategory.instAdditiveShiftFunctorInt` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comp_δ`
`epi_homologyMap_mor₁_iff` 📖	mathematical	`CategoryTheory.Pretriangulated.Triangle` `DerivedCategory` `DerivedCategory.instCategory` `DerivedCategory.instHasShiftInt` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `DerivedCategory.instHasZeroObject` `DerivedCategory.instPreadditive` `DerivedCategory.instAdditiveShiftFunctorInt` `DerivedCategory.instPretriangulated`	`CategoryTheory.Epi` `CategoryTheory.Functor.obj` `DerivedCategory.homologyFunctor` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Functor.map` `CategoryTheory.Pretriangulated.Triangle.mor₁` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Pretriangulated.Triangle.mor₂` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	`DerivedCategory.instHasZeroObject` `DerivedCategory.instAdditiveShiftFunctorInt` `CategoryTheory.Functor.homologySequence_epi_shift_map_mor₁_iff` `DerivedCategory.instIsHomologicalHomologyFunctor`
`epi_homologyMap_mor₂_iff` 📖	mathematical	`CategoryTheory.Pretriangulated.Triangle` `DerivedCategory` `DerivedCategory.instCategory` `DerivedCategory.instHasShiftInt` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `DerivedCategory.instHasZeroObject` `DerivedCategory.instPreadditive` `DerivedCategory.instAdditiveShiftFunctorInt` `DerivedCategory.instPretriangulated`	`CategoryTheory.Epi` `CategoryTheory.Functor.obj` `DerivedCategory.homologyFunctor` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Functor.map` `CategoryTheory.Pretriangulated.Triangle.mor₂` `δ` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	`DerivedCategory.instHasZeroObject` `DerivedCategory.instAdditiveShiftFunctorInt` `CategoryTheory.Functor.homologySequence_epi_shift_map_mor₂_iff` `DerivedCategory.instIsHomologicalHomologyFunctor`
`exact₁` 📖	mathematical	`CategoryTheory.Pretriangulated.Triangle` `DerivedCategory` `DerivedCategory.instCategory` `DerivedCategory.instHasShiftInt` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `DerivedCategory.instHasZeroObject` `DerivedCategory.instPreadditive` `DerivedCategory.instAdditiveShiftFunctorInt` `DerivedCategory.instPretriangulated`	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Functor.obj` `DerivedCategory.homologyFunctor` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.Pretriangulated.Triangle.obj₂` `δ` `CategoryTheory.Functor.map` `CategoryTheory.Pretriangulated.Triangle.mor₁` `δ_comp`	—	`DerivedCategory.instHasZeroObject` `DerivedCategory.instAdditiveShiftFunctorInt` `CategoryTheory.Functor.homologySequence_exact₁` `DerivedCategory.instIsHomologicalHomologyFunctor`
`exact₂` 📖	mathematical	`CategoryTheory.Pretriangulated.Triangle` `DerivedCategory` `DerivedCategory.instCategory` `DerivedCategory.instHasShiftInt` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `DerivedCategory.instHasZeroObject` `DerivedCategory.instPreadditive` `DerivedCategory.instAdditiveShiftFunctorInt` `DerivedCategory.instPretriangulated`	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Functor.obj` `DerivedCategory.homologyFunctor` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Functor.map` `CategoryTheory.Pretriangulated.Triangle.mor₁` `CategoryTheory.Pretriangulated.Triangle.mor₂`	—	`DerivedCategory.instHasZeroObject` `DerivedCategory.instAdditiveShiftFunctorInt` `CategoryTheory.Functor.homologySequence_exact₂` `DerivedCategory.instIsHomologicalHomologyFunctor`
`exact₃` 📖	mathematical	`CategoryTheory.Pretriangulated.Triangle` `DerivedCategory` `DerivedCategory.instCategory` `DerivedCategory.instHasShiftInt` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `DerivedCategory.instHasZeroObject` `DerivedCategory.instPreadditive` `DerivedCategory.instAdditiveShiftFunctorInt` `DerivedCategory.instPretriangulated`	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Functor.obj` `DerivedCategory.homologyFunctor` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.Functor.map` `CategoryTheory.Pretriangulated.Triangle.mor₂` `δ` `comp_δ`	—	`DerivedCategory.instHasZeroObject` `DerivedCategory.instAdditiveShiftFunctorInt` `CategoryTheory.Functor.homologySequence_exact₃` `DerivedCategory.instIsHomologicalHomologyFunctor`
`mono_homologyMap_mor₁_iff` 📖	mathematical	`CategoryTheory.Pretriangulated.Triangle` `DerivedCategory` `DerivedCategory.instCategory` `DerivedCategory.instHasShiftInt` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `DerivedCategory.instHasZeroObject` `DerivedCategory.instPreadditive` `DerivedCategory.instAdditiveShiftFunctorInt` `DerivedCategory.instPretriangulated`	`CategoryTheory.Mono` `CategoryTheory.Functor.obj` `DerivedCategory.homologyFunctor` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Functor.map` `CategoryTheory.Pretriangulated.Triangle.mor₁` `δ` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	`DerivedCategory.instHasZeroObject` `DerivedCategory.instAdditiveShiftFunctorInt` `CategoryTheory.Functor.homologySequence_mono_shift_map_mor₁_iff` `DerivedCategory.instIsHomologicalHomologyFunctor`
`mono_homologyMap_mor₂_iff` 📖	mathematical	`CategoryTheory.Pretriangulated.Triangle` `DerivedCategory` `DerivedCategory.instCategory` `DerivedCategory.instHasShiftInt` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `DerivedCategory.instHasZeroObject` `DerivedCategory.instPreadditive` `DerivedCategory.instAdditiveShiftFunctorInt` `DerivedCategory.instPretriangulated`	`CategoryTheory.Mono` `CategoryTheory.Functor.obj` `DerivedCategory.homologyFunctor` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Functor.map` `CategoryTheory.Pretriangulated.Triangle.mor₂` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.Pretriangulated.Triangle.mor₁` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	`DerivedCategory.instHasZeroObject` `DerivedCategory.instAdditiveShiftFunctorInt` `CategoryTheory.Functor.homologySequence_mono_shift_map_mor₂_iff` `DerivedCategory.instIsHomologicalHomologyFunctor`
`δ_comp` 📖	mathematical	`CategoryTheory.Pretriangulated.Triangle` `DerivedCategory` `DerivedCategory.instCategory` `DerivedCategory.instHasShiftInt` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `DerivedCategory.instHasZeroObject` `DerivedCategory.instPreadditive` `DerivedCategory.instAdditiveShiftFunctorInt` `DerivedCategory.instPretriangulated`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `DerivedCategory.homologyFunctor` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.Pretriangulated.Triangle.obj₂` `δ` `CategoryTheory.Functor.map` `CategoryTheory.Pretriangulated.Triangle.mor₁` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	`DerivedCategory.instHasZeroObject` `DerivedCategory.instAdditiveShiftFunctorInt` `CategoryTheory.Functor.homologySequenceδ_comp` `DerivedCategory.instIsHomologicalHomologyFunctor`
`δ_comp_assoc` 📖	mathematical	`CategoryTheory.Pretriangulated.Triangle` `DerivedCategory` `DerivedCategory.instCategory` `DerivedCategory.instHasShiftInt` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `DerivedCategory.instHasZeroObject` `DerivedCategory.instPreadditive` `DerivedCategory.instAdditiveShiftFunctorInt` `DerivedCategory.instPretriangulated`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `DerivedCategory.homologyFunctor` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Pretriangulated.Triangle.obj₁` `δ` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Functor.map` `CategoryTheory.Pretriangulated.Triangle.mor₁` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive`	—	`DerivedCategory.instHasZeroObject` `DerivedCategory.instAdditiveShiftFunctorInt` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `δ_comp`

---

← Back to Index