Basic

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

Statistics

Metric	Count
Definitions DerivedCategory, Q, Qh, instCommShiftCochainComplexIntQ, instCommShiftHomotopyCategoryIntUpQh, instHasShiftInt, instPreadditive, instPretriangulated, quotientCompQhIso, singleFunctor, singleFunctorIsoCompQ, singleFunctors, singleFunctorsPostcompQIso, singleFunctorsPostcompQhIso, HasDerivedCategory, standard, instCategoryDerivedCategory	17
Theorems Q_map_eq_of_homotopy, Qh_obj_singleFunctors_obj, instAdditiveCochainComplexIntQ, instAdditiveHomotopyCategoryIntUpQh, instAdditiveShiftFunctorInt, instAdditiveSingleFunctor, instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, instEssSurjArrowHomotopyCategoryIntUpMapArrowQh, instEssSurjCochainComplexIntQ, instEssSurjHomotopyCategoryIntUpQh, instFaithfulFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, instFullFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, instHasZeroObject, instIsIsoMapCochainComplexIntQOfQuasiIso, instIsLocalizationCochainComplexIntQQuasiIsoUp, instIsLocalizationHomotopyCategoryIntUpQhQuasiIso, instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic, instIsTriangulated, instIsTriangulatedHomotopyCategoryIntUpQh, isIso_Q_map_iff_quasiIso, mappingCocone_triangle_distinguished, mappingCone_triangle_distinguished, mem_distTriang_iff, singleFunctorsPostcompQIso_hom_hom, singleFunctorsPostcompQIso_inv_hom	25
Total	42

DerivedCategory

Definitions

Name	Category	Theorems
Q 📖	CompOp	60 math math: instIsLocalizationCochainComplexIntQQuasiIsoUp, right_fac, instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, singleFunctorsPostcompQIso_inv_hom, subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE, homologyFunctorFactorsh_hom_app_quotient_obj_assoc, homologyFunctorFactors_hom_naturality, shiftMap_homologyFunctor_map_Q_assoc, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle_assoc, triangleOfSES_mor₁, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, mappingCone_triangle_distinguished, to_singleFunctor_obj_eq_zero_of_injective, right_fac_of_isStrictlyLE_of_isStrictlyGE, instIsIsoMapCochainComplexIntQOfQuasiIso, triangleOfSES_obj₃, instLinearCochainComplexIntQ, CategoryTheory.ProjectiveResolution.extMk_hom, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, triangleOfSES.map_hom₁, CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors, left_fac_of_isStrictlyLE_of_isStrictlyGE, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃, CochainComplex.HomComplex.CohomologyClass.equiv_toSmallShiftedHom_mk, isLE_Q_obj_iff, triangleOfSES_obj₁, isGE_Q_obj_iff, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁, instIsGEObjCochainComplexIntQOfIsGE, exists_iso_Q_obj_of_isGE_of_isLE, triangleOfSES.map_hom₃, from_singleFunctor_obj_eq_zero_of_projective, exists_iso_Q_obj_of_isGE, homologyFunctorFactorsh_hom_app_quotient_obj, CategoryTheory.InjectiveResolution.extMk_hom, right_fac_of_isStrictlyLE, shiftMap_homologyFunctor_map_Q, instAdditiveCochainComplexIntQ, triangleOfSES.map_hom₂, exists_iso_Q_obj_of_isLE, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, triangleOfSES_obj₂, instEssSurjCochainComplexIntQ, singleFunctorsPostcompQIso_hom_hom, triangleOfSES_mor₂, homologyFunctorFactorsh_inv_app_quotient_obj_assoc, homologyFunctorFactorsh_inv_app_quotient_obj, mem_distTriang_iff, instIsLEObjCochainComplexIntQOfIsLE, mappingCocone_triangle_distinguished, Q_map_eq_of_homotopy, isIso_Q_map_iff_quasiIso, left_fac_of_isStrictlyGE, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle, CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app, homologyFunctorFactors_hom_naturality_assoc, left_fac
Qh 📖	CompOp	22 math math: instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, CochainComplex.IsKInjective.Qh_map_bijective, homologyFunctorFactorsh_hom_app_quotient_obj_assoc, CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh, instIsTriangulatedHomotopyCategoryIntUpQh, shiftMap_homologyFunctor_map_Qh_assoc, instAdditiveHomotopyCategoryIntUpQh, instIsLocalizationHomotopyCategoryIntUpQhQuasiIso, CochainComplex.IsKProjective.Qh_map_bijective, instEssSurjHomotopyCategoryIntUpQh, instFaithfulFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, instEssSurjArrowHomotopyCategoryIntUpMapArrowQh, homologyFunctorFactorsh_hom_app_quotient_obj, Qh_obj_singleFunctors_obj, instFullFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, shiftMap_homologyFunctor_map_Qh, instLinearHomotopyCategoryIntUpQh, homologyFunctorFactorsh_inv_app_quotient_obj_assoc, homologyFunctorFactorsh_inv_app_quotient_obj, isIso_Qh_map_iff, CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app, instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic
instCommShiftCochainComplexIntQ 📖	CompOp	22 math math: instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, singleFunctorsPostcompQIso_inv_hom, shiftMap_homologyFunctor_map_Q_assoc, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle_assoc, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, mappingCone_triangle_distinguished, CategoryTheory.ProjectiveResolution.extMk_hom, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃, CochainComplex.HomComplex.CohomologyClass.equiv_toSmallShiftedHom_mk, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁, CategoryTheory.InjectiveResolution.extMk_hom, shiftMap_homologyFunctor_map_Q, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, singleFunctorsPostcompQIso_hom_hom, mem_distTriang_iff, mappingCocone_triangle_distinguished, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle
instCommShiftHomotopyCategoryIntUpQh 📖	CompOp	5 math math: instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh, instIsTriangulatedHomotopyCategoryIntUpQh, shiftMap_homologyFunctor_map_Qh_assoc, shiftMap_homologyFunctor_map_Qh
instHasShiftInt 📖	CompOp	79 math math: CategoryTheory.Abelian.Ext.homLinearEquiv_apply, instIsTriangulated, instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, HomologySequence.comp_δ, CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, CategoryTheory.Abelian.Ext.smul_hom, singleFunctorsPostcompQIso_inv_hom, HomologySequence.exact₂, shiftMap_homologyFunctor_map_Q_assoc, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle_assoc, triangleOfSES_mor₁, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CategoryTheory.Abelian.Ext.mk₀_hom, mappingCone_triangle_distinguished, HomologySequence.mono_homologyMap_mor₁_iff, CategoryTheory.Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply, CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh, CategoryTheory.ShortComplex.ShortExact.singleTriangle.map_hom₁, instIsTriangulatedHomotopyCategoryIntUpQh, shiftMap_homologyFunctor_map_Qh_assoc, triangleOfSES_obj₃, CategoryTheory.Abelian.Ext.singleFunctor_map_comp_hom, CategoryTheory.ProjectiveResolution.extMk_hom, CategoryTheory.Abelian.Ext.mapExactFunctor_hom, CategoryTheory.Abelian.Ext.homEquiv_chgUniv, HomologySequence.comp_δ_assoc, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, triangleOfSES.map_hom₁, CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors, CategoryTheory.ShortComplex.ShortExact.singleTriangle.map_hom₂, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃, CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₂, CategoryTheory.ShortComplex.ShortExact.singleTriangle_mor₃, CategoryTheory.ShortComplex.ShortExact.singleTriangle_mor₁, CategoryTheory.Abelian.Ext.hom_comp_singleFunctor_map_shift, HomologySequence.epi_homologyMap_mor₁_iff, CochainComplex.HomComplex.CohomologyClass.equiv_toSmallShiftedHom_mk, CategoryTheory.Functor.instIsTriangulatedDerivedCategoryMapDerivedCategory, HomologySequence.mono_homologyMap_mor₂_iff, CategoryTheory.Abelian.Ext.homAddEquiv_apply, triangleOfSES_obj₁, instAdditiveShiftFunctorInt, CategoryTheory.ShortComplex.ShortExact.singleTriangle_mor₂, CategoryTheory.Abelian.Ext.add_hom, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁, CategoryTheory.Abelian.Ext.zero_hom, CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₁, instLinearShiftFunctorInt, triangleOfSES.map_hom₃, HomologySequence.exact₁, shift_homologyFunctor, CategoryTheory.InjectiveResolution.extMk_hom, triangleOfSES_mor₃, shiftMap_homologyFunctor_map_Q, CategoryTheory.Abelian.Ext.neg_hom, triangleOfSES_distinguished, triangleOfSES.map_hom₂, CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₃, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, CategoryTheory.hasExt_iff, triangleOfSES_obj₂, singleFunctorsPostcompQIso_hom_hom, shiftMap_homologyFunctor_map_Qh, triangleOfSES_mor₂, CategoryTheory.ShortComplex.ShortExact.singleTriangle_distinguished, instIsHomologicalHomologyFunctor, CategoryTheory.ShortComplex.ShortExact.singleTriangle.map_hom₃, CategoryTheory.Abelian.Ext.homLinearEquiv_symm_apply, HomologySequence.δ_comp_assoc, HomologySequence.δ_comp, mem_distTriang_iff, mappingCocone_triangle_distinguished, HomologySequence.exact₃, HomologySequence.epi_homologyMap_mor₂_iff, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle, CategoryTheory.Abelian.Ext.comp_hom
instPreadditive 📖	CompOp	29 math math: CategoryTheory.Abelian.Ext.homLinearEquiv_apply, instIsTriangulated, CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, CategoryTheory.Abelian.Ext.smul_hom, mappingCone_triangle_distinguished, CategoryTheory.Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply, instIsTriangulatedHomotopyCategoryIntUpQh, to_singleFunctor_obj_eq_zero_of_injective, instLinearCochainComplexIntQ, instAdditiveHomotopyCategoryIntUpQh, CategoryTheory.Functor.instIsTriangulatedDerivedCategoryMapDerivedCategory, CategoryTheory.Abelian.Ext.homAddEquiv_apply, instAdditiveShiftFunctorInt, CategoryTheory.Abelian.Ext.add_hom, CategoryTheory.Abelian.Ext.zero_hom, instLinearShiftFunctorInt, from_singleFunctor_obj_eq_zero_of_projective, CategoryTheory.Abelian.Ext.neg_hom, triangleOfSES_distinguished, instAdditiveCochainComplexIntQ, instAdditiveSingleFunctor, instLinearSingleFunctor, CategoryTheory.ShortComplex.ShortExact.singleTriangle_distinguished, instIsHomologicalHomologyFunctor, instLinearHomotopyCategoryIntUpQh, CategoryTheory.Abelian.Ext.homLinearEquiv_symm_apply, mem_distTriang_iff, mappingCocone_triangle_distinguished, CategoryTheory.Functor.instLinearDerivedCategoryMapDerivedCategory
instPretriangulated 📖	CompOp	9 math math: instIsTriangulated, mappingCone_triangle_distinguished, instIsTriangulatedHomotopyCategoryIntUpQh, CategoryTheory.Functor.instIsTriangulatedDerivedCategoryMapDerivedCategory, triangleOfSES_distinguished, CategoryTheory.ShortComplex.ShortExact.singleTriangle_distinguished, instIsHomologicalHomologyFunctor, mem_distTriang_iff, mappingCocone_triangle_distinguished
quotientCompQhIso 📖	CompOp	6 math math: instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, homologyFunctorFactorsh_hom_app_quotient_obj_assoc, homologyFunctorFactorsh_hom_app_quotient_obj, homologyFunctorFactorsh_inv_app_quotient_obj_assoc, homologyFunctorFactorsh_inv_app_quotient_obj, CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app
singleFunctor 📖	CompOp	37 math math: CategoryTheory.Abelian.Ext.homLinearEquiv_apply, CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, CategoryTheory.Abelian.Ext.smul_hom, instFaithfulSingleFunctor, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CategoryTheory.Abelian.Ext.mk₀_hom, CategoryTheory.Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply, CategoryTheory.ShortComplex.ShortExact.singleTriangle.map_hom₁, CategoryTheory.Abelian.Ext.singleFunctor_map_comp_hom, CategoryTheory.ProjectiveResolution.extMk_hom, CategoryTheory.Abelian.Ext.mapExactFunctor_hom, CategoryTheory.Abelian.Ext.homEquiv_chgUniv, CategoryTheory.ShortComplex.ShortExact.singleTriangle.map_hom₂, CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₂, CategoryTheory.ShortComplex.ShortExact.singleTriangle_mor₁, CategoryTheory.Abelian.Ext.hom_comp_singleFunctor_map_shift, instFullSingleFunctor, CategoryTheory.Abelian.Ext.homAddEquiv_apply, CategoryTheory.ShortComplex.ShortExact.singleTriangle_mor₂, CategoryTheory.Abelian.Ext.add_hom, CategoryTheory.Abelian.Ext.zero_hom, instIsLEObjSingleFunctor, exists_iso_singleFunctor_obj_of_isGE_of_isLE, CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₁, CategoryTheory.instSmallHomDerivedCategoryObjSingleFunctorOfHasExt, CategoryTheory.InjectiveResolution.extMk_hom, CategoryTheory.Abelian.Ext.neg_hom, instAdditiveSingleFunctor, Qh_obj_singleFunctors_obj, CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₃, CategoryTheory.hasExt_iff, instLinearSingleFunctor, CategoryTheory.ShortComplex.ShortExact.singleTriangle.map_hom₃, CategoryTheory.Abelian.Ext.homLinearEquiv_symm_apply, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, instIsGEObjSingleFunctor, CategoryTheory.Abelian.Ext.comp_hom
singleFunctorIsoCompQ 📖	CompOp	4 math math: CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CategoryTheory.ProjectiveResolution.extMk_hom, CategoryTheory.InjectiveResolution.extMk_hom, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom
singleFunctors 📖	CompOp	8 math math: singleFunctorsPostcompQIso_inv_hom, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, singleFunctorsPostcompQIso_hom_hom
singleFunctorsPostcompQIso 📖	CompOp	8 math math: singleFunctorsPostcompQIso_inv_hom, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, singleFunctorsPostcompQIso_hom_hom
singleFunctorsPostcompQhIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Q_map_eq_of_homotopy 📖	mathematical	—	CategoryTheory.Functor.map 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 instCategoryDerivedCategory Q	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplexUpToQuasiIso.Q_map_eq_of_homotopy CategoryTheory.categoryWithHomology_of_abelian instQFactorsThroughHomotopyIntUp CategoryTheory.Abelian.hasBinaryBiproducts
Qh_obj_singleFunctors_obj 📖	mathematical	—	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 DerivedCategory instCategoryDerivedCategory Qh CategoryTheory.SingleFunctors.functor Int.instAddMonoid HomotopyCategory.hasShift HomotopyCategory.singleFunctors CategoryTheory.Abelian.hasZeroObject singleFunctor	—	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.Abelian.hasZeroObject
instAdditiveCochainComplexIntQ 📖	mathematical	—	CategoryTheory.Functor.Additive CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing DerivedCategory HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd instCategoryDerivedCategory HomologicalComplex.instPreadditive instPreadditive Q	—	CategoryTheory.Functor.additive_of_iso AddRightCancelSemigroup.toIsRightCancelAdd 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.instAdditiveComp HomotopyCategory.instAdditiveHomologicalComplexQuotient instAdditiveHomotopyCategoryIntUpQh
instAdditiveHomotopyCategoryIntUpQh 📖	mathematical	—	CategoryTheory.Functor.Additive 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 DerivedCategory instCategoryHomotopyCategory instCategoryDerivedCategory HomotopyCategory.instPreadditive instPreadditive Qh	—	CategoryTheory.Localization.functor_additive 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 HomotopyCategory.instHasZeroObject CategoryTheory.Abelian.hasZeroObject HomotopyCategory.instAdditiveIntUpShiftFunctor CategoryTheory.Abelian.hasBinaryBiproducts instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic CategoryTheory.ObjectProperty.instHasLeftCalculusOfFractionsTrWOfIsTriangulatedOfIsTriangulated HomotopyCategory.instIsTriangulatedIntUp HomotopyCategory.instIsTriangulatedIntUpSubcategoryAcyclic
instAdditiveShiftFunctorInt 📖	mathematical	—	CategoryTheory.Functor.Additive DerivedCategory instCategoryDerivedCategory instPreadditive CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt	—	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.Localization.functor_additive_iff HomotopyCategory.instHasZeroObject CategoryTheory.Abelian.hasZeroObject HomotopyCategory.instAdditiveIntUpShiftFunctor CategoryTheory.Abelian.hasBinaryBiproducts instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic CategoryTheory.ObjectProperty.instHasLeftCalculusOfFractionsTrWOfIsTriangulatedOfIsTriangulated HomotopyCategory.instIsTriangulatedIntUp HomotopyCategory.instIsTriangulatedIntUpSubcategoryAcyclic instAdditiveHomotopyCategoryIntUpQh CategoryTheory.Functor.additive_of_iso CategoryTheory.Functor.instAdditiveComp
instAdditiveSingleFunctor 📖	mathematical	—	CategoryTheory.Functor.Additive DerivedCategory instCategoryDerivedCategory CategoryTheory.Abelian.toPreadditive instPreadditive singleFunctor	—	CategoryTheory.Abelian.hasZeroObject CategoryTheory.Functor.instAdditiveComp HomotopyCategory.instAdditiveIntUpSingleFunctor instAdditiveHomotopyCategoryIntUpQh
instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso 📖	mathematical	—	CategoryTheory.NatTrans.CommShift HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 DerivedCategory HomologicalComplex.instCategory instCategoryDerivedCategory CategoryTheory.Functor.comp HomotopyCategory instCategoryHomotopyCategory HomotopyCategory.quotient Qh Q CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category quotientCompQhIso Int.instAddMonoid CochainComplex.instHasShiftInt instHasShiftInt CategoryTheory.Functor.CommShift.comp HomotopyCategory.hasShift HomotopyCategory.commShiftQuotient instCommShiftHomotopyCategoryIntUpQh instCommShiftCochainComplexIntQ	—	CategoryTheory.Functor.CommShift.ofIso_compatibility 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
instEssSurjArrowHomotopyCategoryIntUpMapArrowQh 📖	mathematical	—	CategoryTheory.Functor.EssSurj CategoryTheory.Arrow 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 DerivedCategory instCategoryDerivedCategory CategoryTheory.instCategoryArrow CategoryTheory.Functor.mapArrow Qh	—	CategoryTheory.Localization.essSurj_mapArrow 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 HomotopyCategory.instHasZeroObject CategoryTheory.Abelian.hasZeroObject HomotopyCategory.instAdditiveIntUpShiftFunctor CategoryTheory.Abelian.hasBinaryBiproducts instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic CategoryTheory.ObjectProperty.instHasLeftCalculusOfFractionsTrWOfIsTriangulatedOfIsTriangulated HomotopyCategory.instIsTriangulatedIntUp HomotopyCategory.instIsTriangulatedIntUpSubcategoryAcyclic
instEssSurjCochainComplexIntQ 📖	mathematical	—	CategoryTheory.Functor.EssSurj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing DerivedCategory HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd instCategoryDerivedCategory Q	—	CategoryTheory.Localization.essSurj AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian instIsLocalizationCochainComplexIntQQuasiIsoUp
instEssSurjHomotopyCategoryIntUpQh 📖	mathematical	—	CategoryTheory.Functor.EssSurj 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 DerivedCategory instCategoryHomotopyCategory instCategoryDerivedCategory Qh	—	CategoryTheory.Localization.essSurj 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 instIsLocalizationHomotopyCategoryIntUpQhQuasiIso
instFaithfulFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Functor DerivedCategory instCategoryDerivedCategory CategoryTheory.Functor.category 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.obj CategoryTheory.Functor.whiskeringLeft Qh	—	CategoryTheory.categoryWithHomology_of_abelian instIsLocalizationHomotopyCategoryIntUpQhQuasiIso
instFullFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.Functor DerivedCategory instCategoryDerivedCategory CategoryTheory.Functor.category 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.obj CategoryTheory.Functor.whiskeringLeft Qh	—	CategoryTheory.categoryWithHomology_of_abelian instIsLocalizationHomotopyCategoryIntUpQhQuasiIso
instHasZeroObject 📖	mathematical	—	CategoryTheory.Limits.HasZeroObject DerivedCategory instCategoryDerivedCategory	—	CategoryTheory.Functor.hasZeroObject_of_additive AddRightCancelSemigroup.toIsRightCancelAdd instAdditiveCochainComplexIntQ HomologicalComplex.instHasZeroObject CategoryTheory.Abelian.hasZeroObject
instIsIsoMapCochainComplexIntQOfQuasiIso 📖	mathematical	—	CategoryTheory.IsIso DerivedCategory instCategoryDerivedCategory 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.Functor.map	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Localization.inverts 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 instIsLocalizationCochainComplexIntQQuasiIsoUp
instIsLocalizationCochainComplexIntQQuasiIsoUp 📖	mathematical	—	CategoryTheory.Functor.IsLocalization CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing DerivedCategory HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd instCategoryDerivedCategory Q HomologicalComplex.quasiIso 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.categoryWithHomology_of_abelian	—	AddRightCancelSemigroup.toIsRightCancelAdd 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 CategoryTheory.MorphismProperty.instIsLocalizationLocalization'Q'
instIsLocalizationHomotopyCategoryIntUpQhQuasiIso 📖	mathematical	—	CategoryTheory.Functor.IsLocalization 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 DerivedCategory instCategoryHomotopyCategory instCategoryDerivedCategory Qh 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 HomologicalComplexUpToQuasiIso.instIsLocalizationHomotopyCategoryQhQuasiIso instIsLocalizationHomologicalComplexIntUpHomotopyCategoryQuotientHomotopyEquivalences CategoryTheory.Abelian.hasBinaryBiproducts
instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic 📖	mathematical	—	CategoryTheory.Functor.IsLocalization 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 DerivedCategory instCategoryHomotopyCategory instCategoryDerivedCategory Qh CategoryTheory.ObjectProperty.trW HomotopyCategory.instHasZeroObject CategoryTheory.Abelian.hasZeroObject HomotopyCategory.hasShift HomotopyCategory.instPreadditive HomotopyCategory.instAdditiveIntUpShiftFunctor HomotopyCategory.instPretriangulatedIntUp CategoryTheory.Abelian.hasBinaryBiproducts HomotopyCategory.subcategoryAcyclic	—	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 HomotopyCategory.instHasZeroObject CategoryTheory.Abelian.hasZeroObject HomotopyCategory.instAdditiveIntUpShiftFunctor CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.categoryWithHomology_of_abelian HomotopyCategory.quasiIso_eq_subcategoryAcyclic_W instIsLocalizationHomotopyCategoryIntUpQhQuasiIso
instIsTriangulated 📖	mathematical	—	CategoryTheory.IsTriangulated DerivedCategory instCategoryDerivedCategory instPreadditive instHasZeroObject instHasShiftInt instAdditiveShiftFunctorInt instPretriangulated	—	CategoryTheory.Triangulated.Localization.isTriangulated 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 HomotopyCategory.instHasZeroObject CategoryTheory.Abelian.hasZeroObject HomotopyCategory.instAdditiveIntUpShiftFunctor CategoryTheory.Abelian.hasBinaryBiproducts instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic CategoryTheory.ObjectProperty.instHasLeftCalculusOfFractionsTrWOfIsTriangulatedOfIsTriangulated HomotopyCategory.instIsTriangulatedIntUp HomotopyCategory.instIsTriangulatedIntUpSubcategoryAcyclic instHasZeroObject instAdditiveShiftFunctorInt instIsTriangulatedHomotopyCategoryIntUpQh
instIsTriangulatedHomotopyCategoryIntUpQh 📖	mathematical	—	CategoryTheory.Functor.IsTriangulated 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 DerivedCategory instCategoryHomotopyCategory instCategoryDerivedCategory HomotopyCategory.hasShift instHasShiftInt Qh instCommShiftHomotopyCategoryIntUpQh HomotopyCategory.instHasZeroObject CategoryTheory.Abelian.hasZeroObject instHasZeroObject HomotopyCategory.instPreadditive instPreadditive HomotopyCategory.instAdditiveIntUpShiftFunctor instAdditiveShiftFunctorInt HomotopyCategory.instPretriangulatedIntUp CategoryTheory.Abelian.hasBinaryBiproducts instPretriangulated	—	CategoryTheory.Triangulated.Localization.isTriangulated_functor 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 HomotopyCategory.instHasZeroObject CategoryTheory.Abelian.hasZeroObject HomotopyCategory.instAdditiveIntUpShiftFunctor CategoryTheory.Abelian.hasBinaryBiproducts instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic CategoryTheory.ObjectProperty.instHasLeftCalculusOfFractionsTrWOfIsTriangulatedOfIsTriangulated HomotopyCategory.instIsTriangulatedIntUp HomotopyCategory.instIsTriangulatedIntUpSubcategoryAcyclic CategoryTheory.ObjectProperty.instIsCompatibleWithTriangulationTrWOfIsTriangulatedOfIsTriangulated instHasZeroObject instAdditiveShiftFunctorInt instAdditiveHomotopyCategoryIntUpQh
isIso_Q_map_iff_quasiIso 📖	mathematical	—	CategoryTheory.IsIso DerivedCategory instCategoryDerivedCategory 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.Functor.map QuasiIso CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplexUpToQuasiIso.isIso_Q_map_iff_mem_quasiIso CategoryTheory.categoryWithHomology_of_abelian
mappingCocone_triangle_distinguished 📖	mathematical	—	CategoryTheory.Pretriangulated.Triangle DerivedCategory instCategoryDerivedCategory instHasShiftInt Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles instHasZeroObject instPreadditive instAdditiveShiftFunctorInt 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 CochainComplex.instHasShiftInt CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Functor.mapTriangle Q instCommShiftCochainComplexIntQ CochainComplex.mappingCocone.triangle CategoryTheory.Abelian.hasBinaryBiproducts	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasZeroObject instAdditiveShiftFunctorInt CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Pretriangulated.rotate_distinguished_triangle CategoryTheory.Pretriangulated.isomorphic_distinguished mappingCone_triangle_distinguished instAdditiveCochainComplexIntQ
mappingCone_triangle_distinguished 📖	mathematical	—	CategoryTheory.Pretriangulated.Triangle DerivedCategory instCategoryDerivedCategory instHasShiftInt Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles instHasZeroObject instPreadditive instAdditiveShiftFunctorInt 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 CochainComplex.instHasShiftInt CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Functor.mapTriangle Q instCommShiftCochainComplexIntQ CochainComplex.mappingCone.triangle CategoryTheory.Abelian.hasBinaryBiproducts	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasZeroObject instAdditiveShiftFunctorInt CategoryTheory.Abelian.hasBinaryBiproducts mem_distTriang_iff
mem_distTriang_iff 📖	mathematical	—	CategoryTheory.Pretriangulated.Triangle DerivedCategory instCategoryDerivedCategory instHasShiftInt Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles instHasZeroObject instPreadditive instAdditiveShiftFunctorInt instPretriangulated CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Iso CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Functor.obj CochainComplex.instHasShiftInt CategoryTheory.Functor.mapTriangle Q instCommShiftCochainComplexIntQ CochainComplex.mappingCone.triangle CategoryTheory.Abelian.hasBinaryBiproducts	—	instHasZeroObject instAdditiveShiftFunctorInt AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Abelian.hasZeroObject 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 instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso CategoryTheory.Pretriangulated.isomorphic_distinguished CategoryTheory.Functor.map_distinguished HomotopyCategory.instHasZeroObject HomotopyCategory.instAdditiveIntUpShiftFunctor instIsTriangulatedHomotopyCategoryIntUpQh
singleFunctorsPostcompQIso_hom_hom 📖	mathematical	—	CategoryTheory.SingleFunctors.Hom.hom DerivedCategory instCategoryDerivedCategory Int.instAddMonoid instHasShiftInt singleFunctors CategoryTheory.SingleFunctors.postcomp 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 CochainComplex.instHasShiftInt CochainComplex.singleFunctors CategoryTheory.Abelian.hasZeroObject Q instCommShiftCochainComplexIntQ CategoryTheory.Iso.hom CategoryTheory.SingleFunctors CategoryTheory.SingleFunctors.instCategory singleFunctorsPostcompQIso CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.SingleFunctors.functor	—	CategoryTheory.NatTrans.ext' AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.hasZeroObject 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 CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp
singleFunctorsPostcompQIso_inv_hom 📖	mathematical	—	CategoryTheory.SingleFunctors.Hom.hom DerivedCategory instCategoryDerivedCategory Int.instAddMonoid instHasShiftInt CategoryTheory.SingleFunctors.postcomp 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 CochainComplex.instHasShiftInt CochainComplex.singleFunctors CategoryTheory.Abelian.hasZeroObject Q instCommShiftCochainComplexIntQ singleFunctors CategoryTheory.Iso.inv CategoryTheory.SingleFunctors CategoryTheory.SingleFunctors.instCategory singleFunctorsPostcompQIso CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.SingleFunctors.functor	—	CategoryTheory.NatTrans.ext' AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.hasZeroObject instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso CategoryTheory.Functor.mapIso_refl CategoryTheory.Category.assoc 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.comp_id

HasDerivedCategory

Definitions

Name	Category	Theorems
standard 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
DerivedCategory 📖	CompOp	135 math math: DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp, DerivedCategory.right_fac, CategoryTheory.Abelian.Ext.homLinearEquiv_apply, DerivedCategory.instHasZeroObject, DerivedCategory.instIsTriangulated, DerivedCategory.instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, DerivedCategory.HomologySequence.comp_δ, CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, DerivedCategory.isLE_iff, CategoryTheory.Abelian.Ext.smul_hom, DerivedCategory.isZero_of_isGE, DerivedCategory.singleFunctorsPostcompQIso_inv_hom, CochainComplex.IsKInjective.Qh_map_bijective, DerivedCategory.subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE, DerivedCategory.HomologySequence.exact₂, DerivedCategory.homologyFunctorFactorsh_hom_app_quotient_obj_assoc, DerivedCategory.homologyFunctorFactors_hom_naturality, DerivedCategory.instFaithfulSingleFunctor, DerivedCategory.shiftMap_homologyFunctor_map_Q_assoc, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle_assoc, DerivedCategory.triangleOfSES_mor₁, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CategoryTheory.Abelian.Ext.mk₀_hom, DerivedCategory.mappingCone_triangle_distinguished, DerivedCategory.HomologySequence.mono_homologyMap_mor₁_iff, CategoryTheory.Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply, CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh, CategoryTheory.ShortComplex.ShortExact.singleTriangle.map_hom₁, DerivedCategory.instIsTriangulatedHomotopyCategoryIntUpQh, DerivedCategory.isZero_of_isLE, DerivedCategory.shiftMap_homologyFunctor_map_Qh_assoc, DerivedCategory.to_singleFunctor_obj_eq_zero_of_injective, DerivedCategory.right_fac_of_isStrictlyLE_of_isStrictlyGE, DerivedCategory.instIsIsoMapCochainComplexIntQOfQuasiIso, DerivedCategory.triangleOfSES_obj₃, DerivedCategory.instLinearCochainComplexIntQ, CategoryTheory.Abelian.Ext.singleFunctor_map_comp_hom, CategoryTheory.ProjectiveResolution.extMk_hom, CategoryTheory.Abelian.Ext.mapExactFunctor_hom, CategoryTheory.Abelian.Ext.homEquiv_chgUniv, DerivedCategory.HomologySequence.comp_δ_assoc, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, DerivedCategory.triangleOfSES.map_hom₁, DerivedCategory.instAdditiveHomotopyCategoryIntUpQh, CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors, DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhQuasiIso, CategoryTheory.ShortComplex.ShortExact.singleTriangle.map_hom₂, DerivedCategory.left_fac_of_isStrictlyLE_of_isStrictlyGE, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃, CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₂, CategoryTheory.ShortComplex.ShortExact.singleTriangle_mor₃, CategoryTheory.ShortComplex.ShortExact.singleTriangle_mor₁, CategoryTheory.Abelian.Ext.hom_comp_singleFunctor_map_shift, DerivedCategory.instFullSingleFunctor, DerivedCategory.HomologySequence.epi_homologyMap_mor₁_iff, CochainComplex.HomComplex.CohomologyClass.equiv_toSmallShiftedHom_mk, CategoryTheory.Functor.instIsTriangulatedDerivedCategoryMapDerivedCategory, DerivedCategory.HomologySequence.mono_homologyMap_mor₂_iff, DerivedCategory.isLE_Q_obj_iff, CategoryTheory.Abelian.Ext.homAddEquiv_apply, DerivedCategory.triangleOfSES_obj₁, DerivedCategory.instAdditiveShiftFunctorInt, CochainComplex.IsKProjective.Qh_map_bijective, CategoryTheory.ShortComplex.ShortExact.singleTriangle_mor₂, DerivedCategory.isGE_Q_obj_iff, CategoryTheory.Abelian.Ext.add_hom, DerivedCategory.instEssSurjHomotopyCategoryIntUpQh, DerivedCategory.instFaithfulFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃, DerivedCategory.isGE_iff, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁, CategoryTheory.Abelian.Ext.zero_hom, DerivedCategory.instIsLEObjSingleFunctor, DerivedCategory.instIsGEObjCochainComplexIntQOfIsGE, DerivedCategory.exists_iso_singleFunctor_obj_of_isGE_of_isLE, CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₁, CategoryTheory.instSmallHomDerivedCategoryObjSingleFunctorOfHasExt, DerivedCategory.instLinearShiftFunctorInt, DerivedCategory.exists_iso_Q_obj_of_isGE_of_isLE, DerivedCategory.triangleOfSES.map_hom₃, DerivedCategory.instEssSurjArrowHomotopyCategoryIntUpMapArrowQh, DerivedCategory.HomologySequence.exact₁, DerivedCategory.from_singleFunctor_obj_eq_zero_of_projective, DerivedCategory.exists_iso_Q_obj_of_isGE, DerivedCategory.shift_homologyFunctor, DerivedCategory.homologyFunctorFactorsh_hom_app_quotient_obj, CategoryTheory.InjectiveResolution.extMk_hom, DerivedCategory.triangleOfSES_mor₃, DerivedCategory.right_fac_of_isStrictlyLE, DerivedCategory.shiftMap_homologyFunctor_map_Q, CategoryTheory.Abelian.Ext.neg_hom, DerivedCategory.triangleOfSES_distinguished, DerivedCategory.instAdditiveCochainComplexIntQ, DerivedCategory.instAdditiveSingleFunctor, DerivedCategory.Qh_obj_singleFunctors_obj, DerivedCategory.triangleOfSES.map_hom₂, CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₃, DerivedCategory.exists_iso_Q_obj_of_isLE, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, DerivedCategory.instFullFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, CategoryTheory.hasExt_iff, DerivedCategory.triangleOfSES_obj₂, DerivedCategory.instEssSurjCochainComplexIntQ, DerivedCategory.singleFunctorsPostcompQIso_hom_hom, DerivedCategory.shiftMap_homologyFunctor_map_Qh, DerivedCategory.triangleOfSES_mor₂, DerivedCategory.instLinearSingleFunctor, CategoryTheory.ShortComplex.ShortExact.singleTriangle_distinguished, DerivedCategory.instIsHomologicalHomologyFunctor, DerivedCategory.instLinearHomotopyCategoryIntUpQh, CategoryTheory.ShortComplex.ShortExact.singleTriangle.map_hom₃, DerivedCategory.homologyFunctorFactorsh_inv_app_quotient_obj_assoc, CategoryTheory.Abelian.Ext.homLinearEquiv_symm_apply, DerivedCategory.HomologySequence.δ_comp_assoc, DerivedCategory.HomologySequence.δ_comp, DerivedCategory.homologyFunctorFactorsh_inv_app_quotient_obj, DerivedCategory.mem_distTriang_iff, DerivedCategory.instIsLEObjCochainComplexIntQOfIsLE, DerivedCategory.mappingCocone_triangle_distinguished, DerivedCategory.HomologySequence.exact₃, DerivedCategory.Q_map_eq_of_homotopy, DerivedCategory.HomologySequence.epi_homologyMap_mor₂_iff, DerivedCategory.isIso_Q_map_iff_quasiIso, DerivedCategory.isIso_Qh_map_iff, CategoryTheory.Functor.instLinearDerivedCategoryMapDerivedCategory, DerivedCategory.left_fac_of_isStrictlyGE, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle, CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app, DerivedCategory.homologyFunctorFactors_hom_naturality_assoc, DerivedCategory.left_fac, DerivedCategory.instIsGEObjSingleFunctor, DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic, CategoryTheory.Abelian.Ext.comp_hom
HasDerivedCategory 📖	CompOp	—
instCategoryDerivedCategory 📖	CompOp	135 math math: DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp, DerivedCategory.right_fac, CategoryTheory.Abelian.Ext.homLinearEquiv_apply, DerivedCategory.instHasZeroObject, DerivedCategory.instIsTriangulated, DerivedCategory.instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, DerivedCategory.HomologySequence.comp_δ, CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, DerivedCategory.isLE_iff, CategoryTheory.Abelian.Ext.smul_hom, DerivedCategory.isZero_of_isGE, DerivedCategory.singleFunctorsPostcompQIso_inv_hom, CochainComplex.IsKInjective.Qh_map_bijective, DerivedCategory.subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE, DerivedCategory.HomologySequence.exact₂, DerivedCategory.homologyFunctorFactorsh_hom_app_quotient_obj_assoc, DerivedCategory.homologyFunctorFactors_hom_naturality, DerivedCategory.instFaithfulSingleFunctor, DerivedCategory.shiftMap_homologyFunctor_map_Q_assoc, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle_assoc, DerivedCategory.triangleOfSES_mor₁, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CategoryTheory.Abelian.Ext.mk₀_hom, DerivedCategory.mappingCone_triangle_distinguished, DerivedCategory.HomologySequence.mono_homologyMap_mor₁_iff, CategoryTheory.Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply, CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh, CategoryTheory.ShortComplex.ShortExact.singleTriangle.map_hom₁, DerivedCategory.instIsTriangulatedHomotopyCategoryIntUpQh, DerivedCategory.isZero_of_isLE, DerivedCategory.shiftMap_homologyFunctor_map_Qh_assoc, DerivedCategory.to_singleFunctor_obj_eq_zero_of_injective, DerivedCategory.right_fac_of_isStrictlyLE_of_isStrictlyGE, DerivedCategory.instIsIsoMapCochainComplexIntQOfQuasiIso, DerivedCategory.triangleOfSES_obj₃, DerivedCategory.instLinearCochainComplexIntQ, CategoryTheory.Abelian.Ext.singleFunctor_map_comp_hom, CategoryTheory.ProjectiveResolution.extMk_hom, CategoryTheory.Abelian.Ext.mapExactFunctor_hom, CategoryTheory.Abelian.Ext.homEquiv_chgUniv, DerivedCategory.HomologySequence.comp_δ_assoc, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, DerivedCategory.triangleOfSES.map_hom₁, DerivedCategory.instAdditiveHomotopyCategoryIntUpQh, CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors, DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhQuasiIso, CategoryTheory.ShortComplex.ShortExact.singleTriangle.map_hom₂, DerivedCategory.left_fac_of_isStrictlyLE_of_isStrictlyGE, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃, CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₂, CategoryTheory.ShortComplex.ShortExact.singleTriangle_mor₃, CategoryTheory.ShortComplex.ShortExact.singleTriangle_mor₁, CategoryTheory.Abelian.Ext.hom_comp_singleFunctor_map_shift, DerivedCategory.instFullSingleFunctor, DerivedCategory.HomologySequence.epi_homologyMap_mor₁_iff, CochainComplex.HomComplex.CohomologyClass.equiv_toSmallShiftedHom_mk, CategoryTheory.Functor.instIsTriangulatedDerivedCategoryMapDerivedCategory, DerivedCategory.HomologySequence.mono_homologyMap_mor₂_iff, DerivedCategory.isLE_Q_obj_iff, CategoryTheory.Abelian.Ext.homAddEquiv_apply, DerivedCategory.triangleOfSES_obj₁, DerivedCategory.instAdditiveShiftFunctorInt, CochainComplex.IsKProjective.Qh_map_bijective, CategoryTheory.ShortComplex.ShortExact.singleTriangle_mor₂, DerivedCategory.isGE_Q_obj_iff, CategoryTheory.Abelian.Ext.add_hom, DerivedCategory.instEssSurjHomotopyCategoryIntUpQh, DerivedCategory.instFaithfulFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃, DerivedCategory.isGE_iff, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁, CategoryTheory.Abelian.Ext.zero_hom, DerivedCategory.instIsLEObjSingleFunctor, DerivedCategory.instIsGEObjCochainComplexIntQOfIsGE, DerivedCategory.exists_iso_singleFunctor_obj_of_isGE_of_isLE, CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₁, CategoryTheory.instSmallHomDerivedCategoryObjSingleFunctorOfHasExt, DerivedCategory.instLinearShiftFunctorInt, DerivedCategory.exists_iso_Q_obj_of_isGE_of_isLE, DerivedCategory.triangleOfSES.map_hom₃, DerivedCategory.instEssSurjArrowHomotopyCategoryIntUpMapArrowQh, DerivedCategory.HomologySequence.exact₁, DerivedCategory.from_singleFunctor_obj_eq_zero_of_projective, DerivedCategory.exists_iso_Q_obj_of_isGE, DerivedCategory.shift_homologyFunctor, DerivedCategory.homologyFunctorFactorsh_hom_app_quotient_obj, CategoryTheory.InjectiveResolution.extMk_hom, DerivedCategory.triangleOfSES_mor₃, DerivedCategory.right_fac_of_isStrictlyLE, DerivedCategory.shiftMap_homologyFunctor_map_Q, CategoryTheory.Abelian.Ext.neg_hom, DerivedCategory.triangleOfSES_distinguished, DerivedCategory.instAdditiveCochainComplexIntQ, DerivedCategory.instAdditiveSingleFunctor, DerivedCategory.Qh_obj_singleFunctors_obj, DerivedCategory.triangleOfSES.map_hom₂, CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₃, DerivedCategory.exists_iso_Q_obj_of_isLE, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, DerivedCategory.instFullFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, CategoryTheory.hasExt_iff, DerivedCategory.triangleOfSES_obj₂, DerivedCategory.instEssSurjCochainComplexIntQ, DerivedCategory.singleFunctorsPostcompQIso_hom_hom, DerivedCategory.shiftMap_homologyFunctor_map_Qh, DerivedCategory.triangleOfSES_mor₂, DerivedCategory.instLinearSingleFunctor, CategoryTheory.ShortComplex.ShortExact.singleTriangle_distinguished, DerivedCategory.instIsHomologicalHomologyFunctor, DerivedCategory.instLinearHomotopyCategoryIntUpQh, CategoryTheory.ShortComplex.ShortExact.singleTriangle.map_hom₃, DerivedCategory.homologyFunctorFactorsh_inv_app_quotient_obj_assoc, CategoryTheory.Abelian.Ext.homLinearEquiv_symm_apply, DerivedCategory.HomologySequence.δ_comp_assoc, DerivedCategory.HomologySequence.δ_comp, DerivedCategory.homologyFunctorFactorsh_inv_app_quotient_obj, DerivedCategory.mem_distTriang_iff, DerivedCategory.instIsLEObjCochainComplexIntQOfIsLE, DerivedCategory.mappingCocone_triangle_distinguished, DerivedCategory.HomologySequence.exact₃, DerivedCategory.Q_map_eq_of_homotopy, DerivedCategory.HomologySequence.epi_homologyMap_mor₂_iff, DerivedCategory.isIso_Q_map_iff_quasiIso, DerivedCategory.isIso_Qh_map_iff, CategoryTheory.Functor.instLinearDerivedCategoryMapDerivedCategory, DerivedCategory.left_fac_of_isStrictlyGE, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle, CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app, DerivedCategory.homologyFunctorFactors_hom_naturality_assoc, DerivedCategory.left_fac, DerivedCategory.instIsGEObjSingleFunctor, DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic, CategoryTheory.Abelian.Ext.comp_hom

---

← Back to Index