CofibrantObjectHomotopy

📁 Source: Mathlib/AlgebraicTopology/ModelCategory/CofibrantObjectHomotopy.lean

Statistics

Metric	Count
Definitions HoCat, localizerMorphismResolution, pResolutionObj, resolution, resolutionCompToLocalizationNatTrans, resolutionMap, resolutionObj, toHoCatCompToLocalizationIso, toLocalization, toπCompToLocalizationIso, ιCompResolutionNatTrans, homRel, instCategoryWithWeakEquivalencesHoCat, localizerMorphism, toHoCat, toHoCatLocalizerMorphism	16
Theorems exists_resolution, exists_resolution_map, localizerMorphismResolution_functor, resolutionMap_fac, resolutionMap_fac_assoc, resolutionObj_hom_ext, weakEquivalence_resolutionMap_iff, ιCompResolutionNatTrans_app, factorsThroughLocalization, homRel_equivalence_of_isFibrant_tgt, homRel_iff_rightHomotopyRel, instFibrationPResolutionObj, instFullHoCatToHoCat, instHasQuotientWeakEquivalencesHomRel, instIsCofibrantObjFunctorWeakEquivalencesLocalizerMorphism, instIsCofibrantResolutionObj, instIsIsoFunctorResolutionCompToLocalizationNatTrans, instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences, instIsLocalizationCompHoCatToHoCatWeakEquivalences, instIsLocalizationCompιWeakEquivalences, instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism, instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism, instIsStableUnderPostcompHomRel, instIsStableUnderPrecompHomRel, instWeakEquivalenceHoCatAppιCompResolutionNatTrans, instWeakEquivalencePResolutionObj, localizerMorphism_functor, toHoCat_map_eq, toHoCat_map_eq_iff, toHoCat_obj_surjective, weakEquivalence_toHoCat_map_iff	31
Total	47

HomotopicalAlgebra.CofibrantObject

Definitions

Name	Category	Theorems
HoCat 📖	CompOp	30 math math: HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject_obj, instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism, toHoCat_map_eq_iff, instFaithfulHoCatHoCatιCofibrantObject, bifibrantResolutionMap_fac', toHoCat_obj_surjective, instFullHoCatToHoCat, instIsLocalizationCompHoCatToHoCatWeakEquivalences, instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences, HoCat.resolutionObj_hom_ext, instIsIsoFunctorHoCatAdjCounit', instIsIsoFunctorHoCatCounitHoCatAdj, instIsIsoFunctorResolutionCompToLocalizationNatTrans, HoCat.bifibrantResolution_map, HoCat.adjCounitIso_inv_app, HoCat.adjUnit_app, HoCat.bifibrantResolution_obj, instIsIsoHoCatAppAdjCounit', instWeakEquivalenceHoCatAppιCompResolutionNatTrans, instWeakEquivalenceHoCatAppAdjUnit, instFullHoCatHoCatιCofibrantObject, instIsLocalizationHoCatHoCatBifibrantResolutionWeakEquivalences, HoCat.ιCompResolutionNatTrans_app, instWeakEquivalenceHoCatAppUnitHoCatAdj, weakEquivalence_toHoCat_map_iff, HoCat.localizerMorphismResolution_functor, HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject_map_toHoCat_map, HoCat.adjCounit'_app, bifibrantResolutionMap_fac'_assoc, toHoCat_map_eq
homRel 📖	CompOp	35 math math: HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject_obj, homRel_equivalence_of_isFibrant_tgt, instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism, toHoCat_map_eq_iff, instFaithfulHoCatHoCatιCofibrantObject, bifibrantResolutionMap_fac', toHoCat_obj_surjective, instFullHoCatToHoCat, instIsLocalizationCompHoCatToHoCatWeakEquivalences, instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences, HoCat.resolutionObj_hom_ext, instIsIsoFunctorHoCatAdjCounit', instIsIsoFunctorHoCatCounitHoCatAdj, instIsIsoFunctorResolutionCompToLocalizationNatTrans, HoCat.bifibrantResolution_map, HoCat.adjCounitIso_inv_app, HoCat.adjUnit_app, HoCat.bifibrantResolution_obj, instIsStableUnderPrecompHomRel, instIsIsoHoCatAppAdjCounit', factorsThroughLocalization, instWeakEquivalenceHoCatAppιCompResolutionNatTrans, instWeakEquivalenceHoCatAppAdjUnit, instFullHoCatHoCatιCofibrantObject, instIsLocalizationHoCatHoCatBifibrantResolutionWeakEquivalences, instHasQuotientWeakEquivalencesHomRel, HoCat.ιCompResolutionNatTrans_app, instWeakEquivalenceHoCatAppUnitHoCatAdj, weakEquivalence_toHoCat_map_iff, HoCat.localizerMorphismResolution_functor, HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject_map_toHoCat_map, HoCat.adjCounit'_app, instIsStableUnderPostcompHomRel, homRel_iff_rightHomotopyRel, bifibrantResolutionMap_fac'_assoc
instCategoryWithWeakEquivalencesHoCat 📖	CompOp	7 math math: instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism, instWeakEquivalenceHoCatAppιCompResolutionNatTrans, instWeakEquivalenceHoCatAppAdjUnit, instIsLocalizationHoCatHoCatBifibrantResolutionWeakEquivalences, instWeakEquivalenceHoCatAppUnitHoCatAdj, weakEquivalence_toHoCat_map_iff, HoCat.localizerMorphismResolution_functor
localizerMorphism 📖	CompOp	7 math math: instHasLeftResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism, instIsCofibrantObjFunctorWeakEquivalencesLocalizerMorphism, instIsConnectedLeftResolutionWeakEquivalencesLocalizerMorphism, instIsLeftDerivabilityStructureWeakEquivalencesLocalizerMorphism, instWeakEquivalenceWWeakEquivalences, localizerMorphism_functor, instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism
toHoCat 📖	CompOp	17 math math: HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject_obj, toHoCat_map_eq_iff, bifibrantResolutionMap_fac', toHoCat_obj_surjective, instFullHoCatToHoCat, instIsLocalizationCompHoCatToHoCatWeakEquivalences, instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences, HoCat.resolutionObj_hom_ext, HoCat.bifibrantResolution_map, HoCat.adjUnit_app, HoCat.bifibrantResolution_obj, instWeakEquivalenceHoCatAppιCompResolutionNatTrans, HoCat.ιCompResolutionNatTrans_app, weakEquivalence_toHoCat_map_iff, HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject_map_toHoCat_map, bifibrantResolutionMap_fac'_assoc, toHoCat_map_eq
toHoCatLocalizerMorphism 📖	CompOp	1 math math: instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
factorsThroughLocalization 📖	mathematical	—	HomRel.FactorsThroughLocalization HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects homRel HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.RightHomotopyRel.exists_very_good_pathObject instIsCofibrantObjCofibrantObjects CategoryTheory.areEqualizedByLocalization_iff CategoryTheory.Functor.q_isLocalization HomotopicalAlgebra.PathObject.instIsCofibrantPOfIsVeryGood CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition HomotopicalAlgebra.instIsMultiplicativeCofibrations HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemCofibrationsTrivialFibrations CategoryTheory.Localization.inverts HomotopicalAlgebra.PathObject.weakEquivalence_ι CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Functor.map_comp HomotopicalAlgebra.PrepathObject.ι_p₀ HomotopicalAlgebra.PrepathObject.ι_p₁ HomotopicalAlgebra.PrepathObject.RightHomotopy.h₀ HomotopicalAlgebra.PrepathObject.RightHomotopy.h₁
homRel_equivalence_of_isFibrant_tgt 📖	mathematical	—	Quiver.Hom HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects homRel	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Equivalence.comap HomotopicalAlgebra.RightHomotopyRel.equivalence
homRel_iff_rightHomotopyRel 📖	mathematical	—	homRel HomotopicalAlgebra.RightHomotopyRel HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences CategoryTheory.ObjectProperty.FullSubcategory.obj HomotopicalAlgebra.cofibrantObjects HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype
instFibrationPResolutionObj 📖	mathematical	—	HomotopicalAlgebra.Fibration HoCat.resolutionObj HoCat.pResolutionObj HomotopicalAlgebra.ModelCategory.categoryWithFibrations	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype HoCat.exists_resolution
instFullHoCatToHoCat 📖	mathematical	—	CategoryTheory.Functor.Full HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects HoCat CategoryTheory.Quotient.category homRel toHoCat	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Quotient.full_functor
instHasQuotientWeakEquivalencesHomRel 📖	mathematical	—	CategoryTheory.MorphismProperty.HasQuotient HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences homRel instIsStableUnderPrecompHomRel instIsStableUnderPostcompHomRel	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype instIsStableUnderPrecompHomRel instIsStableUnderPostcompHomRel HomotopicalAlgebra.PathObject.RightHomotopy.weakEquivalence_iff HomotopicalAlgebra.ModelCategory.cm2 CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities HomotopicalAlgebra.instIsMultiplicativeWeakEquivalencesOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsOfIsStableUnderComposition HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemTrivialCofibrationsFibrations HomotopicalAlgebra.ModelCategory.cm3a CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toIsStableUnderComposition
instIsCofibrantObjFunctorWeakEquivalencesLocalizerMorphism 📖	mathematical	—	HomotopicalAlgebra.IsCofibrant HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.Functor.obj HomotopicalAlgebra.CofibrantObject CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects CategoryTheory.LocalizerMorphism.functor HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences localizerMorphism	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype instIsCofibrantObjCofibrantObjects
instIsCofibrantResolutionObj 📖	mathematical	—	HomotopicalAlgebra.IsCofibrant HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HoCat.resolutionObj	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype HoCat.exists_resolution
instIsIsoFunctorResolutionCompToLocalizationNatTrans 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects homRel HoCat.resolution HoCat.toLocalization HoCat.resolutionCompToLocalizationNatTrans	—	CategoryTheory.NatTrans.isIso_iff_isIso_app CategoryTheory.Localization.inverts HomotopicalAlgebra.weakEquivalence_iff instWeakEquivalencePResolutionObj
instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects CategoryTheory.Functor.category CategoryTheory.Functor.comp HoCat CategoryTheory.Quotient.category homRel ι HoCat.resolution toHoCat CategoryTheory.Functor.whiskerRight HoCat.ιCompResolutionNatTrans	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.NatTrans.isIso_iff_isIso_app CategoryTheory.Localization.inverts HomotopicalAlgebra.weakEquivalence_iff instWeakEquivalenceHoCatAppιCompResolutionNatTrans
instIsLocalizationCompHoCatToHoCatWeakEquivalences 📖	mathematical	—	CategoryTheory.Functor.IsLocalization HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects CategoryTheory.Functor.comp HoCat CategoryTheory.Quotient.category homRel toHoCat HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.isLocalization instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism
instIsLocalizationCompιWeakEquivalences 📖	mathematical	—	CategoryTheory.Functor.IsLocalization HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects CategoryTheory.Functor.comp ι HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.isLocalization instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism
instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism 📖	mathematical	—	CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HoCat CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects CategoryTheory.Quotient.category homRel HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences instCategoryWithWeakEquivalencesHoCat toHoCatLocalizerMorphism	—	HomRel.FactorsThroughLocalization.isLocalizedEquivalence CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype factorsThroughLocalization CategoryTheory.MorphismProperty.eq_inverseImage_quotientFunctor instIsStableUnderPrecompHomRel instIsStableUnderPostcompHomRel instHasQuotientWeakEquivalencesHomRel
instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism 📖	mathematical	—	CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences localizerMorphism	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype instIsLocalizationCompHoCatToHoCatWeakEquivalences CategoryTheory.Functor.q_isLocalization instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences instIsIsoFunctorResolutionCompToLocalizationNatTrans CategoryTheory.Equivalence.isEquivalence_functor CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.mk'
instIsStableUnderPostcompHomRel 📖	mathematical	—	CategoryTheory.HomRel.IsStableUnderPostcomp HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects homRel	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype HomotopicalAlgebra.RightHomotopyRel.postcomp instIsCofibrantObjCofibrantObjects
instIsStableUnderPrecompHomRel 📖	mathematical	—	CategoryTheory.HomRel.IsStableUnderPrecomp HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects homRel	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype HomotopicalAlgebra.RightHomotopyRel.precomp
instWeakEquivalenceHoCatAppιCompResolutionNatTrans 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects homRel CategoryTheory.Functor.obj CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.Functor.comp ι HoCat.resolution toHoCat CategoryTheory.NatTrans.app HoCat.ιCompResolutionNatTrans instCategoryWithWeakEquivalencesHoCat	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype weakEquivalence_toHoCat_map_iff HomotopicalAlgebra.weakEquivalence_iff_of_objectProperty instWeakEquivalencePResolutionObj
instWeakEquivalencePResolutionObj 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence HoCat.resolutionObj HoCat.pResolutionObj HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype HoCat.exists_resolution
localizerMorphism_functor 📖	mathematical	—	CategoryTheory.LocalizerMorphism.functor HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences localizerMorphism ι	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype
toHoCat_map_eq 📖	mathematical	homRel	CategoryTheory.Functor.map HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects HoCat CategoryTheory.Quotient.category toHoCat	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Quotient.sound
toHoCat_map_eq_iff 📖	mathematical	—	CategoryTheory.Functor.map HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects HoCat CategoryTheory.Quotient.category homRel toHoCat	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a CategoryTheory.Functor.homRel_iff CategoryTheory.Quotient.functor_homRel_eq_compClosure_eqvGen CategoryTheory.HomRel.compClosure_eq_self instIsStableUnderPrecompHomRel instIsStableUnderPostcompHomRel Equivalence.eqvGen_eq homRel_equivalence_of_isFibrant_tgt
toHoCat_obj_surjective 📖	mathematical	—	HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HoCat CategoryTheory.Functor.obj CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects CategoryTheory.Quotient.category homRel toHoCat	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype
weakEquivalence_toHoCat_map_iff 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects homRel CategoryTheory.Functor.obj CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty toHoCat CategoryTheory.Functor.map instCategoryWithWeakEquivalencesHoCat HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.MorphismProperty.quotient_iff instIsStableUnderPrecompHomRel instIsStableUnderPostcompHomRel instHasQuotientWeakEquivalencesHomRel

HomotopicalAlgebra.CofibrantObject.HoCat

Definitions

Name	Category	Theorems
localizerMorphismResolution 📖	CompOp	1 math math: localizerMorphismResolution_functor
pResolutionObj 📖	CompOp	6 math math: HomotopicalAlgebra.CofibrantObject.instFibrationPResolutionObj, exists_resolution_map, resolutionMap_fac, HomotopicalAlgebra.CofibrantObject.instWeakEquivalencePResolutionObj, resolutionMap_fac_assoc, ιCompResolutionNatTrans_app
resolution 📖	CompOp	5 math math: HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences, HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorResolutionCompToLocalizationNatTrans, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppιCompResolutionNatTrans, ιCompResolutionNatTrans_app, localizerMorphismResolution_functor
resolutionCompToLocalizationNatTrans 📖	CompOp	1 math math: HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorResolutionCompToLocalizationNatTrans
resolutionMap 📖	CompOp	3 math math: weakEquivalence_resolutionMap_iff, resolutionMap_fac, resolutionMap_fac_assoc
resolutionObj 📖	CompOp	8 math math: HomotopicalAlgebra.CofibrantObject.instFibrationPResolutionObj, weakEquivalence_resolutionMap_iff, HomotopicalAlgebra.CofibrantObject.instIsCofibrantResolutionObj, exists_resolution_map, resolutionMap_fac, HomotopicalAlgebra.CofibrantObject.instWeakEquivalencePResolutionObj, resolutionMap_fac_assoc, ιCompResolutionNatTrans_app
toHoCatCompToLocalizationIso 📖	CompOp	—
toLocalization 📖	CompOp	1 math math: HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorResolutionCompToLocalizationNatTrans
toπCompToLocalizationIso 📖	CompOp	—
ιCompResolutionNatTrans 📖	CompOp	3 math math: HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppιCompResolutionNatTrans, ιCompResolutionNatTrans_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_resolution 📖	mathematical	—	HomotopicalAlgebra.Fibration HomotopicalAlgebra.ModelCategory.categoryWithFibrations HomotopicalAlgebra.WeakEquivalence HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype HomotopicalAlgebra.ModelCategory.cm5b HomotopicalAlgebra.isCofibrant_iff_of_isInitial CategoryTheory.MorphismProperty.instRespectsIsoOfIsStableUnderRetracts HomotopicalAlgebra.ModelCategory.cm3c HomotopicalAlgebra.instCofibrationICofibrationsTrivialFibrations HomotopicalAlgebra.instFibrationPCofibrationsTrivialFibrations HomotopicalAlgebra.instWeakEquivalencePCofibrationsTrivialFibrations
exists_resolution_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct resolutionObj pResolutionObj	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.initial.to_comp CategoryTheory.sq_hasLift_of_hasLiftingProperty HomotopicalAlgebra.ModelCategory.cm4b HomotopicalAlgebra.CofibrantObject.instIsCofibrantResolutionObj HomotopicalAlgebra.CofibrantObject.instFibrationPResolutionObj HomotopicalAlgebra.CofibrantObject.instWeakEquivalencePResolutionObj CategoryTheory.CommSq.fac_right
localizerMorphismResolution_functor 📖	mathematical	—	CategoryTheory.LocalizerMorphism.functor HomotopicalAlgebra.CofibrantObject.HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects HomotopicalAlgebra.CofibrantObject.homRel HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences HomotopicalAlgebra.CofibrantObject.instCategoryWithWeakEquivalencesHoCat localizerMorphismResolution resolution	—	—
resolutionMap_fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct resolutionObj resolutionMap pResolutionObj	—	exists_resolution_map
resolutionMap_fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct resolutionObj resolutionMap pResolutionObj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' resolutionMap_fac
resolutionObj_hom_ext 📖	mathematical	HomotopicalAlgebra.LeftHomotopyRel HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct resolutionObj pResolutionObj	CategoryTheory.Functor.map HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects HomotopicalAlgebra.CofibrantObject.HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.CofibrantObject.homRel HomotopicalAlgebra.CofibrantObject.toHoCat HomotopicalAlgebra.CofibrantObject.instIsCofibrantResolutionObj HomotopicalAlgebra.CofibrantObject.homMk	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype HomotopicalAlgebra.CofibrantObject.toHoCat_map_eq HomotopicalAlgebra.CofibrantObject.instIsCofibrantResolutionObj HomotopicalAlgebra.CofibrantObject.homRel_iff_rightHomotopyRel HomotopicalAlgebra.LeftHomotopyRel.rightHomotopyRel HomotopicalAlgebra.LeftHomotopyClass.mk_eq_mk_iff Function.Bijective.injective HomotopicalAlgebra.LeftHomotopyClass.postcomp_bijective_of_fibration_of_weakEquivalence HomotopicalAlgebra.CofibrantObject.instFibrationPResolutionObj HomotopicalAlgebra.CofibrantObject.instWeakEquivalencePResolutionObj
weakEquivalence_resolutionMap_iff 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence resolutionObj resolutionMap HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	HomotopicalAlgebra.weakEquivalence_postcomp_iff HomotopicalAlgebra.ModelCategory.cm2 HomotopicalAlgebra.CofibrantObject.instWeakEquivalencePResolutionObj resolutionMap_fac HomotopicalAlgebra.weakEquivalence_precomp_iff
ιCompResolutionNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects HomotopicalAlgebra.CofibrantObject.HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.CofibrantObject.homRel CategoryTheory.Functor.comp HomotopicalAlgebra.CofibrantObject.ι resolution HomotopicalAlgebra.CofibrantObject.toHoCat ιCompResolutionNatTrans CategoryTheory.Functor.map resolutionObj CategoryTheory.Functor.obj CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj pResolutionObj	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype

---

← Back to Index