Documentation Verification Report

HomologySequence

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

Statistics

Metric	Count
Definitions `homologyδOfTriangle`, `δ`, `homologyFunctor`, `homologyFunctorFactors`, `homologyFunctorFactorsh`, `instShiftSequenceHomologyFunctorOfNatInt`	6
Theorems `homologyFunctorFactors_hom_app_homologyδOfTriangle`, `homologyFunctorFactors_hom_app_homologyδOfTriangle_assoc`, `homologyMap_comp_eq_zero_of_distTriang`, `homologyMap_comp_eq_zero_of_distTriang_assoc`, `homologyMap_exact₁_of_distTriang`, `homologyMap_exact₂_of_distTriang`, `homologyMap_exact₃_of_distTriang`, `homologyMap_homologyδOfTriangle`, `homologyMap_homologyδOfTriangle_assoc`, `homologyδOfTriangle_homologyMap`, `homologyδOfTriangle_homologyMap_assoc`, `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`, `homologyFunctorFactors_hom_naturality`, `homologyFunctorFactors_hom_naturality_assoc`, `homologyFunctorFactorsh_hom_app_quotient_obj`, `homologyFunctorFactorsh_hom_app_quotient_obj_assoc`, `homologyFunctorFactorsh_inv_app_quotient_obj`, `homologyFunctorFactorsh_inv_app_quotient_obj_assoc`, `instIsHomologicalHomologyFunctor`, `isIso_Qh_map_iff`, `shiftMap_homologyFunctor_map_Q`, `shiftMap_homologyFunctor_map_Q_assoc`, `shiftMap_homologyFunctor_map_Qh`, `shiftMap_homologyFunctor_map_Qh_assoc`, `shift_homologyFunctor`	35
Total	41

CochainComplex

Definitions

Name	Category	Theorems
`homologyδOfTriangle` 📖	CompOp	8 math math: `homologyMap_homologyδOfTriangle_assoc`, `homologyFunctorFactors_hom_app_homologyδOfTriangle_assoc`, `homologyδOfTriangle_homologyMap_assoc`, `homologyδOfTriangle_homologyMap`, `homologyMap_exact₃_of_distTriang`, `homologyMap_exact₁_of_distTriang`, `homologyMap_homologyδOfTriangle`, `homologyFunctorFactors_hom_app_homologyδOfTriangle`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homologyFunctorFactors_hom_app_homologyδOfTriangle` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Functor.comp` `DerivedCategory` `instCategoryDerivedCategory` `DerivedCategory.Q` `DerivedCategory.homologyFunctor` `CategoryTheory.Pretriangulated.Triangle.obj₃` `instHasShiftInt` `HomologicalComplex.homologyFunctor` `CategoryTheory.categoryWithHomology_of_abelian` `HomologicalComplex.homology` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.CategoryWithHomology.hasHomology` `HomologicalComplex.sc` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `DerivedCategory.homologyFunctorFactors` `homologyδOfTriangle` `DerivedCategory.instHasShiftInt` `CategoryTheory.Pretriangulated.Triangle` `CategoryTheory.Pretriangulated.triangleCategory` `CategoryTheory.Functor.mapTriangle` `DerivedCategory.instCommShiftCochainComplexIntQ` `DerivedCategory.HomologySequence.δ`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instAddLeftMono` `DerivedCategory.shiftMap_homologyFunctor_map_Q` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_app` `CategoryTheory.Category.comp_id`
`homologyFunctorFactors_hom_app_homologyδOfTriangle_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `DerivedCategory` `instCategoryDerivedCategory` `DerivedCategory.homologyFunctor` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `DerivedCategory.Q` `CategoryTheory.Pretriangulated.Triangle.obj₃` `instHasShiftInt` `HomologicalComplex.homologyFunctor` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `DerivedCategory.homologyFunctorFactors` `HomologicalComplex.homology` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.CategoryWithHomology.hasHomology` `HomologicalComplex.sc` `homologyδOfTriangle` `DerivedCategory.instHasShiftInt` `CategoryTheory.Pretriangulated.Triangle` `CategoryTheory.Pretriangulated.triangleCategory` `CategoryTheory.Functor.mapTriangle` `DerivedCategory.instCommShiftCochainComplexIntQ` `DerivedCategory.HomologySequence.δ`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homologyFunctorFactors_hom_app_homologyδOfTriangle`
`homologyMap_comp_eq_zero_of_distTriang` 📖	mathematical	`CategoryTheory.Pretriangulated.Triangle` `DerivedCategory` `instCategoryDerivedCategory` `DerivedCategory.instHasShiftInt` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `DerivedCategory.instHasZeroObject` `DerivedCategory.instPreadditive` `DerivedCategory.instAdditiveShiftFunctorInt` `DerivedCategory.instPretriangulated` `CategoryTheory.Functor.obj` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `instHasShiftInt` `CategoryTheory.Pretriangulated.triangleCategory` `CategoryTheory.Functor.mapTriangle` `DerivedCategory.Q` `DerivedCategory.instCommShiftCochainComplexIntQ`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.homology` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CochainComplex` `HomologicalComplex.instCategory` `instHasShiftInt` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `HomologicalComplex.sc` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Pretriangulated.Triangle.obj₃` `HomologicalComplex.homologyMap` `CategoryTheory.Pretriangulated.Triangle.mor₁` `CategoryTheory.Pretriangulated.Triangle.mor₂` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `DerivedCategory.instHasZeroObject` `DerivedCategory.instAdditiveShiftFunctorInt` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.NatIso.hom_app_isIso` `DerivedCategory.homologyFunctorFactors_hom_naturality_assoc` `DerivedCategory.homologyFunctorFactors_hom_naturality` `CategoryTheory.Functor.map_comp_assoc` `CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂` `CategoryTheory.Functor.map_zero` `CategoryTheory.Functor.IsHomological.toPreservesZeroMorphisms` `DerivedCategory.instIsHomologicalHomologyFunctor` `CategoryTheory.Limits.zero_comp` `CategoryTheory.Limits.comp_zero`
`homologyMap_comp_eq_zero_of_distTriang_assoc` 📖	mathematical	`CategoryTheory.Pretriangulated.Triangle` `DerivedCategory` `instCategoryDerivedCategory` `DerivedCategory.instHasShiftInt` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `DerivedCategory.instHasZeroObject` `DerivedCategory.instPreadditive` `DerivedCategory.instAdditiveShiftFunctorInt` `DerivedCategory.instPretriangulated` `CategoryTheory.Functor.obj` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `instHasShiftInt` `CategoryTheory.Pretriangulated.triangleCategory` `CategoryTheory.Functor.mapTriangle` `DerivedCategory.Q` `DerivedCategory.instCommShiftCochainComplexIntQ`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.homology` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CochainComplex` `HomologicalComplex.instCategory` `instHasShiftInt` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `HomologicalComplex.sc` `CategoryTheory.Pretriangulated.Triangle.obj₂` `HomologicalComplex.homologyMap` `CategoryTheory.Pretriangulated.Triangle.mor₁` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Pretriangulated.Triangle.mor₂` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `DerivedCategory.instHasZeroObject` `DerivedCategory.instAdditiveShiftFunctorInt` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homologyMap_comp_eq_zero_of_distTriang`
`homologyMap_exact₁_of_distTriang` 📖	mathematical	`CategoryTheory.Pretriangulated.Triangle` `DerivedCategory` `instCategoryDerivedCategory` `DerivedCategory.instHasShiftInt` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `DerivedCategory.instHasZeroObject` `DerivedCategory.instPreadditive` `DerivedCategory.instAdditiveShiftFunctorInt` `DerivedCategory.instPretriangulated` `CategoryTheory.Functor.obj` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `instHasShiftInt` `CategoryTheory.Pretriangulated.triangleCategory` `CategoryTheory.Functor.mapTriangle` `DerivedCategory.Q` `DerivedCategory.instCommShiftCochainComplexIntQ`	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `HomologicalComplex.homology` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CochainComplex` `HomologicalComplex.instCategory` `instHasShiftInt` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `HomologicalComplex.sc` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.Pretriangulated.Triangle.obj₂` `homologyδOfTriangle` `HomologicalComplex.homologyMap` `CategoryTheory.Pretriangulated.Triangle.mor₁` `homologyδOfTriangle_homologyMap`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `DerivedCategory.instHasZeroObject` `DerivedCategory.instAdditiveShiftFunctorInt` `CategoryTheory.ShortComplex.exact_of_iso` `DerivedCategory.HomologySequence.δ_comp` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `homologyδOfTriangle_homologyMap` `homologyFunctorFactors_hom_app_homologyδOfTriangle` `DerivedCategory.homologyFunctorFactors_hom_naturality` `DerivedCategory.HomologySequence.exact₁`
`homologyMap_exact₂_of_distTriang` 📖	mathematical	`CategoryTheory.Pretriangulated.Triangle` `DerivedCategory` `instCategoryDerivedCategory` `DerivedCategory.instHasShiftInt` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `DerivedCategory.instHasZeroObject` `DerivedCategory.instPreadditive` `DerivedCategory.instAdditiveShiftFunctorInt` `DerivedCategory.instPretriangulated` `CategoryTheory.Functor.obj` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `instHasShiftInt` `CategoryTheory.Pretriangulated.triangleCategory` `CategoryTheory.Functor.mapTriangle` `DerivedCategory.Q` `DerivedCategory.instCommShiftCochainComplexIntQ`	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `HomologicalComplex.homology` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CochainComplex` `HomologicalComplex.instCategory` `instHasShiftInt` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `HomologicalComplex.sc` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Pretriangulated.Triangle.obj₃` `HomologicalComplex.homologyMap` `CategoryTheory.Pretriangulated.Triangle.mor₁` `CategoryTheory.Pretriangulated.Triangle.mor₂` `homologyMap_comp_eq_zero_of_distTriang`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `DerivedCategory.instHasZeroObject` `DerivedCategory.instAdditiveShiftFunctorInt` `CategoryTheory.ShortComplex.exact_of_iso` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `homologyMap_comp_eq_zero_of_distTriang` `DerivedCategory.homologyFunctorFactors_hom_naturality` `DerivedCategory.HomologySequence.exact₂`
`homologyMap_exact₃_of_distTriang` 📖	mathematical	`CategoryTheory.Pretriangulated.Triangle` `DerivedCategory` `instCategoryDerivedCategory` `DerivedCategory.instHasShiftInt` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `DerivedCategory.instHasZeroObject` `DerivedCategory.instPreadditive` `DerivedCategory.instAdditiveShiftFunctorInt` `DerivedCategory.instPretriangulated` `CategoryTheory.Functor.obj` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `instHasShiftInt` `CategoryTheory.Pretriangulated.triangleCategory` `CategoryTheory.Functor.mapTriangle` `DerivedCategory.Q` `DerivedCategory.instCommShiftCochainComplexIntQ`	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `HomologicalComplex.homology` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CochainComplex` `HomologicalComplex.instCategory` `instHasShiftInt` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `HomologicalComplex.sc` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Pretriangulated.Triangle.obj₁` `HomologicalComplex.homologyMap` `CategoryTheory.Pretriangulated.Triangle.mor₂` `homologyδOfTriangle` `homologyMap_homologyδOfTriangle`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `DerivedCategory.instHasZeroObject` `DerivedCategory.instAdditiveShiftFunctorInt` `CategoryTheory.ShortComplex.exact_of_iso` `DerivedCategory.HomologySequence.comp_δ` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `homologyMap_homologyδOfTriangle` `DerivedCategory.homologyFunctorFactors_hom_naturality` `homologyFunctorFactors_hom_app_homologyδOfTriangle` `DerivedCategory.HomologySequence.exact₃`
`homologyMap_homologyδOfTriangle` 📖	mathematical	`CategoryTheory.Pretriangulated.Triangle` `DerivedCategory` `instCategoryDerivedCategory` `DerivedCategory.instHasShiftInt` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `DerivedCategory.instHasZeroObject` `DerivedCategory.instPreadditive` `DerivedCategory.instAdditiveShiftFunctorInt` `DerivedCategory.instPretriangulated` `CategoryTheory.Functor.obj` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `instHasShiftInt` `CategoryTheory.Pretriangulated.triangleCategory` `CategoryTheory.Functor.mapTriangle` `DerivedCategory.Q` `DerivedCategory.instCommShiftCochainComplexIntQ`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.homology` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CochainComplex` `HomologicalComplex.instCategory` `instHasShiftInt` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `HomologicalComplex.sc` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Pretriangulated.Triangle.obj₁` `HomologicalComplex.homologyMap` `CategoryTheory.Pretriangulated.Triangle.mor₂` `homologyδOfTriangle` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `DerivedCategory.instHasZeroObject` `DerivedCategory.instAdditiveShiftFunctorInt` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.NatIso.hom_app_isIso` `homologyFunctorFactors_hom_app_homologyδOfTriangle` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `DerivedCategory.HomologySequence.comp_δ` `CategoryTheory.Limits.zero_comp` `CategoryTheory.Limits.comp_zero`
`homologyMap_homologyδOfTriangle_assoc` 📖	mathematical	`CategoryTheory.Pretriangulated.Triangle` `DerivedCategory` `instCategoryDerivedCategory` `DerivedCategory.instHasShiftInt` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `DerivedCategory.instHasZeroObject` `DerivedCategory.instPreadditive` `DerivedCategory.instAdditiveShiftFunctorInt` `DerivedCategory.instPretriangulated` `CategoryTheory.Functor.obj` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `instHasShiftInt` `CategoryTheory.Pretriangulated.triangleCategory` `CategoryTheory.Functor.mapTriangle` `DerivedCategory.Q` `DerivedCategory.instCommShiftCochainComplexIntQ`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.homology` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CochainComplex` `HomologicalComplex.instCategory` `instHasShiftInt` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `HomologicalComplex.sc` `CategoryTheory.Pretriangulated.Triangle.obj₃` `HomologicalComplex.homologyMap` `CategoryTheory.Pretriangulated.Triangle.mor₂` `CategoryTheory.Pretriangulated.Triangle.obj₁` `homologyδOfTriangle` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `DerivedCategory.instHasZeroObject` `DerivedCategory.instAdditiveShiftFunctorInt` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homologyMap_homologyδOfTriangle`
`homologyδOfTriangle_homologyMap` 📖	mathematical	`CategoryTheory.Pretriangulated.Triangle` `DerivedCategory` `instCategoryDerivedCategory` `DerivedCategory.instHasShiftInt` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `DerivedCategory.instHasZeroObject` `DerivedCategory.instPreadditive` `DerivedCategory.instAdditiveShiftFunctorInt` `DerivedCategory.instPretriangulated` `CategoryTheory.Functor.obj` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `instHasShiftInt` `CategoryTheory.Pretriangulated.triangleCategory` `CategoryTheory.Functor.mapTriangle` `DerivedCategory.Q` `DerivedCategory.instCommShiftCochainComplexIntQ`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.homology` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CochainComplex` `HomologicalComplex.instCategory` `instHasShiftInt` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `HomologicalComplex.sc` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CategoryTheory.Pretriangulated.Triangle.obj₂` `homologyδOfTriangle` `HomologicalComplex.homologyMap` `CategoryTheory.Pretriangulated.Triangle.mor₁` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `DerivedCategory.instHasZeroObject` `DerivedCategory.instAdditiveShiftFunctorInt` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.NatIso.hom_app_isIso` `homologyFunctorFactors_hom_app_homologyδOfTriangle_assoc` `DerivedCategory.homologyFunctorFactors_hom_naturality` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `DerivedCategory.HomologySequence.δ_comp` `CategoryTheory.Limits.zero_comp` `CategoryTheory.Limits.comp_zero`
`homologyδOfTriangle_homologyMap_assoc` 📖	mathematical	`CategoryTheory.Pretriangulated.Triangle` `DerivedCategory` `instCategoryDerivedCategory` `DerivedCategory.instHasShiftInt` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `DerivedCategory.instHasZeroObject` `DerivedCategory.instPreadditive` `DerivedCategory.instAdditiveShiftFunctorInt` `DerivedCategory.instPretriangulated` `CategoryTheory.Functor.obj` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `instHasShiftInt` `CategoryTheory.Pretriangulated.triangleCategory` `CategoryTheory.Functor.mapTriangle` `DerivedCategory.Q` `DerivedCategory.instCommShiftCochainComplexIntQ`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.homology` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CochainComplex` `HomologicalComplex.instCategory` `instHasShiftInt` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `HomologicalComplex.sc` `CategoryTheory.Pretriangulated.Triangle.obj₁` `homologyδOfTriangle` `CategoryTheory.Pretriangulated.Triangle.obj₂` `HomologicalComplex.homologyMap` `CategoryTheory.Pretriangulated.Triangle.mor₁` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `DerivedCategory.instHasZeroObject` `DerivedCategory.instAdditiveShiftFunctorInt` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homologyδOfTriangle_homologyMap`

DerivedCategory

Definitions

Name	Category	Theorems
`homologyFunctor` 📖	CompOp	29 math math: `HomologySequence.comp_δ`, `isLE_iff`, `isZero_of_isGE`, `HomologySequence.exact₂`, `homologyFunctorFactorsh_hom_app_quotient_obj_assoc`, `homologyFunctorFactors_hom_naturality`, `shiftMap_homologyFunctor_map_Q_assoc`, `CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle_assoc`, `HomologySequence.mono_homologyMap_mor₁_iff`, `isZero_of_isLE`, `shiftMap_homologyFunctor_map_Qh_assoc`, `HomologySequence.comp_δ_assoc`, `HomologySequence.epi_homologyMap_mor₁_iff`, `HomologySequence.mono_homologyMap_mor₂_iff`, `isGE_iff`, `HomologySequence.exact₁`, `shift_homologyFunctor`, `homologyFunctorFactorsh_hom_app_quotient_obj`, `shiftMap_homologyFunctor_map_Q`, `shiftMap_homologyFunctor_map_Qh`, `instIsHomologicalHomologyFunctor`, `homologyFunctorFactorsh_inv_app_quotient_obj_assoc`, `HomologySequence.δ_comp_assoc`, `HomologySequence.δ_comp`, `homologyFunctorFactorsh_inv_app_quotient_obj`, `HomologySequence.exact₃`, `HomologySequence.epi_homologyMap_mor₂_iff`, `CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle`, `homologyFunctorFactors_hom_naturality_assoc`
`homologyFunctorFactors` 📖	CompOp	10 math math: `homologyFunctorFactorsh_hom_app_quotient_obj_assoc`, `homologyFunctorFactors_hom_naturality`, `shiftMap_homologyFunctor_map_Q_assoc`, `CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle_assoc`, `homologyFunctorFactorsh_hom_app_quotient_obj`, `shiftMap_homologyFunctor_map_Q`, `homologyFunctorFactorsh_inv_app_quotient_obj_assoc`, `homologyFunctorFactorsh_inv_app_quotient_obj`, `CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle`, `homologyFunctorFactors_hom_naturality_assoc`
`homologyFunctorFactorsh` 📖	CompOp	6 math math: `homologyFunctorFactorsh_hom_app_quotient_obj_assoc`, `shiftMap_homologyFunctor_map_Qh_assoc`, `homologyFunctorFactorsh_hom_app_quotient_obj`, `shiftMap_homologyFunctor_map_Qh`, `homologyFunctorFactorsh_inv_app_quotient_obj_assoc`, `homologyFunctorFactorsh_inv_app_quotient_obj`
`instShiftSequenceHomologyFunctorOfNatInt` 📖	CompOp	5 math math: `shiftMap_homologyFunctor_map_Q_assoc`, `shiftMap_homologyFunctor_map_Qh_assoc`, `shift_homologyFunctor`, `shiftMap_homologyFunctor_map_Q`, `shiftMap_homologyFunctor_map_Qh`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homologyFunctorFactors_hom_naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `DerivedCategory` `instCategoryDerivedCategory` `homologyFunctor` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `Q` `HomologicalComplex.homologyFunctor` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.Functor.map` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `homologyFunctorFactors` `HomologicalComplex.homology` `CategoryTheory.CategoryWithHomology.hasHomology` `HomologicalComplex.sc` `HomologicalComplex.homologyMap`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.NatTrans.naturality` `CategoryTheory.categoryWithHomology_of_abelian`
`homologyFunctorFactors_hom_naturality_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `DerivedCategory` `instCategoryDerivedCategory` `homologyFunctor` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `Q` `CategoryTheory.Functor.map` `HomologicalComplex.homologyFunctor` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `homologyFunctorFactors` `HomologicalComplex.homologyMap` `CategoryTheory.CategoryWithHomology.hasHomology` `HomologicalComplex.sc`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homologyFunctorFactors_hom_naturality`
`homologyFunctorFactorsh_hom_app_quotient_obj` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `HomotopyCategory` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `instIsRightCancelAddOfAddRightReflectLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `Int.instAddCommSemigroup` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Int.instAddCommMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instLinearOrder` `Int.instAddLeftMono` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `instCategoryHomotopyCategory` `CategoryTheory.Functor.comp` `DerivedCategory` `instCategoryDerivedCategory` `Qh` `homologyFunctor` `HomotopyCategory.homologyFunctor` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `homologyFunctorFactorsh` `CategoryTheory.Functor.obj` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex.instCategory` `HomotopyCategory.quotient` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Q` `CategoryTheory.Functor.map` `quotientCompQhIso` `CochainComplex` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.homologyFunctor` `homologyFunctorFactors` `CategoryTheory.Iso.inv` `HomotopyCategory.homologyFunctorFactors`	—	`HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_hom_app_quotient_obj` `CategoryTheory.categoryWithHomology_of_abelian`
`homologyFunctorFactorsh_hom_app_quotient_obj_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `DerivedCategory` `instCategoryDerivedCategory` `homologyFunctor` `HomotopyCategory` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `instIsRightCancelAddOfAddRightReflectLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `Int.instAddCommSemigroup` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Int.instAddCommMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instLinearOrder` `Int.instAddLeftMono` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `instCategoryHomotopyCategory` `Qh` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex.instCategory` `HomotopyCategory.quotient` `HomotopyCategory.homologyFunctor` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `homologyFunctorFactorsh` `Q` `CategoryTheory.Functor.map` `quotientCompQhIso` `CochainComplex` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.homologyFunctor` `homologyFunctorFactors` `CategoryTheory.Iso.inv` `HomotopyCategory.homologyFunctorFactors`	—	`instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instAddLeftMono` `CategoryTheory.categoryWithHomology_of_abelian` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homologyFunctorFactorsh_hom_app_quotient_obj`
`homologyFunctorFactorsh_inv_app_quotient_obj` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `HomotopyCategory` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `instIsRightCancelAddOfAddRightReflectLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `Int.instAddCommSemigroup` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Int.instAddCommMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instLinearOrder` `Int.instAddLeftMono` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `instCategoryHomotopyCategory` `HomotopyCategory.homologyFunctor` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.Functor.comp` `DerivedCategory` `instCategoryDerivedCategory` `Qh` `homologyFunctor` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `homologyFunctorFactorsh` `CategoryTheory.Functor.obj` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex.instCategory` `HomotopyCategory.quotient` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.homologyFunctor` `CategoryTheory.Iso.hom` `HomotopyCategory.homologyFunctorFactors` `CochainComplex` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `Q` `homologyFunctorFactors` `CategoryTheory.Functor.map` `quotientCompQhIso`	—	`HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_inv_app_quotient_obj` `CategoryTheory.categoryWithHomology_of_abelian`
`homologyFunctorFactorsh_inv_app_quotient_obj_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `HomotopyCategory` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `instIsRightCancelAddOfAddRightReflectLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `Int.instAddCommSemigroup` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Int.instAddCommMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instLinearOrder` `Int.instAddLeftMono` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `instCategoryHomotopyCategory` `HomotopyCategory.homologyFunctor` `CategoryTheory.categoryWithHomology_of_abelian` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex.instCategory` `HomotopyCategory.quotient` `DerivedCategory` `instCategoryDerivedCategory` `homologyFunctor` `Qh` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.inv` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `homologyFunctorFactorsh` `HomologicalComplex.homologyFunctor` `CategoryTheory.Iso.hom` `HomotopyCategory.homologyFunctorFactors` `CochainComplex` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `Q` `homologyFunctorFactors` `CategoryTheory.Functor.map` `quotientCompQhIso`	—	`instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instAddLeftMono` `CategoryTheory.categoryWithHomology_of_abelian` `AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `homologyFunctorFactorsh_inv_app_quotient_obj`
`instIsHomologicalHomologyFunctor` 📖	mathematical	—	`CategoryTheory.Functor.IsHomological` `DerivedCategory` `instCategoryDerivedCategory` `instHasShiftInt` `homologyFunctor` `instHasZeroObject` `instPreadditive` `instAdditiveShiftFunctorInt` `instPretriangulated`	—	`CategoryTheory.Functor.isHomological_of_localization` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instAddLeftMono` `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` `instCategoryDerivedCategory` `CategoryTheory.Functor.obj` `HomotopyCategory` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `instIsRightCancelAddOfAddRightReflectLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `Int.instAddCommSemigroup` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Int.instAddCommMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instLinearOrder` `Int.instAddLeftMono` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `instCategoryHomotopyCategory` `Qh` `CategoryTheory.Functor.map` `HomotopyCategory.quasiIso` `CategoryTheory.categoryWithHomology_of_abelian`	—	`instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instAddLeftMono` `CategoryTheory.categoryWithHomology_of_abelian` `HomotopyCategory.mem_quasiIso_iff` `CategoryTheory.NatIso.isIso_map_iff` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Localization.inverts` `instIsLocalizationHomotopyCategoryIntUpQhQuasiIso`
`shiftMap_homologyFunctor_map_Q` 📖	mathematical	—	`CategoryTheory.Functor.shiftMap` `DerivedCategory` `instCategoryDerivedCategory` `homologyFunctor` `Int.instAddMonoid` `instHasShiftInt` `instShiftSequenceHomologyFunctorOfNatInt` `CategoryTheory.Functor.obj` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `Q` `CategoryTheory.ShiftedHom.map` `CochainComplex.instHasShiftInt` `instCommShiftCochainComplexIntQ` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.comp` `HomologicalComplex.homologyFunctor` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `homologyFunctorFactors` `HomologicalComplex` `instIsRightCancelAddOfAddRightReflectLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `Int.instAddCommSemigroup` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Int.instAddCommMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instLinearOrder` `Int.instAddLeftMono` `CategoryTheory.Functor.shift` `CochainComplex.instShiftSequenceHomologicalComplexIntUpHomologyFunctorOfNat` `CategoryTheory.Iso.inv`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.categoryWithHomology_of_abelian` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instAddLeftMono` `zero_add` `add_zero` `CategoryTheory.ShiftedHom.map_naturality_1` `instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso` `CategoryTheory.ShiftedHom.mk₀_comp` `CategoryTheory.ShiftedHom.comp_mk₀` `CategoryTheory.Functor.shiftMap_comp'` `CategoryTheory.Functor.shiftMap_comp` `CategoryTheory.ShiftedHom.comp_map` `shiftMap_homologyFunctor_map_Qh` `homologyFunctorFactorsh_hom_app_quotient_obj` `homologyFunctorFactorsh_inv_app_quotient_obj` `HomotopyCategory.homologyFunctor_shiftMap` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_app_assoc` `CategoryTheory.Iso.inv_hom_id_app` `CategoryTheory.Functor.map_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp`
`shiftMap_homologyFunctor_map_Q_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `DerivedCategory` `instCategoryDerivedCategory` `CategoryTheory.Functor.shift` `homologyFunctor` `Int.instAddMonoid` `instHasShiftInt` `instShiftSequenceHomologyFunctorOfNatInt` `CochainComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `HomologicalComplex.instCategory` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelSemigroup.toIsRightCancelAdd` `Q` `CategoryTheory.Functor.shiftMap` `CategoryTheory.ShiftedHom.map` `CochainComplex.instHasShiftInt` `instCommShiftCochainComplexIntQ` `HomologicalComplex.homologyFunctor` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `homologyFunctorFactors` `HomologicalComplex` `instIsRightCancelAddOfAddRightReflectLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `Int.instAddCommSemigroup` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Int.instAddCommMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instLinearOrder` `Int.instAddLeftMono` `CochainComplex.instShiftSequenceHomologicalComplexIntUpHomologyFunctorOfNat` `CategoryTheory.Iso.inv`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.categoryWithHomology_of_abelian` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instAddLeftMono` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `shiftMap_homologyFunctor_map_Q`
`shiftMap_homologyFunctor_map_Qh` 📖	mathematical	—	`CategoryTheory.Functor.shiftMap` `DerivedCategory` `instCategoryDerivedCategory` `homologyFunctor` `Int.instAddMonoid` `instHasShiftInt` `instShiftSequenceHomologyFunctorOfNatInt` `CategoryTheory.Functor.obj` `HomotopyCategory` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `instIsRightCancelAddOfAddRightReflectLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `Int.instAddCommSemigroup` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Int.instAddCommMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instLinearOrder` `Int.instAddLeftMono` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `instCategoryHomotopyCategory` `Qh` `CategoryTheory.ShiftedHom.map` `HomotopyCategory.hasShift` `instCommShiftHomotopyCategoryIntUpQh` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.comp` `HomotopyCategory.homologyFunctor` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.NatTrans.app` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `homologyFunctorFactorsh` `CategoryTheory.Functor.shift` `HomotopyCategory.instShiftSequenceIntUpHomologyFunctorOfNat` `CategoryTheory.Iso.inv`	—	`instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instAddLeftMono` `CategoryTheory.Functor.ShiftSequence.induced_shiftMap` `CategoryTheory.categoryWithHomology_of_abelian` `instFullFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh` `instFaithfulFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh`
`shiftMap_homologyFunctor_map_Qh_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `DerivedCategory` `instCategoryDerivedCategory` `CategoryTheory.Functor.shift` `homologyFunctor` `Int.instAddMonoid` `instHasShiftInt` `instShiftSequenceHomologyFunctorOfNatInt` `HomotopyCategory` `CategoryTheory.Abelian.toPreadditive` `ComplexShape.up` `instIsRightCancelAddOfAddRightReflectLE` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `instLatticeInt` `contravariant_swap_add_of_contravariant_add` `Preorder.toLE` `PartialOrder.toPreorder` `Int.instAddCommSemigroup` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Int.instAddCommMonoid` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instSemiring` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instLinearOrder` `Int.instAddLeftMono` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `instCategoryHomotopyCategory` `Qh` `CategoryTheory.Functor.shiftMap` `CategoryTheory.ShiftedHom.map` `HomotopyCategory.hasShift` `instCommShiftHomotopyCategoryIntUpQh` `HomotopyCategory.homologyFunctor` `CategoryTheory.categoryWithHomology_of_abelian` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor.comp` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `homologyFunctorFactorsh` `HomotopyCategory.instShiftSequenceIntUpHomologyFunctorOfNat` `CategoryTheory.Iso.inv`	—	`instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Int.instIsStrictOrderedRing` `contravariant_lt_of_covariant_le` `Int.instAddLeftMono` `CategoryTheory.categoryWithHomology_of_abelian` `Mathlib.Tactic.Reassoc.eq_whisker'` `shiftMap_homologyFunctor_map_Qh`
`shift_homologyFunctor` 📖	mathematical	—	`CategoryTheory.Functor.shift` `DerivedCategory` `instCategoryDerivedCategory` `homologyFunctor` `Int.instAddMonoid` `instHasShiftInt` `instShiftSequenceHomologyFunctorOfNatInt`	—	—

DerivedCategory.HomologySequence

Definitions

Name	Category	Theorems
`δ` 📖	CompOp	10 math math: `comp_δ`, `CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle_assoc`, `mono_homologyMap_mor₁_iff`, `comp_δ_assoc`, `exact₁`, `δ_comp_assoc`, `δ_comp`, `exact₃`, `epi_homologyMap_mor₂_iff`, `CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_δ` 📖	mathematical	`CategoryTheory.Pretriangulated.Triangle` `DerivedCategory` `instCategoryDerivedCategory` `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` `instCategoryDerivedCategory` `DerivedCategory.homologyFunctor` `CategoryTheory.Pretriangulated.Triangle.obj₂` `DerivedCategory.instHasShiftInt` `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` `instCategoryDerivedCategory` `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` `instCategoryDerivedCategory` `DerivedCategory.homologyFunctor` `CategoryTheory.Pretriangulated.Triangle.obj₂` `DerivedCategory.instHasShiftInt` `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` `instCategoryDerivedCategory` `DerivedCategory.instHasShiftInt` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `DerivedCategory.instHasZeroObject` `DerivedCategory.instPreadditive` `DerivedCategory.instAdditiveShiftFunctorInt` `DerivedCategory.instPretriangulated`	`CategoryTheory.Epi` `CategoryTheory.Functor.obj` `DerivedCategory` `instCategoryDerivedCategory` `DerivedCategory.homologyFunctor` `CategoryTheory.Pretriangulated.Triangle.obj₁` `DerivedCategory.instHasShiftInt` `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` `instCategoryDerivedCategory` `DerivedCategory.instHasShiftInt` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `DerivedCategory.instHasZeroObject` `DerivedCategory.instPreadditive` `DerivedCategory.instAdditiveShiftFunctorInt` `DerivedCategory.instPretriangulated`	`CategoryTheory.Epi` `CategoryTheory.Functor.obj` `DerivedCategory` `instCategoryDerivedCategory` `DerivedCategory.homologyFunctor` `CategoryTheory.Pretriangulated.Triangle.obj₂` `DerivedCategory.instHasShiftInt` `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` `instCategoryDerivedCategory` `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` `instCategoryDerivedCategory` `DerivedCategory.homologyFunctor` `CategoryTheory.Pretriangulated.Triangle.obj₃` `DerivedCategory.instHasShiftInt` `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` `instCategoryDerivedCategory` `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` `instCategoryDerivedCategory` `DerivedCategory.homologyFunctor` `CategoryTheory.Pretriangulated.Triangle.obj₁` `DerivedCategory.instHasShiftInt` `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` `instCategoryDerivedCategory` `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` `instCategoryDerivedCategory` `DerivedCategory.homologyFunctor` `CategoryTheory.Pretriangulated.Triangle.obj₂` `DerivedCategory.instHasShiftInt` `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` `instCategoryDerivedCategory` `DerivedCategory.instHasShiftInt` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `DerivedCategory.instHasZeroObject` `DerivedCategory.instPreadditive` `DerivedCategory.instAdditiveShiftFunctorInt` `DerivedCategory.instPretriangulated`	`CategoryTheory.Mono` `CategoryTheory.Functor.obj` `DerivedCategory` `instCategoryDerivedCategory` `DerivedCategory.homologyFunctor` `CategoryTheory.Pretriangulated.Triangle.obj₁` `DerivedCategory.instHasShiftInt` `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` `instCategoryDerivedCategory` `DerivedCategory.instHasShiftInt` `Set` `Set.instMembership` `CategoryTheory.Pretriangulated.distinguishedTriangles` `DerivedCategory.instHasZeroObject` `DerivedCategory.instPreadditive` `DerivedCategory.instAdditiveShiftFunctorInt` `DerivedCategory.instPretriangulated`	`CategoryTheory.Mono` `CategoryTheory.Functor.obj` `DerivedCategory` `instCategoryDerivedCategory` `DerivedCategory.homologyFunctor` `CategoryTheory.Pretriangulated.Triangle.obj₂` `DerivedCategory.instHasShiftInt` `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` `instCategoryDerivedCategory` `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` `instCategoryDerivedCategory` `DerivedCategory.homologyFunctor` `CategoryTheory.Pretriangulated.Triangle.obj₃` `DerivedCategory.instHasShiftInt` `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` `instCategoryDerivedCategory` `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` `instCategoryDerivedCategory` `DerivedCategory.homologyFunctor` `CategoryTheory.Pretriangulated.Triangle.obj₃` `DerivedCategory.instHasShiftInt` `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