FibrantObjectHomotopy

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

Statistics

Metric	Count
Definitions HoCat, iResolutionObj, localizerMorphismResolution, resolution, resolutionCompToLocalizationNatTrans, resolutionMap, resolutionObj, toHoCatCompToLocalizationIso, toLocalization, ιCompResolutionNatTrans, homRel, instCategoryWithWeakEquivalencesHoCat, localizerMorphism, toHoCat, toHoCatLocalizerMorphism	15
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_isCofibrant_src, homRel_iff_leftHomotopyRel, instCofibrationIResolutionObj, instFullHoCatToHoCat, instHasQuotientWeakEquivalencesHomRel, instIsFibrantObjFunctorWeakEquivalencesLocalizerMorphism, instIsFibrantResolutionObj, instIsIsoFunctorResolutionCompToLocalizationNatTrans, instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences, instIsLocalizationCompHoCatToHoCatWeakEquivalences, instIsLocalizationCompιWeakEquivalences, instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism, instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism, instIsStableUnderPostcompHomRel, instIsStableUnderPrecompHomRel, instWeakEquivalenceHoCatAppιCompResolutionNatTrans, instWeakEquivalenceIResolutionObj, localizerMorphism_functor, toHoCat_map_eq, toHoCat_map_eq_iff, toHoCat_obj_surjective, weakEquivalence_toHoCat_map_iff	31
Total	46

HomotopicalAlgebra.FibrantObject

Definitions

Name	Category	Theorems
HoCat 📖	CompOp	15 math math: instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences, instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism, instIsLocalizationCompHoCatToHoCatWeakEquivalences, toHoCat_map_eq_iff, weakEquivalence_toHoCat_map_iff, instWeakEquivalenceHoCatAppιCompResolutionNatTrans, instFullHoCatToHoCat, toHoCat_map_eq, HoCat.resolutionObj_hom_ext, HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject_obj, HoCat.ιCompResolutionNatTrans_app, toHoCat_obj_surjective, instIsIsoFunctorResolutionCompToLocalizationNatTrans, HoCat.localizerMorphismResolution_functor, HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject_map_toHoCat_map
homRel 📖	CompOp	20 math math: instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences, instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism, instIsLocalizationCompHoCatToHoCatWeakEquivalences, toHoCat_map_eq_iff, weakEquivalence_toHoCat_map_iff, homRel_iff_leftHomotopyRel, instWeakEquivalenceHoCatAppιCompResolutionNatTrans, instFullHoCatToHoCat, HoCat.resolutionObj_hom_ext, instIsStableUnderPrecompHomRel, HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject_obj, homRel_equivalence_of_isCofibrant_src, instHasQuotientWeakEquivalencesHomRel, HoCat.ιCompResolutionNatTrans_app, toHoCat_obj_surjective, instIsIsoFunctorResolutionCompToLocalizationNatTrans, factorsThroughLocalization, HoCat.localizerMorphismResolution_functor, instIsStableUnderPostcompHomRel, HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject_map_toHoCat_map
instCategoryWithWeakEquivalencesHoCat 📖	CompOp	4 math math: instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism, weakEquivalence_toHoCat_map_iff, instWeakEquivalenceHoCatAppιCompResolutionNatTrans, HoCat.localizerMorphismResolution_functor
localizerMorphism 📖	CompOp	7 math math: instHasRightResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism, localizerMorphism_functor, instIsConnectedRightResolutionWeakEquivalencesLocalizerMorphism, instWeakEquivalenceWWeakEquivalences, instIsFibrantObjFunctorWeakEquivalencesLocalizerMorphism, instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism, instIsRightDerivabilityStructureWeakEquivalencesLocalizerMorphism
toHoCat 📖	CompOp	12 math math: instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences, instIsLocalizationCompHoCatToHoCatWeakEquivalences, toHoCat_map_eq_iff, weakEquivalence_toHoCat_map_iff, instWeakEquivalenceHoCatAppιCompResolutionNatTrans, instFullHoCatToHoCat, toHoCat_map_eq, HoCat.resolutionObj_hom_ext, HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject_obj, HoCat.ιCompResolutionNatTrans_app, toHoCat_obj_surjective, HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject_map_toHoCat_map
toHoCatLocalizerMorphism 📖	CompOp	1 math math: instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
factorsThroughLocalization 📖	mathematical	—	HomRel.FactorsThroughLocalization HomotopicalAlgebra.FibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects homRel HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b HomotopicalAlgebra.LeftHomotopyRel.exists_very_good_cylinder instIsFibrantObjFibrantObjects CategoryTheory.areEqualizedByLocalization_iff CategoryTheory.Functor.q_isLocalization HomotopicalAlgebra.Cylinder.instIsFibrantIOfIsVeryGood CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition HomotopicalAlgebra.instIsMultiplicativeFibrations HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemTrivialCofibrationsFibrations CategoryTheory.Localization.inverts HomotopicalAlgebra.Cylinder.weakEquivalence_π CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Functor.map_comp HomotopicalAlgebra.Precylinder.i₀_π CategoryTheory.Functor.map_id HomotopicalAlgebra.Precylinder.i₁_π HomotopicalAlgebra.Precylinder.LeftHomotopy.h₀ HomotopicalAlgebra.Precylinder.LeftHomotopy.h₁
homRel_equivalence_of_isCofibrant_src 📖	mathematical	—	Quiver.Hom HomotopicalAlgebra.FibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Fintype.instPEmpty CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects homRel	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Equivalence.comap HomotopicalAlgebra.LeftHomotopyRel.equivalence
homRel_iff_leftHomotopyRel 📖	mathematical	—	homRel HomotopicalAlgebra.LeftHomotopyRel HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences CategoryTheory.ObjectProperty.FullSubcategory.obj HomotopicalAlgebra.fibrantObjects HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Fintype.instPEmpty CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype
instCofibrationIResolutionObj 📖	mathematical	—	HomotopicalAlgebra.Cofibration HoCat.resolutionObj HoCat.iResolutionObj HomotopicalAlgebra.ModelCategory.categoryWithCofibrations	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype HoCat.exists_resolution
instFullHoCatToHoCat 📖	mathematical	—	CategoryTheory.Functor.Full HomotopicalAlgebra.FibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects HoCat CategoryTheory.Quotient.category homRel toHoCat	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.Quotient.full_functor
instHasQuotientWeakEquivalencesHomRel 📖	mathematical	—	CategoryTheory.MorphismProperty.HasQuotient HomotopicalAlgebra.FibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences homRel instIsStableUnderPrecompHomRel instIsStableUnderPostcompHomRel	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype instIsStableUnderPrecompHomRel instIsStableUnderPostcompHomRel HomotopicalAlgebra.Cylinder.LeftHomotopy.weakEquivalence_iff HomotopicalAlgebra.ModelCategory.cm2 CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities HomotopicalAlgebra.instIsMultiplicativeWeakEquivalencesOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsOfIsStableUnderComposition HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemTrivialCofibrationsFibrations HomotopicalAlgebra.ModelCategory.cm3a CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toIsStableUnderComposition
instIsFibrantObjFunctorWeakEquivalencesLocalizerMorphism 📖	mathematical	—	HomotopicalAlgebra.IsFibrant HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Fintype.instPEmpty CategoryTheory.Functor.obj HomotopicalAlgebra.FibrantObject CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects CategoryTheory.LocalizerMorphism.functor HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences localizerMorphism	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype instIsFibrantObjFibrantObjects
instIsFibrantResolutionObj 📖	mathematical	—	HomotopicalAlgebra.IsFibrant HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Fintype.instPEmpty HoCat.resolutionObj	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype HoCat.exists_resolution
instIsIsoFunctorResolutionCompToLocalizationNatTrans 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.FibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects homRel HoCat.resolution HoCat.toLocalization HoCat.resolutionCompToLocalizationNatTrans	—	CategoryTheory.NatTrans.isIso_iff_isIso_app CategoryTheory.Localization.inverts HomotopicalAlgebra.weakEquivalence_iff instWeakEquivalenceIResolutionObj
instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor HomotopicalAlgebra.FibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects CategoryTheory.Functor.category CategoryTheory.Functor.comp HoCat CategoryTheory.Quotient.category homRel toHoCat ι HoCat.resolution CategoryTheory.Functor.whiskerRight HoCat.ιCompResolutionNatTrans	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.NatTrans.isIso_iff_isIso_app CategoryTheory.Localization.inverts HomotopicalAlgebra.weakEquivalence_iff instWeakEquivalenceHoCatAppιCompResolutionNatTrans
instIsLocalizationCompHoCatToHoCatWeakEquivalences 📖	mathematical	—	CategoryTheory.Functor.IsLocalization HomotopicalAlgebra.FibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects CategoryTheory.Functor.comp HoCat CategoryTheory.Quotient.category homRel toHoCat HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.isLocalization instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism
instIsLocalizationCompιWeakEquivalences 📖	mathematical	—	CategoryTheory.Functor.IsLocalization HomotopicalAlgebra.FibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects CategoryTheory.Functor.comp ι HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.isLocalization instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism
instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism 📖	mathematical	—	CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence HomotopicalAlgebra.FibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Fintype.instPEmpty HoCat CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects CategoryTheory.Quotient.category homRel HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences instCategoryWithWeakEquivalencesHoCat toHoCatLocalizerMorphism	—	HomRel.FactorsThroughLocalization.isLocalizedEquivalence CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype factorsThroughLocalization CategoryTheory.MorphismProperty.eq_inverseImage_quotientFunctor instIsStableUnderPrecompHomRel instIsStableUnderPostcompHomRel instHasQuotientWeakEquivalencesHomRel
instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism 📖	mathematical	—	CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence HomotopicalAlgebra.FibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences localizerMorphism	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a 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.FibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects homRel	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype HomotopicalAlgebra.LeftHomotopyRel.postcomp
instIsStableUnderPrecompHomRel 📖	mathematical	—	CategoryTheory.HomRel.IsStableUnderPrecomp HomotopicalAlgebra.FibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects homRel	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype HomotopicalAlgebra.LeftHomotopyRel.precomp instIsFibrantObjFibrantObjects
instWeakEquivalenceHoCatAppιCompResolutionNatTrans 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.FibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects homRel CategoryTheory.Functor.obj CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Fintype.instPEmpty toHoCat CategoryTheory.Functor.comp ι HoCat.resolution CategoryTheory.NatTrans.app HoCat.ιCompResolutionNatTrans instCategoryWithWeakEquivalencesHoCat	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype weakEquivalence_toHoCat_map_iff HomotopicalAlgebra.weakEquivalence_iff_of_objectProperty instWeakEquivalenceIResolutionObj
instWeakEquivalenceIResolutionObj 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence HoCat.resolutionObj HoCat.iResolutionObj HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype HoCat.exists_resolution
localizerMorphism_functor 📖	mathematical	—	CategoryTheory.LocalizerMorphism.functor HomotopicalAlgebra.FibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences localizerMorphism ι	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype
toHoCat_map_eq 📖	mathematical	homRel	CategoryTheory.Functor.map HomotopicalAlgebra.FibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects HoCat CategoryTheory.Quotient.category toHoCat	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.Quotient.sound
toHoCat_map_eq_iff 📖	mathematical	—	CategoryTheory.Functor.map HomotopicalAlgebra.FibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects HoCat CategoryTheory.Quotient.category homRel toHoCat	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b CategoryTheory.Functor.homRel_iff CategoryTheory.Quotient.functor_homRel_eq_compClosure_eqvGen CategoryTheory.HomRel.compClosure_eq_self instIsStableUnderPrecompHomRel instIsStableUnderPostcompHomRel Equivalence.eqvGen_eq homRel_equivalence_of_isCofibrant_src
toHoCat_obj_surjective 📖	mathematical	—	HomotopicalAlgebra.FibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Fintype.instPEmpty HoCat CategoryTheory.Functor.obj CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects CategoryTheory.Quotient.category homRel toHoCat	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype
weakEquivalence_toHoCat_map_iff 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.FibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects homRel CategoryTheory.Functor.obj CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Fintype.instPEmpty toHoCat CategoryTheory.Functor.map instCategoryWithWeakEquivalencesHoCat HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.MorphismProperty.quotient_iff instIsStableUnderPrecompHomRel instIsStableUnderPostcompHomRel instHasQuotientWeakEquivalencesHomRel

HomotopicalAlgebra.FibrantObject.HoCat

Definitions

Name	Category	Theorems
iResolutionObj 📖	CompOp	6 math math: exists_resolution_map, resolutionMap_fac, HomotopicalAlgebra.FibrantObject.instWeakEquivalenceIResolutionObj, HomotopicalAlgebra.FibrantObject.instCofibrationIResolutionObj, ιCompResolutionNatTrans_app, resolutionMap_fac_assoc
localizerMorphismResolution 📖	CompOp	1 math math: localizerMorphismResolution_functor
resolution 📖	CompOp	5 math math: HomotopicalAlgebra.FibrantObject.instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences, HomotopicalAlgebra.FibrantObject.instWeakEquivalenceHoCatAppιCompResolutionNatTrans, ιCompResolutionNatTrans_app, HomotopicalAlgebra.FibrantObject.instIsIsoFunctorResolutionCompToLocalizationNatTrans, localizerMorphismResolution_functor
resolutionCompToLocalizationNatTrans 📖	CompOp	1 math math: HomotopicalAlgebra.FibrantObject.instIsIsoFunctorResolutionCompToLocalizationNatTrans
resolutionMap 📖	CompOp	3 math math: resolutionMap_fac, weakEquivalence_resolutionMap_iff, resolutionMap_fac_assoc
resolutionObj 📖	CompOp	8 math math: exists_resolution_map, resolutionMap_fac, HomotopicalAlgebra.FibrantObject.instWeakEquivalenceIResolutionObj, weakEquivalence_resolutionMap_iff, HomotopicalAlgebra.FibrantObject.instCofibrationIResolutionObj, HomotopicalAlgebra.FibrantObject.instIsFibrantResolutionObj, ιCompResolutionNatTrans_app, resolutionMap_fac_assoc
toHoCatCompToLocalizationIso 📖	CompOp	—
toLocalization 📖	CompOp	1 math math: HomotopicalAlgebra.FibrantObject.instIsIsoFunctorResolutionCompToLocalizationNatTrans
ιCompResolutionNatTrans 📖	CompOp	3 math math: HomotopicalAlgebra.FibrantObject.instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences, HomotopicalAlgebra.FibrantObject.instWeakEquivalenceHoCatAppιCompResolutionNatTrans, ιCompResolutionNatTrans_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_resolution 📖	mathematical	—	HomotopicalAlgebra.Cofibration HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.WeakEquivalence HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype HomotopicalAlgebra.ModelCategory.cm5a HomotopicalAlgebra.isFibrant_iff_of_isTerminal CategoryTheory.MorphismProperty.instRespectsIsoOfIsStableUnderRetracts HomotopicalAlgebra.ModelCategory.cm3b HomotopicalAlgebra.instFibrationPTrivialCofibrationsFibrations HomotopicalAlgebra.instCofibrationITrivialCofibrationsFibrations HomotopicalAlgebra.instWeakEquivalenceITrivialCofibrationsFibrations
exists_resolution_map 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct resolutionObj iResolutionObj	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.Limits.terminal.comp_from CategoryTheory.sq_hasLift_of_hasLiftingProperty HomotopicalAlgebra.ModelCategory.cm4a HomotopicalAlgebra.FibrantObject.instCofibrationIResolutionObj HomotopicalAlgebra.FibrantObject.instWeakEquivalenceIResolutionObj HomotopicalAlgebra.FibrantObject.instIsFibrantResolutionObj CategoryTheory.CommSq.fac_left
localizerMorphismResolution_functor 📖	mathematical	—	CategoryTheory.LocalizerMorphism.functor HomotopicalAlgebra.FibrantObject.HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.FibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects HomotopicalAlgebra.FibrantObject.homRel HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences HomotopicalAlgebra.FibrantObject.instCategoryWithWeakEquivalencesHoCat localizerMorphismResolution resolution	—	—
resolutionMap_fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct resolutionObj iResolutionObj resolutionMap	—	exists_resolution_map
resolutionMap_fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct resolutionObj iResolutionObj resolutionMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' resolutionMap_fac
resolutionObj_hom_ext 📖	mathematical	HomotopicalAlgebra.RightHomotopyRel HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct resolutionObj iResolutionObj	CategoryTheory.Functor.map HomotopicalAlgebra.FibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects HomotopicalAlgebra.FibrantObject.HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.FibrantObject.homRel HomotopicalAlgebra.FibrantObject.toHoCat HomotopicalAlgebra.FibrantObject.instIsFibrantResolutionObj HomotopicalAlgebra.FibrantObject.homMk	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype HomotopicalAlgebra.FibrantObject.toHoCat_map_eq HomotopicalAlgebra.FibrantObject.instIsFibrantResolutionObj HomotopicalAlgebra.FibrantObject.homRel_iff_leftHomotopyRel HomotopicalAlgebra.RightHomotopyRel.leftHomotopyRel HomotopicalAlgebra.RightHomotopyClass.mk_eq_mk_iff HomotopicalAlgebra.RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalence HomotopicalAlgebra.FibrantObject.instCofibrationIResolutionObj HomotopicalAlgebra.FibrantObject.instWeakEquivalenceIResolutionObj
weakEquivalence_resolutionMap_iff 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence resolutionObj resolutionMap HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	HomotopicalAlgebra.weakEquivalence_precomp_iff HomotopicalAlgebra.ModelCategory.cm2 HomotopicalAlgebra.FibrantObject.instWeakEquivalenceIResolutionObj resolutionMap_fac HomotopicalAlgebra.weakEquivalence_postcomp_iff
ιCompResolutionNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app HomotopicalAlgebra.FibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects HomotopicalAlgebra.FibrantObject.HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.FibrantObject.homRel HomotopicalAlgebra.FibrantObject.toHoCat CategoryTheory.Functor.comp HomotopicalAlgebra.FibrantObject.ι resolution ιCompResolutionNatTrans CategoryTheory.Functor.map resolutionObj CategoryTheory.Functor.obj CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj iResolutionObj	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype

---

← Back to Index