HomotopyCategory

📁 Source: Mathlib/Algebra/Homology/HomotopyCategory.lean

Statistics

Metric	Count
Definitions mapHomotopyCategory, mapHomotopyCategoryFactors, mapHomotopyCategory, HomotopyCategory, homologyFunctor, homologyFunctorFactors, homotopyEquivOfIso, homotopyOfEq, homotopyOutMap, instInhabitedOfHasZeroObject, instLinear, instPreadditive, instPreadditiveQuotientHomologicalComplexHomotopic, isoOfHomotopyEquiv, quotient, HomotopyCategory, homotopic, instCategoryHomotopyCategory	18
Theorems mapHomotopyCategory_map, mapHomotopyCategory_obj, mapHomotopyCategory_app, mapHomotopyCategory_comp, mapHomotopyCategory_id, instAdditiveHomotopyCategoryMapHomotopyCategory, instLinearHomotopyCategoryMapHomotopyCategory, eq_of_homotopy, instAdditiveHomologicalComplexQuotient, instAdditiveHomologicalComplexQuotientHomotopicFunctor, instAdditiveHomologyFunctor, instEssSurjHomologicalComplexQuotient, instFaithfulFunctorHomologicalComplexObjWhiskeringLeftQuotient, instFullFunctorHomologicalComplexObjWhiskeringLeftQuotient, instFullHomologicalComplexQuotient, instHasZeroObject, instLinearHomologicalComplexQuotient, isZero_quotient_obj_iff, isoOfHomotopyEquiv_hom, isoOfHomotopyEquiv_inv, quot_mk_eq_quotient_map, quotient_inverts_homotopyEquivalences, quotient_map_eq_zero_iff, quotient_map_out, quotient_map_out_comp_out, quotient_obj_as, quotient_obj_surjective, homotopy_congruence	28
Total	46

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instAdditiveHomotopyCategoryMapHomotopyCategory 📖	mathematical	—	Functor.Additive HomotopyCategory instCategoryHomotopyCategory HomotopyCategory.instPreadditive Functor.mapHomotopyCategory	—	Functor.additive_of_iso Functor.preservesZeroMorphisms_of_additive Functor.instAdditiveComp Functor.map_homogical_complex_additive HomotopyCategory.instAdditiveHomologicalComplexQuotient Functor.additive_of_full_essSurj_comp HomotopyCategory.instFullHomologicalComplexQuotient HomotopyCategory.instEssSurjHomologicalComplexQuotient
instLinearHomotopyCategoryMapHomotopyCategory 📖	mathematical	—	Functor.Linear HomotopyCategory instCategoryHomotopyCategory HomotopyCategory.instPreadditive HomotopyCategory.instLinear Functor.mapHomotopyCategory	—	Functor.linear_of_iso Functor.preservesZeroMorphisms_of_additive Functor.instLinearComp Functor.mapHomologicalComplex_linear HomotopyCategory.instLinearHomologicalComplexQuotient Functor.linear_of_full_essSurj_comp HomotopyCategory.instFullHomologicalComplexQuotient HomotopyCategory.instEssSurjHomologicalComplexQuotient

CategoryTheory.Functor

Definitions

Name	Category	Theorems
mapHomotopyCategory 📖	CompOp	13 math math: mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app_assoc, CategoryTheory.instAdditiveHomotopyCategoryMapHomotopyCategory, CategoryTheory.NatTrans.mapHomotopyCategory_app, CategoryTheory.NatTrans.mapHomotopyCategory_comp, instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh, CategoryTheory.NatTrans.mapHomotopyCategory_id, HomotopyCategory.instIsTriangulatedIntUpMapHomotopyCategory, CategoryTheory.instLinearHomotopyCategoryMapHomotopyCategory, mapHomotopyCategory_map, mapHomotopyCategory_obj, mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app, mapDerivedCategoryFactorsh_hom_app, HomotopyCategory.instCommShiftHomologicalComplexIntUpHomFunctorMapHomotopyCategoryFactors
mapHomotopyCategoryFactors 📖	CompOp	4 math math: mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app_assoc, mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app, mapDerivedCategoryFactorsh_hom_app, HomotopyCategory.instCommShiftHomologicalComplexIntUpHomFunctorMapHomotopyCategoryFactors

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapHomotopyCategory_map 📖	mathematical	—	map HomotopyCategory instCategoryHomotopyCategory mapHomotopyCategory obj HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomotopyCategory.quotient mapHomologicalComplex preservesZeroMorphisms_of_additive	—	—
mapHomotopyCategory_obj 📖	mathematical	—	obj HomotopyCategory instCategoryHomotopyCategory mapHomotopyCategory HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomotopyCategory.quotient mapHomologicalComplex preservesZeroMorphisms_of_additive CategoryTheory.Quotient.as homotopic	—	—

CategoryTheory.NatTrans

Definitions

Name	Category	Theorems
mapHomotopyCategory 📖	CompOp	3 math math: mapHomotopyCategory_app, mapHomotopyCategory_comp, mapHomotopyCategory_id

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapHomotopyCategory_app 📖	mathematical	—	app HomotopyCategory instCategoryHomotopyCategory CategoryTheory.Functor.mapHomotopyCategory mapHomotopyCategory CategoryTheory.Functor.map HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomotopyCategory.quotient CategoryTheory.Functor.obj CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Quotient.as homotopic mapHomologicalComplex	—	CategoryTheory.Functor.preservesZeroMorphisms_of_additive
mapHomotopyCategory_comp 📖	mathematical	—	mapHomotopyCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category HomotopyCategory instCategoryHomotopyCategory CategoryTheory.Functor.mapHomotopyCategory	—	—
mapHomotopyCategory_id 📖	mathematical	—	mapHomotopyCategory CategoryTheory.CategoryStruct.id CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category HomotopyCategory instCategoryHomotopyCategory CategoryTheory.Functor.mapHomotopyCategory	—	—

HomotopyCategory

Definitions

Name	Category	Theorems
homologyFunctor 📖	CompOp	21 math math: CochainComplex.mappingCone.homologySequenceδ_triangleh, instIsHomologicalIntUpHomologyFunctor, DerivedCategory.homologyFunctorFactorsh_hom_app_quotient_obj_assoc, DerivedCategory.shiftMap_homologyFunctor_map_Qh_assoc, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc, HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_inv_app_quotient_obj, mem_quasiIso_iff, DerivedCategory.homologyFunctorFactorsh_hom_app_quotient_obj, mem_subcategoryAcyclic_iff, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj, homologyFunctor_shiftMap_assoc, homologyShiftIso_hom_app, HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_hom_app_quotient_obj, DerivedCategory.shiftMap_homologyFunctor_map_Qh, HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_hom_app_quotient_obj_assoc, instAdditiveHomologyFunctor, homologyFunctor_shiftMap, DerivedCategory.homologyFunctorFactorsh_inv_app_quotient_obj_assoc, homologyFunctor_inverts_quasiIso, DerivedCategory.homologyFunctorFactorsh_inv_app_quotient_obj, HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_inv_app_quotient_obj_assoc
homologyFunctorFactors 📖	CompOp	14 math math: CochainComplex.mappingCone.homologySequenceδ_triangleh, DerivedCategory.homologyFunctorFactorsh_hom_app_quotient_obj_assoc, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc, HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_inv_app_quotient_obj, DerivedCategory.homologyFunctorFactorsh_hom_app_quotient_obj, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj, homologyFunctor_shiftMap_assoc, homologyShiftIso_hom_app, HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_hom_app_quotient_obj, HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_hom_app_quotient_obj_assoc, homologyFunctor_shiftMap, DerivedCategory.homologyFunctorFactorsh_inv_app_quotient_obj_assoc, DerivedCategory.homologyFunctorFactorsh_inv_app_quotient_obj, HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_inv_app_quotient_obj_assoc
homotopyEquivOfIso 📖	CompOp	—
homotopyOfEq 📖	CompOp	—
homotopyOutMap 📖	CompOp	—
instInhabitedOfHasZeroObject 📖	CompOp	—
instLinear 📖	CompOp	5 math math: instLinearIntUpShiftFunctor, instLinearIntUpSingleFunctor, CategoryTheory.instLinearHomotopyCategoryMapHomotopyCategory, DerivedCategory.instLinearHomotopyCategoryIntUpQh, instLinearHomologicalComplexQuotient
instPreadditive 📖	CompOp	37 math math: spectralObjectMappingCone_δ'_app, CategoryTheory.instAdditiveHomotopyCategoryMapHomotopyCategory, CochainComplex.IsKInjective.rightOrthogonal, instIsHomologicalIntUpHomologyFunctor, quotient_map_eq_zero_iff, instAdditiveIntUpShiftFunctor, DerivedCategory.instIsTriangulatedHomotopyCategoryIntUpQh, mappingCone_triangleh_distinguished, DerivedCategory.instAdditiveHomotopyCategoryIntUpQh, instLinearIntUpShiftFunctor, instLinearIntUpSingleFunctor, instAdditiveIntUpSingleFunctor, Pretriangulated.contractible_distinguished, instIsTriangulatedIntUpSubcategoryAcyclic, instIsTriangulatedIntUp, CochainComplex.HomComplex.CohomologyClass.toHom_bijective, instIsTriangulatedIntUpMapHomotopyCategory, quasiIso_eq_subcategoryAcyclic_W, CochainComplex.IsKProjective.leftOrthogonal, CategoryTheory.instLinearHomotopyCategoryMapHomotopyCategory, CochainComplex.isKProjective_iff_leftOrthogonal, distinguished_iff_iso_trianglehOfDegreewiseSplit, spectralObjectMappingCone_ω₁, Pretriangulated.rotate_distinguished_triangle', CochainComplex.HomComplex.CohomologyClass.toHom_mk_eq_zero_iff, Pretriangulated.rotate_distinguished_triangle, instAdditiveHomologyFunctor, instAdditiveHomologicalComplexQuotient, Pretriangulated.invRotate_distinguished_triangle', DerivedCategory.instLinearHomotopyCategoryIntUpQh, CochainComplex.isKInjective_iff_rightOrthogonal, CochainComplex.HomComplex.CohomologyClass.toHom_mk, mappingConeCompTriangleh_distinguished, Pretriangulated.shift_distinguished_triangle, instLinearHomologicalComplexQuotient, CochainComplex.HomComplex.CohomologyClass.homAddEquiv_apply, DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic
instPreadditiveQuotientHomologicalComplexHomotopic 📖	CompOp	1 math math: instAdditiveHomologicalComplexQuotientHomotopicFunctor
isoOfHomotopyEquiv 📖	CompOp	2 math math: isoOfHomotopyEquiv_hom, isoOfHomotopyEquiv_inv
quotient 📖	CompOp	85 math math: spectralObjectMappingCone_δ'_app, CochainComplex.mappingConeCompTriangleh_comm₁_assoc, quotient_map_out_comp_out, CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app_assoc, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality_assoc, CategoryTheory.ProjectiveResolution.iso_hom_naturality_assoc, CategoryTheory.InjectiveResolution.iso_hom_naturality, DerivedCategory.instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality, isZero_quotient_obj_iff, CochainComplex.mappingCone.homologySequenceδ_triangleh, HomologicalComplexUpToQuasiIso.instIsLocalizationHomologicalComplexCompHomotopyCategoryQuotientQhQuasiIso, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂_assoc, CochainComplex.IsKInjective.rightOrthogonal, quotient_inverts_homotopyEquivalences, CochainComplex.IsKInjective.Qh_map_bijective, DerivedCategory.homologyFunctorFactorsh_hom_app_quotient_obj_assoc, CategoryTheory.NatTrans.mapHomotopyCategory_app, quotient_map_eq_zero_iff, instFullHomologicalComplexQuotient, isoOfHomotopyEquiv_hom, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality_assoc, instIsLocalizationHomologicalComplexIntUpHomotopyCategoryQuotientHomotopyEquivalences, eq_of_homotopy, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality_assoc, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc, instEssSurjHomologicalComplexQuotient, quasiIso_eq_quasiIso_map_quotient, quot_mk_eq_quotient_map, CategoryTheory.ProjectiveResolution.iso_hom_naturality, instFullFunctorHomologicalComplexObjWhiskeringLeftQuotient, quotient_obj_surjective, HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_inv_app_quotient_obj, instFaithfulFunctorHomologicalComplexObjWhiskeringLeftQuotient, CochainComplex.IsKProjective.Qh_map_bijective, CategoryTheory.InjectiveResolution.iso_hom_naturality_assoc, CochainComplex.HomComplex.CohomologyClass.toHom_bijective, instIsLocalizationHomologicalComplexDownHomotopyCategoryQuotientHomotopyEquivalences, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality_assoc, CochainComplex.IsKProjective.leftOrthogonal, quotient_obj_as, CategoryTheory.ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq, CochainComplex.isKProjective_iff_leftOrthogonal, DerivedCategory.homologyFunctorFactorsh_hom_app_quotient_obj, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₃, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₁, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj, homologyFunctor_shiftMap_assoc, CategoryTheory.Functor.mapHomotopyCategory_map, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₂, spectralObjectMappingCone_ω₁, CategoryTheory.Functor.mapHomotopyCategory_obj, homologyShiftIso_hom_app, CategoryTheory.InjectiveResolution.iso_inv_naturality_assoc, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality, CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app, CochainComplex.HomComplex.CohomologyClass.toHom_mk_eq_zero_iff, quotient_obj_singleFunctors_obj, ComplexShape.quotient_isLocalization, HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_hom_app_quotient_obj, HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_hom_app_quotient_obj_assoc, quotient_obj_mem_subcategoryAcyclic_iff_acyclic, instAdditiveHomologicalComplexQuotient, quotient_map_out, CategoryTheory.ProjectiveResolution.iso_inv_naturality, homologyFunctor_shiftMap, DerivedCategory.homologyFunctorFactorsh_inv_app_quotient_obj_assoc, CochainComplex.mappingConeCompTriangleh_comm₁, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality, DerivedCategory.homologyFunctorFactorsh_inv_app_quotient_obj, CochainComplex.isKInjective_iff_rightOrthogonal, CategoryTheory.ProjectiveResolution.iso_inv_naturality_assoc, CategoryTheory.InjectiveResolution.rightDerivedToHomotopyCategory_app_eq, quotient_obj_mem_subcategoryAcyclic_iff_exactAt, CochainComplex.HomComplex.CohomologyClass.toHom_mk, quotient_map_mem_quasiIso_iff, CategoryTheory.InjectiveResolution.iso_inv_naturality, isoOfHomotopyEquiv_inv, CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app, HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_inv_app_quotient_obj_assoc, instLinearHomologicalComplexQuotient, CochainComplex.HomComplex.CohomologyClass.homAddEquiv_apply, instCommShiftHomologicalComplexIntUpHomFunctorMapHomotopyCategoryFactors

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_homotopy 📖	mathematical	—	CategoryTheory.Functor.map HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomotopyCategory instCategoryHomotopyCategory quotient	—	CategoryTheory.Quotient.sound
instAdditiveHomologicalComplexQuotient 📖	mathematical	—	CategoryTheory.Functor.Additive HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomotopyCategory HomologicalComplex.instCategory instCategoryHomotopyCategory HomologicalComplex.instPreadditive instPreadditive quotient	—	—
instAdditiveHomologicalComplexQuotientHomotopicFunctor 📖	mathematical	—	CategoryTheory.Functor.Additive HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Quotient HomologicalComplex.instCategory homotopic CategoryTheory.Quotient.category HomologicalComplex.instPreadditive instPreadditiveQuotientHomologicalComplexHomotopic CategoryTheory.Quotient.functor	—	—
instAdditiveHomologyFunctor 📖	mathematical	—	CategoryTheory.Functor.Additive HomotopyCategory instCategoryHomotopyCategory instPreadditive homologyFunctor	—	CategoryTheory.Functor.additive_of_iso HomologicalComplex.instAdditiveHomologyFunctor CategoryTheory.Functor.additive_of_full_essSurj_comp instAdditiveHomologicalComplexQuotient instFullHomologicalComplexQuotient instEssSurjHomologicalComplexQuotient
instEssSurjHomologicalComplexQuotient 📖	mathematical	—	CategoryTheory.Functor.EssSurj HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomotopyCategory HomologicalComplex.instCategory instCategoryHomotopyCategory quotient	—	CategoryTheory.Quotient.essSurj_functor
instFaithfulFunctorHomologicalComplexObjWhiskeringLeftQuotient 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Functor HomotopyCategory instCategoryHomotopyCategory CategoryTheory.Functor.category HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft quotient	—	CategoryTheory.Quotient.faithful_whiskeringLeft_functor
instFullFunctorHomologicalComplexObjWhiskeringLeftQuotient 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.Functor HomotopyCategory instCategoryHomotopyCategory CategoryTheory.Functor.category HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor.whiskeringLeft quotient	—	CategoryTheory.Quotient.full_whiskeringLeft_functor
instFullHomologicalComplexQuotient 📖	mathematical	—	CategoryTheory.Functor.Full HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomotopyCategory instCategoryHomotopyCategory quotient	—	CategoryTheory.Quotient.full_functor
instHasZeroObject 📖	mathematical	—	CategoryTheory.Limits.HasZeroObject HomotopyCategory instCategoryHomotopyCategory	—	HomologicalComplex.instHasZeroObject CategoryTheory.Limits.IsZero.iff_id_eq_zero CategoryTheory.Functor.map_id CategoryTheory.Limits.id_zero CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditiveHomologicalComplexQuotient
instLinearHomologicalComplexQuotient 📖	mathematical	—	CategoryTheory.Functor.Linear HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomotopyCategory HomologicalComplex.instCategory instCategoryHomotopyCategory HomologicalComplex.instPreadditive instPreadditive HomologicalComplex.instLinear instLinear quotient	—	CategoryTheory.Quotient.linear_functor homotopy_congruence instAdditiveHomologicalComplexQuotientHomotopicFunctor
isZero_quotient_obj_iff 📖	mathematical	—	CategoryTheory.Limits.IsZero HomotopyCategory instCategoryHomotopyCategory CategoryTheory.Functor.obj HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory quotient Homotopy CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instZeroHom_1	—	CategoryTheory.Limits.IsZero.iff_id_eq_zero CategoryTheory.Functor.map_id CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditiveHomologicalComplexQuotient eq_of_homotopy
isoOfHomotopyEquiv_hom 📖	mathematical	—	CategoryTheory.Iso.hom HomotopyCategory instCategoryHomotopyCategory CategoryTheory.Functor.obj HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory quotient isoOfHomotopyEquiv CategoryTheory.Functor.map HomotopyEquiv.hom	—	—
isoOfHomotopyEquiv_inv 📖	mathematical	—	CategoryTheory.Iso.inv HomotopyCategory instCategoryHomotopyCategory CategoryTheory.Functor.obj HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory quotient isoOfHomotopyEquiv CategoryTheory.Functor.map HomotopyEquiv.inv	—	—
quot_mk_eq_quotient_map 📖	mathematical	—	Quiver.Hom HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory CategoryTheory.HomRel.CompClosure homotopic CategoryTheory.Quotient.as CategoryTheory.Functor.obj HomotopyCategory instCategoryHomotopyCategory quotient CategoryTheory.Functor.map	—	—
quotient_inverts_homotopyEquivalences 📖	mathematical	—	CategoryTheory.MorphismProperty.IsInvertedBy HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomotopyCategory instCategoryHomotopyCategory HomologicalComplex.homotopyEquivalences quotient	—	CategoryTheory.Iso.isIso_hom
quotient_map_eq_zero_iff 📖	mathematical	—	CategoryTheory.Functor.map HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomotopyCategory instCategoryHomotopyCategory quotient Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.HasZeroMorphisms.zero instPreadditive Homotopy HomologicalComplex.instZeroHom_1	—	CategoryTheory.Functor.map_zero CategoryTheory.Functor.preservesZeroMorphisms_of_additive instAdditiveHomologicalComplexQuotient eq_of_homotopy
quotient_map_out 📖	mathematical	—	CategoryTheory.Functor.map HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomotopyCategory instCategoryHomotopyCategory quotient CategoryTheory.Quotient.as homotopic Quot.out Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.HomRel.CompClosure	—	Quot.out_eq
quotient_map_out_comp_out 📖	mathematical	—	CategoryTheory.Functor.map HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomotopyCategory instCategoryHomotopyCategory quotient CategoryTheory.Quotient.as homotopic CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quot.out Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.HomRel.CompClosure	—	CategoryTheory.Functor.map_comp quotient_map_out
quotient_obj_as 📖	mathematical	—	CategoryTheory.Quotient.as HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory homotopic CategoryTheory.Functor.obj HomotopyCategory instCategoryHomotopyCategory quotient	—	—
quotient_obj_surjective 📖	mathematical	—	HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj HomologicalComplex.instCategory HomotopyCategory instCategoryHomotopyCategory quotient	—	—

SSet.Truncated

Definitions

Name	Category	Theorems
HomotopyCategory 📖	CompOp	52 math math: HomotopyCategory.BinaryProduct.iso_inv_toFunctor, HomotopyCategory.descOfTruncation_comp, mapHomotopyCategory_homMk, SSet.instIsDiscreteHomotopyCategoryObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk, HomotopyCategory.BinaryProduct.inverse_map_mkHom_id_homMk, HomotopyCategory.instSubsingletonOfObjOppositeTruncatedOfNatNatOpMkSimplexCategoryLeLenMk, HomotopyCategory.mkNatTrans_app_mk, HomotopyCategory.BinaryProduct.functorCompInverseIso_inv_app, HomotopyCategory.BinaryProduct.functorCompInverseIso_hom_app, HomotopyCategory.multiplicativeClosure_morphismPropertyHomMk, HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_fst, HomotopyCategory.lift_obj_mk, HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_snd, HomotopyCategory.instFullFreeReflOneTruncation₂QuotientFunctor, HomotopyCategory.mk_surjective, HomotopyCategory.BinaryProduct.left_unitality, HomotopyCategory.BinaryProduct.inverseCompFunctorIso_inv_app, HomotopyCategory.homMk_id, HomotopyCategory.BinaryProduct.iso_hom_toFunctor, HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_id, HomotopyCategory.BinaryProduct.mapHomotopyCategory_prod_id_comp_inverse, HomotopyCategory.BinaryProduct.functor_comp_inverse, HomotopyCategory.descOfTruncation_map_homMk, HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_homMk, hoFunctor₂_naturality, HomotopyCategory.mkNatIso_inv_app_mk, HomotopyCategory.BinaryProduct.inverse_comp_functor, HomotopyCategory.homToNerveMk_app_one, HomotopyCategory.congr_arrowMk_homMk, mapHomotopyCategory_obj, HomotopyCategory.lift_map_homMk, HomotopyCategory.BinaryProduct.associativity'Iso_hom_app, HomotopyCategory.BinaryProduct.functor_obj, HomotopyCategory.mkNatIso_hom_app_mk, HomotopyCategory.BinaryProduct.square, HomotopyCategory.BinaryProduct.inverseCompFunctorIso_hom_app, HomotopyCategory.homToNerveMk_app_edge, HomotopyCategory.BinaryProduct.associativity, HomotopyCategory.BinaryProduct.right_unitality, HomotopyCategory.BinaryProduct.associativityIso_hom_app, HomotopyCategory.homMk_comp_homMk_assoc, HomotopyCategory.homToNerveMk_app_zero, HomotopyCategory.morphismPropertyHomMk_eq_strictMap, HomotopyCategory.homMk_comp_homMk, HomotopyCategory.homToNerveMk_comp, HomotopyCategory.BinaryProduct.functor_map, HomotopyCategory.subsingleton_hom, HomotopyCategory.BinaryProduct.id_prod_mapHomotopyCategory_comp_inverse, HomotopyCategory.descOfTruncation_obj_mk, HomotopyCategory.BinaryProduct.inverse_obj, HomotopyCategory.homToNerveMk_comp_assoc, HomotopyCategory.morphismProperty_eq_top

(root)

Definitions

Name	Category	Theorems
HomotopyCategory 📖	CompOp	142 math math: HomotopyCategory.spectralObjectMappingCone_δ'_app, CochainComplex.mappingConeCompTriangleh_comm₁_assoc, HomotopyCategory.quotient_map_out_comp_out, CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_id, CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app_assoc, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality_assoc, CategoryTheory.ProjectiveResolution.iso_hom_naturality_assoc, CategoryTheory.InjectiveResolution.iso_hom_naturality, DerivedCategory.instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, HomotopyCategory.respectsIso_quasiIso, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality, HomotopyCategory.isZero_quotient_obj_iff, CochainComplex.mappingCone.homologySequenceδ_triangleh, HomologicalComplexUpToQuasiIso.instIsLocalizationHomologicalComplexCompHomotopyCategoryQuotientQhQuasiIso, CategoryTheory.instAdditiveHomotopyCategoryMapHomotopyCategory, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂_assoc, CochainComplex.IsKInjective.rightOrthogonal, HomotopyCategory.quotient_inverts_homotopyEquivalences, CochainComplex.IsKInjective.Qh_map_bijective, HomotopyCategory.instIsHomologicalIntUpHomologyFunctor, DerivedCategory.homologyFunctorFactorsh_hom_app_quotient_obj_assoc, CategoryTheory.NatTrans.mapHomotopyCategory_app, HomotopyCategory.quotient_map_eq_zero_iff, HomotopyCategory.instFullHomologicalComplexQuotient, ComplexShape.Embedding.instFaithfulHomotopyCategoryExtendHomotopyFunctor, HomotopyCategory.isoOfHomotopyEquiv_hom, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality_assoc, ComplexShape.Embedding.instFullHomotopyCategoryExtendHomotopyFunctor, CategoryTheory.NatTrans.mapHomotopyCategory_comp, HomotopyCategory.instAdditiveIntUpShiftFunctor, instIsLocalizationHomologicalComplexIntUpHomotopyCategoryQuotientHomotopyEquivalences, HomotopyCategory.eq_of_homotopy, CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh, DerivedCategory.instIsTriangulatedHomotopyCategoryIntUpQh, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality_assoc, DerivedCategory.shiftMap_homologyFunctor_map_Qh_assoc, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp_assoc, HomotopyCategory.Pretriangulated.complete_distinguished_triangle_morphism, HomotopyCategory.mappingCone_triangleh_distinguished, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc, HomotopyCategory.instEssSurjHomologicalComplexQuotient, HomotopyCategory.quasiIso_eq_quasiIso_map_quotient, HomotopyCategory.quot_mk_eq_quotient_map, DerivedCategory.instAdditiveHomotopyCategoryIntUpQh, CategoryTheory.ProjectiveResolution.iso_hom_naturality, DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhQuasiIso, CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_comp_assoc, HomotopyCategory.instFullFunctorHomologicalComplexObjWhiskeringLeftQuotient, DerivedCategory.instHasLeftCalculusOfFractionsHomotopyCategoryIntUpQuasiIso, HomotopyCategory.quotient_obj_surjective, HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_inv_app_quotient_obj, HomotopyCategory.instLinearIntUpShiftFunctor, HomotopyCategory.Pretriangulated.distinguished_cocone_triangle, HomotopyCategory.instLinearIntUpSingleFunctor, HomotopyCategory.instAdditiveIntUpSingleFunctor, HomotopyCategory.Pretriangulated.contractible_distinguished, HomotopyCategory.instFaithfulFunctorHomologicalComplexObjWhiskeringLeftQuotient, CochainComplex.IsKProjective.Qh_map_bijective, DerivedCategory.instEssSurjHomotopyCategoryIntUpQh, HomotopyCategory.instIsTriangulatedIntUpSubcategoryAcyclic, HomotopyCategory.instHasZeroObject, HomotopyCategory.instIsTriangulatedIntUp, DerivedCategory.instFaithfulFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, CategoryTheory.InjectiveResolution.iso_hom_naturality_assoc, CategoryTheory.NatTrans.mapHomotopyCategory_id, CochainComplex.HomComplex.CohomologyClass.toHom_bijective, HomotopyCategory.instIsTriangulatedIntUpMapHomotopyCategory, HomotopyCategory.mem_quasiIso_iff, HomologicalComplexUpToQuasiIso.Qh_inverts_quasiIso, instIsLocalizationHomologicalComplexDownHomotopyCategoryQuotientHomotopyEquivalences, DerivedCategory.instEssSurjArrowHomotopyCategoryIntUpMapArrowQh, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality_assoc, HomotopyCategory.quasiIso_eq_subcategoryAcyclic_W, CochainComplex.IsKProjective.leftOrthogonal, HomotopyCategory.quotient_obj_as, CategoryTheory.ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq, CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_comp, CategoryTheory.instLinearHomotopyCategoryMapHomotopyCategory, CochainComplex.isKProjective_iff_leftOrthogonal, DerivedCategory.homologyFunctorFactorsh_hom_app_quotient_obj, HomologicalComplexUpToQuasiIso.instIsLocalizationHomotopyCategoryQhQuasiIso, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₃, HomotopyCategory.mem_subcategoryAcyclic_iff, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₁, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj, HomotopyCategory.homologyFunctor_shiftMap_assoc, CategoryTheory.Functor.mapHomotopyCategory_map, HomotopyCategory.distinguished_iff_iso_trianglehOfDegreewiseSplit, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₂, HomotopyCategory.spectralObjectMappingCone_ω₁, CategoryTheory.Functor.mapHomotopyCategory_obj, HomotopyCategory.homologyShiftIso_hom_app, DerivedCategory.Qh_obj_singleFunctors_obj, CategoryTheory.InjectiveResolution.iso_inv_naturality_assoc, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality, HomotopyCategory.Pretriangulated.rotate_distinguished_triangle', CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app, DerivedCategory.instFullFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, CochainComplex.HomComplex.CohomologyClass.toHom_mk_eq_zero_iff, HomotopyCategory.Pretriangulated.rotate_distinguished_triangle, HomotopyCategory.quotient_obj_singleFunctors_obj, ComplexShape.quotient_isLocalization, HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_hom_app_quotient_obj, DerivedCategory.shiftMap_homologyFunctor_map_Qh, HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_hom_app_quotient_obj_assoc, HomotopyCategory.instAdditiveHomologyFunctor, HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic, HomotopyCategory.instAdditiveHomologicalComplexQuotient, HomotopyCategory.quotient_map_out, CategoryTheory.ProjectiveResolution.iso_inv_naturality, HomotopyCategory.homologyFunctor_shiftMap, HomotopyCategory.Pretriangulated.invRotate_distinguished_triangle', DerivedCategory.instLinearHomotopyCategoryIntUpQh, DerivedCategory.homologyFunctorFactorsh_inv_app_quotient_obj_assoc, HomotopyCategory.Pretriangulated.isomorphic_distinguished, CochainComplex.mappingConeCompTriangleh_comm₁, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality, HomotopyCategory.homologyFunctor_inverts_quasiIso, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_id, DerivedCategory.homologyFunctorFactorsh_inv_app_quotient_obj, CochainComplex.isKInjective_iff_rightOrthogonal, CategoryTheory.ProjectiveResolution.iso_inv_naturality_assoc, CategoryTheory.InjectiveResolution.rightDerivedToHomotopyCategory_app_eq, HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_exactAt, DerivedCategory.isIso_Qh_map_iff, CochainComplex.HomComplex.CohomologyClass.toHom_mk, HomotopyCategory.quotient_map_mem_quasiIso_iff, CategoryTheory.InjectiveResolution.iso_inv_naturality, HomotopyCategory.mappingConeCompTriangleh_distinguished, HomotopyCategory.isoOfHomotopyEquiv_inv, CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app, HomotopyCategory.instIsClosedUnderIsomorphismsIntUpSubcategoryAcyclic, HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_inv_app_quotient_obj_assoc, HomotopyCategory.Pretriangulated.shift_distinguished_triangle, HomotopyCategory.instLinearHomologicalComplexQuotient, CochainComplex.HomComplex.CohomologyClass.homAddEquiv_apply, HomotopyCategory.instCommShiftHomologicalComplexIntUpHomFunctorMapHomotopyCategoryFactors, DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic, DerivedCategory.instHasRightCalculusOfFractionsHomotopyCategoryIntUpQuasiIso
homotopic 📖	CompOp	9 math math: HomotopyCategory.quotient_map_out_comp_out, HomotopyCategory.instAdditiveHomologicalComplexQuotientHomotopicFunctor, CategoryTheory.NatTrans.mapHomotopyCategory_app, HomotopyCategory.quot_mk_eq_quotient_map, HomotopyCategory.instIsCompatibleWithShiftHomologicalComplexIntUpHomotopic, HomotopyCategory.quotient_obj_as, homotopy_congruence, CategoryTheory.Functor.mapHomotopyCategory_obj, HomotopyCategory.quotient_map_out
instCategoryHomotopyCategory 📖	CompOp	142 math math: HomotopyCategory.spectralObjectMappingCone_δ'_app, CochainComplex.mappingConeCompTriangleh_comm₁_assoc, HomotopyCategory.quotient_map_out_comp_out, CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_id, CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app_assoc, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality_assoc, CategoryTheory.ProjectiveResolution.iso_hom_naturality_assoc, CategoryTheory.InjectiveResolution.iso_hom_naturality, DerivedCategory.instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, HomotopyCategory.respectsIso_quasiIso, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality, HomotopyCategory.isZero_quotient_obj_iff, CochainComplex.mappingCone.homologySequenceδ_triangleh, HomologicalComplexUpToQuasiIso.instIsLocalizationHomologicalComplexCompHomotopyCategoryQuotientQhQuasiIso, CategoryTheory.instAdditiveHomotopyCategoryMapHomotopyCategory, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂_assoc, CochainComplex.IsKInjective.rightOrthogonal, HomotopyCategory.quotient_inverts_homotopyEquivalences, CochainComplex.IsKInjective.Qh_map_bijective, HomotopyCategory.instIsHomologicalIntUpHomologyFunctor, DerivedCategory.homologyFunctorFactorsh_hom_app_quotient_obj_assoc, CategoryTheory.NatTrans.mapHomotopyCategory_app, HomotopyCategory.quotient_map_eq_zero_iff, HomotopyCategory.instFullHomologicalComplexQuotient, ComplexShape.Embedding.instFaithfulHomotopyCategoryExtendHomotopyFunctor, HomotopyCategory.isoOfHomotopyEquiv_hom, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality_assoc, ComplexShape.Embedding.instFullHomotopyCategoryExtendHomotopyFunctor, CategoryTheory.NatTrans.mapHomotopyCategory_comp, HomotopyCategory.instAdditiveIntUpShiftFunctor, instIsLocalizationHomologicalComplexIntUpHomotopyCategoryQuotientHomotopyEquivalences, HomotopyCategory.eq_of_homotopy, CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh, DerivedCategory.instIsTriangulatedHomotopyCategoryIntUpQh, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality_assoc, DerivedCategory.shiftMap_homologyFunctor_map_Qh_assoc, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp_assoc, HomotopyCategory.Pretriangulated.complete_distinguished_triangle_morphism, HomotopyCategory.mappingCone_triangleh_distinguished, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc, HomotopyCategory.instEssSurjHomologicalComplexQuotient, HomotopyCategory.quasiIso_eq_quasiIso_map_quotient, HomotopyCategory.quot_mk_eq_quotient_map, DerivedCategory.instAdditiveHomotopyCategoryIntUpQh, CategoryTheory.ProjectiveResolution.iso_hom_naturality, DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhQuasiIso, CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_comp_assoc, HomotopyCategory.instFullFunctorHomologicalComplexObjWhiskeringLeftQuotient, DerivedCategory.instHasLeftCalculusOfFractionsHomotopyCategoryIntUpQuasiIso, HomotopyCategory.quotient_obj_surjective, HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_inv_app_quotient_obj, HomotopyCategory.instLinearIntUpShiftFunctor, HomotopyCategory.Pretriangulated.distinguished_cocone_triangle, HomotopyCategory.instLinearIntUpSingleFunctor, HomotopyCategory.instAdditiveIntUpSingleFunctor, HomotopyCategory.Pretriangulated.contractible_distinguished, HomotopyCategory.instFaithfulFunctorHomologicalComplexObjWhiskeringLeftQuotient, CochainComplex.IsKProjective.Qh_map_bijective, DerivedCategory.instEssSurjHomotopyCategoryIntUpQh, HomotopyCategory.instIsTriangulatedIntUpSubcategoryAcyclic, HomotopyCategory.instHasZeroObject, HomotopyCategory.instIsTriangulatedIntUp, DerivedCategory.instFaithfulFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, CategoryTheory.InjectiveResolution.iso_hom_naturality_assoc, CategoryTheory.NatTrans.mapHomotopyCategory_id, CochainComplex.HomComplex.CohomologyClass.toHom_bijective, HomotopyCategory.instIsTriangulatedIntUpMapHomotopyCategory, HomotopyCategory.mem_quasiIso_iff, HomologicalComplexUpToQuasiIso.Qh_inverts_quasiIso, instIsLocalizationHomologicalComplexDownHomotopyCategoryQuotientHomotopyEquivalences, DerivedCategory.instEssSurjArrowHomotopyCategoryIntUpMapArrowQh, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality_assoc, HomotopyCategory.quasiIso_eq_subcategoryAcyclic_W, CochainComplex.IsKProjective.leftOrthogonal, HomotopyCategory.quotient_obj_as, CategoryTheory.ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq, CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_comp, CategoryTheory.instLinearHomotopyCategoryMapHomotopyCategory, CochainComplex.isKProjective_iff_leftOrthogonal, DerivedCategory.homologyFunctorFactorsh_hom_app_quotient_obj, HomologicalComplexUpToQuasiIso.instIsLocalizationHomotopyCategoryQhQuasiIso, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₃, HomotopyCategory.mem_subcategoryAcyclic_iff, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₁, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj, HomotopyCategory.homologyFunctor_shiftMap_assoc, CategoryTheory.Functor.mapHomotopyCategory_map, HomotopyCategory.distinguished_iff_iso_trianglehOfDegreewiseSplit, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₂, HomotopyCategory.spectralObjectMappingCone_ω₁, CategoryTheory.Functor.mapHomotopyCategory_obj, HomotopyCategory.homologyShiftIso_hom_app, DerivedCategory.Qh_obj_singleFunctors_obj, CategoryTheory.InjectiveResolution.iso_inv_naturality_assoc, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality, HomotopyCategory.Pretriangulated.rotate_distinguished_triangle', CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app, DerivedCategory.instFullFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, CochainComplex.HomComplex.CohomologyClass.toHom_mk_eq_zero_iff, HomotopyCategory.Pretriangulated.rotate_distinguished_triangle, HomotopyCategory.quotient_obj_singleFunctors_obj, ComplexShape.quotient_isLocalization, HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_hom_app_quotient_obj, DerivedCategory.shiftMap_homologyFunctor_map_Qh, HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_hom_app_quotient_obj_assoc, HomotopyCategory.instAdditiveHomologyFunctor, HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic, HomotopyCategory.instAdditiveHomologicalComplexQuotient, HomotopyCategory.quotient_map_out, CategoryTheory.ProjectiveResolution.iso_inv_naturality, HomotopyCategory.homologyFunctor_shiftMap, HomotopyCategory.Pretriangulated.invRotate_distinguished_triangle', DerivedCategory.instLinearHomotopyCategoryIntUpQh, DerivedCategory.homologyFunctorFactorsh_inv_app_quotient_obj_assoc, HomotopyCategory.Pretriangulated.isomorphic_distinguished, CochainComplex.mappingConeCompTriangleh_comm₁, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality, HomotopyCategory.homologyFunctor_inverts_quasiIso, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_id, DerivedCategory.homologyFunctorFactorsh_inv_app_quotient_obj, CochainComplex.isKInjective_iff_rightOrthogonal, CategoryTheory.ProjectiveResolution.iso_inv_naturality_assoc, CategoryTheory.InjectiveResolution.rightDerivedToHomotopyCategory_app_eq, HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_exactAt, DerivedCategory.isIso_Qh_map_iff, CochainComplex.HomComplex.CohomologyClass.toHom_mk, HomotopyCategory.quotient_map_mem_quasiIso_iff, CategoryTheory.InjectiveResolution.iso_inv_naturality, HomotopyCategory.mappingConeCompTriangleh_distinguished, HomotopyCategory.isoOfHomotopyEquiv_inv, CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app, HomotopyCategory.instIsClosedUnderIsomorphismsIntUpSubcategoryAcyclic, HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_inv_app_quotient_obj_assoc, HomotopyCategory.Pretriangulated.shift_distinguished_triangle, HomotopyCategory.instLinearHomologicalComplexQuotient, CochainComplex.HomComplex.CohomologyClass.homAddEquiv_apply, HomotopyCategory.instCommShiftHomologicalComplexIntUpHomFunctorMapHomotopyCategoryFactors, DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic, DerivedCategory.instHasRightCalculusOfFractionsHomotopyCategoryIntUpQuasiIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homotopy_congruence 📖	mathematical	—	CategoryTheory.Congruence HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory homotopic	—	—

---

← Back to Index