Basic

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

Statistics

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

DerivedCategory

Definitions

Name	Category	Theorems
Q 📖	CompOp	45 math math: instIsLocalizationCochainComplexIntQQuasiIsoUp, right_fac, instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, singleFunctorsPostcompQIso_inv_hom, subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, triangleOfSES_mor₁, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, to_singleFunctor_obj_eq_zero_of_injective, right_fac_of_isStrictlyLE_of_isStrictlyGE, triangleOfSES_obj₃, instLinearCochainComplexIntQ, CategoryTheory.ProjectiveResolution.extMk_hom, instIsIsoMapCochainComplexIntQ, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_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, from_singleFunctor_obj_eq_zero_of_projective, exists_iso_Q_obj_of_isGE, CategoryTheory.InjectiveResolution.extMk_hom, right_fac_of_isStrictlyLE, instAdditiveCochainComplexIntQ, exists_iso_Q_obj_of_isLE, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, triangleOfSES_obj₂, instEssSurjCochainComplexIntQ, singleFunctorsPostcompQIso_hom_hom, triangleOfSES_mor₂, mem_distTriang_iff, instIsLEObjCochainComplexIntQOfIsLE, Q_map_eq_of_homotopy, isIso_Q_map_iff_quasiIso, left_fac_of_isStrictlyGE, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app, left_fac
Qh 📖	CompOp	16 math math: instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, CochainComplex.IsKInjective.Qh_map_bijective, CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh, instIsTriangulatedHomotopyCategoryIntUpQh, instAdditiveHomotopyCategoryIntUpQh, instIsLocalizationHomotopyCategoryIntUpQhQuasiIso, CochainComplex.IsKProjective.Qh_map_bijective, instEssSurjHomotopyCategoryIntUpQh, instFaithfulFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, instEssSurjArrowHomotopyCategoryIntUpMapArrowQh, Qh_obj_singleFunctors_obj, instFullFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, instLinearHomotopyCategoryIntUpQh, isIso_Qh_map_iff, CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app, instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic
instCategory 📖	CompOp	103 math math: instIsLocalizationCochainComplexIntQQuasiIsoUp, right_fac, CategoryTheory.Abelian.Ext.homLinearEquiv_apply, instHasZeroObject, instIsTriangulated, instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, isLE_iff, CategoryTheory.Abelian.Ext.smul_hom, isZero_of_isGE, singleFunctorsPostcompQIso_inv_hom, CochainComplex.IsKInjective.Qh_map_bijective, subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE, instFaithfulSingleFunctor, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, triangleOfSES_mor₁, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CategoryTheory.Abelian.Ext.mk₀_hom, CategoryTheory.Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply, CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh, instIsTriangulatedHomotopyCategoryIntUpQh, isZero_of_isLE, to_singleFunctor_obj_eq_zero_of_injective, right_fac_of_isStrictlyLE_of_isStrictlyGE, triangleOfSES_obj₃, instLinearCochainComplexIntQ, CategoryTheory.Abelian.Ext.singleFunctor_map_comp_hom, CategoryTheory.ProjectiveResolution.extMk_hom, CategoryTheory.Abelian.Ext.mapExactFunctor_hom, instIsIsoMapCochainComplexIntQ, CategoryTheory.Abelian.Ext.homEquiv_chgUniv, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, instAdditiveHomotopyCategoryIntUpQh, CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors, instIsLocalizationHomotopyCategoryIntUpQhQuasiIso, 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, instFullSingleFunctor, CochainComplex.HomComplex.CohomologyClass.equiv_toSmallShiftedHom_mk, CategoryTheory.Functor.instIsTriangulatedDerivedCategoryMapDerivedCategory, isLE_Q_obj_iff, CategoryTheory.Abelian.Ext.homAddEquiv_apply, triangleOfSES_obj₁, instAdditiveShiftFunctorInt, CochainComplex.IsKProjective.Qh_map_bijective, CategoryTheory.ShortComplex.ShortExact.singleTriangle_mor₂, isGE_Q_obj_iff, CategoryTheory.Abelian.Ext.add_hom, instEssSurjHomotopyCategoryIntUpQh, instFaithfulFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃, isGE_iff, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁, CategoryTheory.Abelian.Ext.zero_hom, instIsLEObjSingleFunctor, instIsGEObjCochainComplexIntQOfIsGE, exists_iso_singleFunctor_obj_of_isGE_of_isLE, CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₁, CategoryTheory.instSmallHomDerivedCategoryObjSingleFunctorOfHasExt, instLinearShiftFunctorInt, exists_iso_Q_obj_of_isGE_of_isLE, instEssSurjArrowHomotopyCategoryIntUpMapArrowQh, from_singleFunctor_obj_eq_zero_of_projective, exists_iso_Q_obj_of_isGE, CategoryTheory.InjectiveResolution.extMk_hom, triangleOfSES_mor₃, right_fac_of_isStrictlyLE, CategoryTheory.Abelian.Ext.neg_hom, triangleOfSES_distinguished, instAdditiveCochainComplexIntQ, instAdditiveSingleFunctor, Qh_obj_singleFunctors_obj, CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₃, exists_iso_Q_obj_of_isLE, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, instFullFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, CategoryTheory.hasExt_iff, triangleOfSES_obj₂, instEssSurjCochainComplexIntQ, singleFunctorsPostcompQIso_hom_hom, triangleOfSES_mor₂, instLinearSingleFunctor, CategoryTheory.ShortComplex.ShortExact.singleTriangle_distinguished, instIsHomologicalHomologyFunctor, instLinearHomotopyCategoryIntUpQh, CategoryTheory.Abelian.Ext.homLinearEquiv_symm_apply, mem_distTriang_iff, instIsLEObjCochainComplexIntQOfIsLE, Q_map_eq_of_homotopy, isIso_Q_map_iff_quasiIso, isIso_Qh_map_iff, CategoryTheory.Functor.instLinearDerivedCategoryMapDerivedCategory, left_fac_of_isStrictlyGE, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app, left_fac, instIsGEObjSingleFunctor, instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic, CategoryTheory.Abelian.Ext.comp_hom
instCommShiftCochainComplexIntQ 📖	CompOp	16 math math: instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, singleFunctorsPostcompQIso_inv_hom, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, 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, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, singleFunctorsPostcompQIso_hom_hom, mem_distTriang_iff, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom
instCommShiftHomotopyCategoryIntUpQh 📖	CompOp	3 math math: instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh, instIsTriangulatedHomotopyCategoryIntUpQh
instHasShiftInt 📖	CompOp	53 math math: CategoryTheory.Abelian.Ext.homLinearEquiv_apply, instIsTriangulated, instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, CategoryTheory.Abelian.Ext.smul_hom, singleFunctorsPostcompQIso_inv_hom, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, triangleOfSES_mor₁, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CategoryTheory.Abelian.Ext.mk₀_hom, CategoryTheory.Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply, CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh, instIsTriangulatedHomotopyCategoryIntUpQh, triangleOfSES_obj₃, CategoryTheory.Abelian.Ext.singleFunctor_map_comp_hom, CategoryTheory.ProjectiveResolution.extMk_hom, CategoryTheory.Abelian.Ext.mapExactFunctor_hom, CategoryTheory.Abelian.Ext.homEquiv_chgUniv, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors, 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, CochainComplex.HomComplex.CohomologyClass.equiv_toSmallShiftedHom_mk, CategoryTheory.Functor.instIsTriangulatedDerivedCategoryMapDerivedCategory, 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, CategoryTheory.InjectiveResolution.extMk_hom, triangleOfSES_mor₃, CategoryTheory.Abelian.Ext.neg_hom, triangleOfSES_distinguished, CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₃, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, CategoryTheory.hasExt_iff, triangleOfSES_obj₂, singleFunctorsPostcompQIso_hom_hom, triangleOfSES_mor₂, CategoryTheory.ShortComplex.ShortExact.singleTriangle_distinguished, instIsHomologicalHomologyFunctor, CategoryTheory.Abelian.Ext.homLinearEquiv_symm_apply, mem_distTriang_iff, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CategoryTheory.Abelian.Ext.comp_hom
instPreadditive 📖	CompOp	27 math math: CategoryTheory.Abelian.Ext.homLinearEquiv_apply, instIsTriangulated, CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, CategoryTheory.Abelian.Ext.smul_hom, 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, CategoryTheory.Functor.instLinearDerivedCategoryMapDerivedCategory
instPretriangulated 📖	CompOp	7 math math: instIsTriangulated, instIsTriangulatedHomotopyCategoryIntUpQh, CategoryTheory.Functor.instIsTriangulatedDerivedCategoryMapDerivedCategory, triangleOfSES_distinguished, CategoryTheory.ShortComplex.ShortExact.singleTriangle_distinguished, instIsHomologicalHomologyFunctor, mem_distTriang_iff
quotientCompQhIso 📖	CompOp	2 math math: instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app
singleFunctor 📖	CompOp	34 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.Abelian.Ext.singleFunctor_map_comp_hom, CategoryTheory.ProjectiveResolution.extMk_hom, CategoryTheory.Abelian.Ext.mapExactFunctor_hom, CategoryTheory.Abelian.Ext.homEquiv_chgUniv, 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.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 instCategory 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 AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory DerivedCategory instCategory Qh CategoryTheory.SingleFunctors.functor Int.instAddMonoid HomotopyCategory.hasShift HomotopyCategory.singleFunctors CategoryTheory.Abelian.hasZeroObject singleFunctor	—	AddRightCancelSemigroup.toIsRightCancelAdd 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 instCategory HomologicalComplex.instPreadditive instPreadditive Q	—	CategoryTheory.Functor.additive_of_iso AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.instAdditiveComp HomotopyCategory.instAdditiveHomologicalComplexQuotient instAdditiveHomotopyCategoryIntUpQh
instAdditiveHomotopyCategoryIntUpQh 📖	mathematical	—	CategoryTheory.Functor.Additive HomotopyCategory CategoryTheory.Abelian.toPreadditive ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing DerivedCategory instCategoryHomotopyCategory instCategory HomotopyCategory.instPreadditive instPreadditive Qh	—	CategoryTheory.Localization.functor_additive AddRightCancelSemigroup.toIsRightCancelAdd HomotopyCategory.instHasZeroObject CategoryTheory.Abelian.hasZeroObject HomotopyCategory.instAdditiveIntUpShiftFunctor CategoryTheory.Abelian.hasBinaryBiproducts instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic CategoryTheory.ObjectProperty.instHasLeftCalculusOfFractionsTrWOfIsTriangulatedOfIsTriangulated HomotopyCategory.instIsTriangulatedIntUp HomotopyCategory.instIsTriangulatedIntUpSubcategoryAcyclic
instAdditiveShiftFunctorInt 📖	mathematical	—	CategoryTheory.Functor.Additive DerivedCategory instCategory instPreadditive CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt	—	AddRightCancelSemigroup.toIsRightCancelAdd 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 instCategory 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 AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing DerivedCategory HomologicalComplex.instCategory instCategory 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 AddRightCancelSemigroup.toIsRightCancelAdd
instEssSurjArrowHomotopyCategoryIntUpMapArrowQh 📖	mathematical	—	CategoryTheory.Functor.EssSurj CategoryTheory.Arrow HomotopyCategory CategoryTheory.Abelian.toPreadditive ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory DerivedCategory instCategory CategoryTheory.instCategoryArrow CategoryTheory.Functor.mapArrow Qh	—	CategoryTheory.Localization.essSurj_mapArrow AddRightCancelSemigroup.toIsRightCancelAdd 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 instCategory Q	—	CategoryTheory.Localization.essSurj AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian instIsLocalizationCochainComplexIntQQuasiIsoUp
instEssSurjHomotopyCategoryIntUpQh 📖	mathematical	—	CategoryTheory.Functor.EssSurj HomotopyCategory CategoryTheory.Abelian.toPreadditive ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing DerivedCategory instCategoryHomotopyCategory instCategory Qh	—	CategoryTheory.Localization.essSurj AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian instIsLocalizationHomotopyCategoryIntUpQhQuasiIso
instFaithfulFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Functor DerivedCategory instCategory CategoryTheory.Functor.category HomotopyCategory CategoryTheory.Abelian.toPreadditive ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft Qh	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian instIsLocalizationHomotopyCategoryIntUpQhQuasiIso CategoryTheory.Localization.instFaithfulFunctorWhiskeringLeftFunctor'
instFullFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.Functor DerivedCategory instCategory CategoryTheory.Functor.category HomotopyCategory CategoryTheory.Abelian.toPreadditive ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft Qh	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian instIsLocalizationHomotopyCategoryIntUpQhQuasiIso CategoryTheory.Localization.instFullFunctorWhiskeringLeftFunctor'
instHasZeroObject 📖	mathematical	—	CategoryTheory.Limits.HasZeroObject DerivedCategory instCategory	—	CategoryTheory.Functor.hasZeroObject_of_additive AddRightCancelSemigroup.toIsRightCancelAdd instAdditiveCochainComplexIntQ HomologicalComplex.instHasZeroObject CategoryTheory.Abelian.hasZeroObject
instIsIsoMapCochainComplexIntQ 📖	mathematical	—	CategoryTheory.IsIso DerivedCategory instCategory 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 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 instCategory Q HomologicalComplex.quasiIso CategoryTheory.categoryWithHomology_of_abelian	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.MorphismProperty.instIsLocalizationLocalization'Q'
instIsLocalizationHomotopyCategoryIntUpQhQuasiIso 📖	mathematical	—	CategoryTheory.Functor.IsLocalization HomotopyCategory CategoryTheory.Abelian.toPreadditive ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing DerivedCategory instCategoryHomotopyCategory instCategory Qh HomotopyCategory.quasiIso CategoryTheory.categoryWithHomology_of_abelian	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian HomologicalComplexUpToQuasiIso.instIsLocalizationHomotopyCategoryQhQuasiIso instIsLocalizationHomologicalComplexIntUpHomotopyCategoryQuotientHomotopyEquivalences CategoryTheory.Abelian.hasBinaryBiproducts
instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic 📖	mathematical	—	CategoryTheory.Functor.IsLocalization HomotopyCategory CategoryTheory.Abelian.toPreadditive ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing DerivedCategory instCategoryHomotopyCategory instCategory Qh CategoryTheory.ObjectProperty.trW HomotopyCategory.instHasZeroObject CategoryTheory.Abelian.hasZeroObject HomotopyCategory.hasShift HomotopyCategory.instPreadditive HomotopyCategory.instAdditiveIntUpShiftFunctor HomotopyCategory.instPretriangulatedIntUp CategoryTheory.Abelian.hasBinaryBiproducts HomotopyCategory.subcategoryAcyclic	—	AddRightCancelSemigroup.toIsRightCancelAdd 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 instCategory instPreadditive instHasZeroObject instHasShiftInt instAdditiveShiftFunctorInt instPretriangulated	—	CategoryTheory.Triangulated.Localization.isTriangulated AddRightCancelSemigroup.toIsRightCancelAdd 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 AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing DerivedCategory instCategoryHomotopyCategory instCategory 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 AddRightCancelSemigroup.toIsRightCancelAdd 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 instCategory 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
mem_distTriang_iff 📖	mathematical	—	CategoryTheory.Pretriangulated.Triangle DerivedCategory instCategory instHasShiftInt Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles instHasZeroObject instPreadditive instAdditiveShiftFunctorInt instPretriangulated CategoryTheory.Iso CategoryTheory.Pretriangulated.triangleCategory 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.Functor.mapTriangle Q instCommShiftCochainComplexIntQ CochainComplex.mappingCone.triangle CategoryTheory.Abelian.hasBinaryBiproducts	—	instHasZeroObject instAdditiveShiftFunctorInt AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Abelian.hasZeroObject instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso CategoryTheory.Pretriangulated.isomorphic_distinguished CategoryTheory.Functor.map_distinguished HomotopyCategory.instHasZeroObject HomotopyCategory.instAdditiveIntUpShiftFunctor instIsTriangulatedHomotopyCategoryIntUpQh
singleFunctorsPostcompQIso_hom_hom 📖	mathematical	—	CategoryTheory.SingleFunctors.Hom.hom DerivedCategory instCategory 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 CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.map_id CategoryTheory.Category.id_comp
singleFunctorsPostcompQIso_inv_hom 📖	mathematical	—	CategoryTheory.SingleFunctors.Hom.hom DerivedCategory instCategory 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 CategoryTheory.Category.comp_id

HasDerivedCategory

Definitions

Name	Category	Theorems
standard 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
DerivedCategory 📖	CompOp	103 math math: DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp, DerivedCategory.right_fac, CategoryTheory.Abelian.Ext.homLinearEquiv_apply, DerivedCategory.instHasZeroObject, DerivedCategory.instIsTriangulated, DerivedCategory.instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, 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.instFaithfulSingleFunctor, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, DerivedCategory.triangleOfSES_mor₁, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CategoryTheory.Abelian.Ext.mk₀_hom, CategoryTheory.Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply, CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh, DerivedCategory.instIsTriangulatedHomotopyCategoryIntUpQh, DerivedCategory.isZero_of_isLE, DerivedCategory.to_singleFunctor_obj_eq_zero_of_injective, DerivedCategory.right_fac_of_isStrictlyLE_of_isStrictlyGE, DerivedCategory.triangleOfSES_obj₃, DerivedCategory.instLinearCochainComplexIntQ, CategoryTheory.Abelian.Ext.singleFunctor_map_comp_hom, CategoryTheory.ProjectiveResolution.extMk_hom, CategoryTheory.Abelian.Ext.mapExactFunctor_hom, DerivedCategory.instIsIsoMapCochainComplexIntQ, CategoryTheory.Abelian.Ext.homEquiv_chgUniv, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, DerivedCategory.instAdditiveHomotopyCategoryIntUpQh, CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors, DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhQuasiIso, 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, CochainComplex.HomComplex.CohomologyClass.equiv_toSmallShiftedHom_mk, CategoryTheory.Functor.instIsTriangulatedDerivedCategoryMapDerivedCategory, 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.instEssSurjArrowHomotopyCategoryIntUpMapArrowQh, DerivedCategory.from_singleFunctor_obj_eq_zero_of_projective, DerivedCategory.exists_iso_Q_obj_of_isGE, CategoryTheory.InjectiveResolution.extMk_hom, DerivedCategory.triangleOfSES_mor₃, DerivedCategory.right_fac_of_isStrictlyLE, CategoryTheory.Abelian.Ext.neg_hom, DerivedCategory.triangleOfSES_distinguished, DerivedCategory.instAdditiveCochainComplexIntQ, DerivedCategory.instAdditiveSingleFunctor, DerivedCategory.Qh_obj_singleFunctors_obj, 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.triangleOfSES_mor₂, DerivedCategory.instLinearSingleFunctor, CategoryTheory.ShortComplex.ShortExact.singleTriangle_distinguished, DerivedCategory.instIsHomologicalHomologyFunctor, DerivedCategory.instLinearHomotopyCategoryIntUpQh, CategoryTheory.Abelian.Ext.homLinearEquiv_symm_apply, DerivedCategory.mem_distTriang_iff, DerivedCategory.instIsLEObjCochainComplexIntQOfIsLE, DerivedCategory.Q_map_eq_of_homotopy, 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, CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app, DerivedCategory.left_fac, DerivedCategory.instIsGEObjSingleFunctor, DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic, CategoryTheory.Abelian.Ext.comp_hom
HasDerivedCategory 📖	CompOp	—

---

← Back to Index