BifibrantObjectHomotopy

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

Statistics

Metric	Count
Definitions HoCat, homEquivLeft, homEquivRight, ιCofibrantObject, ιFibrantObject, homRel, localizerMorphism, strictUniversalPropertyFixedTargetToHoCat, toHoCat, toHoCatCompιCofibrantObject, toHoCatCompιFibrantObject, ιCofibrantObjectLocalizerMorphism, ιFibrantObjectLocalizerMorphism, adj, adjCounit', adjCounitIso, adjUnit, bifibrantResolution, bifibrantResolution', bifibrantResolutionMap, bifibrantResolutionObj, iBifibrantResolutionObj	22
Theorems homEquivLeft_apply, homEquivLeft_symm_apply, homEquivRight_apply, homEquivRight_symm_apply, ιCofibrantObject_map_toHoCat_map, ιCofibrantObject_obj, ιFibrantObject_map_toHoCat_map, ιFibrantObject_obj, homRel_iff_leftHomotopyRel, homRel_iff_rightHomotopyRel, instCongruenceHomRel, instFullHoCatToHoCat, instIsIsoHoCatMapToHoCatOfWeakEquivalence, instIsLocalizationCompCofibrantObjectιCofibrantObjectWeakEquivalences, instIsLocalizationCompFibrantObjectιFibrantObjectWeakEquivalences, instIsLocalizationCompιWeakEquivalences, instIsLocalizationHoCatToHoCatWeakEquivalences, instIsLocalizedEquivalenceCofibrantObjectWeakEquivalencesιCofibrantObjectLocalizerMorphism, instIsLocalizedEquivalenceFibrantObjectWeakEquivalencesιFibrantObjectLocalizerMorphism, instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism, instIsStableUnderPostcompHomRel, instIsStableUnderPrecompHomRel, instLocallySmallHoCat, inverts_iff_factors, toHoCat_map_eq, toHoCat_map_eq_iff, toHoCat_obj_surjective, ιCofibrantObjectLocalizerMorphism_functor, ιFibrantObjectLocalizerMorphism_functor, adjCounit'_app, adjCounitIso_inv_app, adjUnit_app, bifibrantResolution'_map, bifibrantResolution'_obj, bifibrantResolution_map, bifibrantResolution_obj, bifibrantResolutionMap_fac, bifibrantResolutionMap_fac', bifibrantResolutionMap_fac'_assoc, bifibrantResolutionMap_fac_assoc, bifibrantResolutionObj_hom_ext, exists_bifibrant, exists_bifibrant_map, instCofibrationHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, instFaithfulHoCatHoCatιCofibrantObject, instFullHoCatHoCatιCofibrantObject, instIsFibrantObjιBifibrantObjectιCofibrantObject, instIsIsoFunctorHoCatAdjCounit', instIsIsoFunctorHoCatCounitHoCatAdj, instIsIsoHoCatAppAdjCounit', instIsLocalizationHoCatHoCatBifibrantResolutionWeakEquivalences, instWeakEquivalenceBifibrantObjectBifibrantResolutionMap, instWeakEquivalenceHoCatAppAdjUnit, instWeakEquivalenceHoCatAppUnitHoCatAdj, instWeakEquivalenceHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, instWeakEquivalenceIBifibrantResolutionObj, locallySmall_of_isLocalization	57
Total	79

HomotopicalAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locallySmall_of_isLocalization 📖	mathematical	—	CategoryTheory.LocallySmall	—	CategoryTheory.locallySmall_of_faithful CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits ModelCategory.cm1b Finite.of_fintype CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits ModelCategory.cm1a BifibrantObject.instIsLocalizationHoCatToHoCatWeakEquivalences CategoryTheory.LocalizerMorphism.localizedFunctor_isEquivalence BifibrantObject.instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism CategoryTheory.Functor.IsEquivalence.faithful CategoryTheory.Functor.isEquivalence_inv BifibrantObject.instLocallySmallHoCat

HomotopicalAlgebra.BifibrantObject

Definitions

Name	Category	Theorems
HoCat 📖	CompOp	30 math math: HoCat.ιCofibrantObject_obj, instLocallySmallHoCat, HoCat.homEquivRight_apply, HomotopicalAlgebra.CofibrantObject.instFaithfulHoCatHoCatιCofibrantObject, HoCat.homEquivLeft_symm_apply, HoCat.homEquivLeft_apply, toHoCat_map_eq, instIsIsoHoCatMapToHoCatOfWeakEquivalence, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution'_obj, instIsLocalizationHoCatToHoCatWeakEquivalences, toHoCat_obj_surjective, HoCat.homEquivRight_symm_apply, HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorHoCatAdjCounit', HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorHoCatCounitHoCatAdj, HoCat.ιFibrantObject_obj, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution_map, HomotopicalAlgebra.CofibrantObject.HoCat.adjCounitIso_inv_app, HomotopicalAlgebra.CofibrantObject.HoCat.adjUnit_app, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution_obj, toHoCat_map_eq_iff, HomotopicalAlgebra.CofibrantObject.instIsIsoHoCatAppAdjCounit', HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppAdjUnit, HomotopicalAlgebra.CofibrantObject.instFullHoCatHoCatιCofibrantObject, HomotopicalAlgebra.CofibrantObject.instIsLocalizationHoCatHoCatBifibrantResolutionWeakEquivalences, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution'_map, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppUnitHoCatAdj, HoCat.ιCofibrantObject_map_toHoCat_map, HomotopicalAlgebra.CofibrantObject.HoCat.adjCounit'_app, instFullHoCatToHoCat, HoCat.ιFibrantObject_map_toHoCat_map
homRel 📖	CompOp	35 math math: HoCat.ιCofibrantObject_obj, instLocallySmallHoCat, HoCat.homEquivRight_apply, HomotopicalAlgebra.CofibrantObject.instFaithfulHoCatHoCatιCofibrantObject, HoCat.homEquivLeft_symm_apply, HoCat.homEquivLeft_apply, toHoCat_map_eq, instIsIsoHoCatMapToHoCatOfWeakEquivalence, instCongruenceHomRel, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution'_obj, instIsLocalizationHoCatToHoCatWeakEquivalences, toHoCat_obj_surjective, HoCat.homEquivRight_symm_apply, HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorHoCatAdjCounit', HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorHoCatCounitHoCatAdj, instIsStableUnderPostcompHomRel, HoCat.ιFibrantObject_obj, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution_map, homRel_iff_leftHomotopyRel, HomotopicalAlgebra.CofibrantObject.HoCat.adjCounitIso_inv_app, HomotopicalAlgebra.CofibrantObject.HoCat.adjUnit_app, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution_obj, toHoCat_map_eq_iff, HomotopicalAlgebra.CofibrantObject.instIsIsoHoCatAppAdjCounit', instIsStableUnderPrecompHomRel, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppAdjUnit, HomotopicalAlgebra.CofibrantObject.instFullHoCatHoCatιCofibrantObject, HomotopicalAlgebra.CofibrantObject.instIsLocalizationHoCatHoCatBifibrantResolutionWeakEquivalences, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution'_map, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppUnitHoCatAdj, HoCat.ιCofibrantObject_map_toHoCat_map, homRel_iff_rightHomotopyRel, HomotopicalAlgebra.CofibrantObject.HoCat.adjCounit'_app, instFullHoCatToHoCat, HoCat.ιFibrantObject_map_toHoCat_map
localizerMorphism 📖	CompOp	1 math math: instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism
strictUniversalPropertyFixedTargetToHoCat 📖	CompOp	—
toHoCat 📖	CompOp	20 math math: HoCat.ιCofibrantObject_obj, HoCat.homEquivRight_apply, HoCat.homEquivLeft_symm_apply, HoCat.homEquivLeft_apply, toHoCat_map_eq, instIsIsoHoCatMapToHoCatOfWeakEquivalence, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution'_obj, instIsLocalizationHoCatToHoCatWeakEquivalences, toHoCat_obj_surjective, HoCat.homEquivRight_symm_apply, HoCat.ιFibrantObject_obj, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution_map, HomotopicalAlgebra.CofibrantObject.HoCat.adjCounitIso_inv_app, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution_obj, toHoCat_map_eq_iff, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution'_map, HoCat.ιCofibrantObject_map_toHoCat_map, HomotopicalAlgebra.CofibrantObject.HoCat.adjCounit'_app, instFullHoCatToHoCat, HoCat.ιFibrantObject_map_toHoCat_map
toHoCatCompιCofibrantObject 📖	CompOp	—
toHoCatCompιFibrantObject 📖	CompOp	—
ιCofibrantObjectLocalizerMorphism 📖	CompOp	2 math math: instIsLocalizedEquivalenceCofibrantObjectWeakEquivalencesιCofibrantObjectLocalizerMorphism, ιCofibrantObjectLocalizerMorphism_functor
ιFibrantObjectLocalizerMorphism 📖	CompOp	2 math math: ιFibrantObjectLocalizerMorphism_functor, instIsLocalizedEquivalenceFibrantObjectWeakEquivalencesιFibrantObjectLocalizerMorphism

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homRel_iff_leftHomotopyRel 📖	mathematical	—	homRel HomotopicalAlgebra.LeftHomotopyRel HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences CategoryTheory.ObjectProperty.FullSubcategory.obj HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	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 homRel_iff_rightHomotopyRel HomotopicalAlgebra.leftHomotopyRel_iff_rightHomotopyRel instIsCofibrantObjBifibrantObjects instIsFibrantObjBifibrantObjects
homRel_iff_rightHomotopyRel 📖	mathematical	—	homRel HomotopicalAlgebra.RightHomotopyRel HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences CategoryTheory.ObjectProperty.FullSubcategory.obj HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	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
instCongruenceHomRel 📖	mathematical	—	CategoryTheory.Congruence HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects 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 instIsStableUnderPrecompHomRel instIsStableUnderPostcompHomRel HomotopicalAlgebra.RightHomotopyRel.refl HomotopicalAlgebra.RightHomotopyRel.symm HomotopicalAlgebra.RightHomotopyRel.trans instIsFibrantObjBifibrantObjects
instFullHoCatToHoCat 📖	mathematical	—	CategoryTheory.Functor.Full HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects 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.Quotient.full_functor
instIsIsoHoCatMapToHoCatOfWeakEquivalence 📖	mathematical	—	CategoryTheory.IsIso HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects homRel CategoryTheory.Functor.obj CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a toHoCat CategoryTheory.Functor.map	—	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.Localization.inverts instIsLocalizationHoCatToHoCatWeakEquivalences HomotopicalAlgebra.weakEquivalence_iff
instIsLocalizationCompCofibrantObjectιCofibrantObjectWeakEquivalences 📖	mathematical	—	CategoryTheory.Functor.IsLocalization HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects CategoryTheory.Functor.comp HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.cofibrantObjects ιCofibrantObject HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype
instIsLocalizationCompFibrantObjectιFibrantObjectWeakEquivalences 📖	mathematical	—	CategoryTheory.Functor.IsLocalization HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects CategoryTheory.Functor.comp HomotopicalAlgebra.FibrantObject HomotopicalAlgebra.fibrantObjects ιFibrantObject HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype
instIsLocalizationCompιWeakEquivalences 📖	mathematical	—	CategoryTheory.Functor.IsLocalization HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects CategoryTheory.Functor.comp ι HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	—
instIsLocalizationHoCatToHoCatWeakEquivalences 📖	mathematical	—	CategoryTheory.Functor.IsLocalization HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HoCat CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects CategoryTheory.Quotient.category homRel toHoCat HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	CategoryTheory.Functor.IsLocalization.mk' 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
instIsLocalizedEquivalenceCofibrantObjectWeakEquivalencesιCofibrantObjectLocalizerMorphism 📖	mathematical	—	CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.CofibrantObject CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.cofibrantObjects HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences ιCofibrantObjectLocalizerMorphism	—	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 HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorHoCatCounitHoCatAdj CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.mk' instIsLocalizationHoCatToHoCatWeakEquivalences HomotopicalAlgebra.CofibrantObject.instIsLocalizationCompHoCatToHoCatWeakEquivalences HomotopicalAlgebra.CofibrantObject.instIsLocalizationHoCatHoCatBifibrantResolutionWeakEquivalences CategoryTheory.Functor.isEquivalence_refl
instIsLocalizedEquivalenceFibrantObjectWeakEquivalencesιFibrantObjectLocalizerMorphism 📖	mathematical	—	CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.FibrantObject CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.fibrantObjects HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences ιFibrantObjectLocalizerMorphism	—	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.LocalizerMorphism.IsLocalizedEquivalence.of_isLocalization_of_isLocalization HomotopicalAlgebra.FibrantObject.instIsLocalizationCompιWeakEquivalences CategoryTheory.Functor.q_isLocalization
instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism 📖	mathematical	—	CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences localizerMorphism	—	—
instIsStableUnderPostcompHomRel 📖	mathematical	—	CategoryTheory.HomRel.IsStableUnderPostcomp HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects 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 HomotopicalAlgebra.RightHomotopyRel.postcomp instIsCofibrantObjBifibrantObjects
instIsStableUnderPrecompHomRel 📖	mathematical	—	CategoryTheory.HomRel.IsStableUnderPrecomp HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects 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 HomotopicalAlgebra.RightHomotopyRel.precomp
instLocallySmallHoCat 📖	mathematical	—	CategoryTheory.LocallySmall HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects homRel	—	CategoryTheory.Quotient.instLocallySmall CategoryTheory.locallySmall_fullSubcategory
inverts_iff_factors 📖	mathematical	—	CategoryTheory.MorphismProperty.IsInvertedBy HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences CategoryTheory.Functor.map	—	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.Limits.hasLimitOfHasLimitsOfShape HomotopicalAlgebra.RightHomotopyRel.exists_very_good_pathObject instIsCofibrantObjBifibrantObjects HomotopicalAlgebra.isCofibrant_of_cofibration CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition HomotopicalAlgebra.instIsMultiplicativeCofibrations HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemCofibrationsTrivialFibrations HomotopicalAlgebra.PathObject.IsVeryGood.cofibration_ι instIsFibrantObjBifibrantObjects HomotopicalAlgebra.PathObject.instIsFibrantP HomotopicalAlgebra.instIsMultiplicativeFibrations HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemTrivialCofibrationsFibrations HomotopicalAlgebra.instIsStableUnderBaseChangeFibrations HomotopicalAlgebra.PathObject.IsVeryGood.toIsGood HomotopicalAlgebra.weakEquivalence_iff HomotopicalAlgebra.weakEquivalence_iff_of_objectProperty HomotopicalAlgebra.PrepathObject.RightHomotopy.h₀ CategoryTheory.Functor.map_comp HomotopicalAlgebra.PrepathObject.RightHomotopy.h₁ CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso HomotopicalAlgebra.PrepathObject.ι_p₀ CategoryTheory.Functor.map_id HomotopicalAlgebra.PrepathObject.ι_p₁ HomotopicalAlgebra.RightHomotopyClass.whitehead
toHoCat_map_eq 📖	mathematical	homRel	CategoryTheory.Functor.map HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects 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.Quotient.sound
toHoCat_map_eq_iff 📖	mathematical	—	CategoryTheory.Functor.map HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects 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.Quotient.functor_map_eq_iff instCongruenceHomRel
toHoCat_obj_surjective 📖	mathematical	—	HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HoCat CategoryTheory.Functor.obj CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects 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
ιCofibrantObjectLocalizerMorphism_functor 📖	mathematical	—	CategoryTheory.LocalizerMorphism.functor HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.CofibrantObject CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.cofibrantObjects HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences ιCofibrantObjectLocalizerMorphism ιCofibrantObject	—	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
ιFibrantObjectLocalizerMorphism_functor 📖	mathematical	—	CategoryTheory.LocalizerMorphism.functor HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.FibrantObject CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.fibrantObjects HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences ιFibrantObjectLocalizerMorphism ιFibrantObject	—	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

HomotopicalAlgebra.BifibrantObject.HoCat

Definitions

Name	Category	Theorems
homEquivLeft 📖	CompOp	1 math math: homEquivLeft_apply
homEquivRight 📖	CompOp	3 math math: homEquivRight_apply, homEquivLeft_symm_apply, homEquivRight_symm_apply
ιCofibrantObject 📖	CompOp	12 math math: ιCofibrantObject_obj, HomotopicalAlgebra.CofibrantObject.instFaithfulHoCatHoCatιCofibrantObject, HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorHoCatAdjCounit', HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorHoCatCounitHoCatAdj, HomotopicalAlgebra.CofibrantObject.HoCat.adjCounitIso_inv_app, HomotopicalAlgebra.CofibrantObject.HoCat.adjUnit_app, HomotopicalAlgebra.CofibrantObject.instIsIsoHoCatAppAdjCounit', HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppAdjUnit, HomotopicalAlgebra.CofibrantObject.instFullHoCatHoCatιCofibrantObject, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppUnitHoCatAdj, ιCofibrantObject_map_toHoCat_map, HomotopicalAlgebra.CofibrantObject.HoCat.adjCounit'_app
ιFibrantObject 📖	CompOp	2 math math: ιFibrantObject_obj, ιFibrantObject_map_toHoCat_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homEquivLeft_apply 📖	mathematical	—	DFunLike.coe Equiv HomotopicalAlgebra.LeftHomotopyClass HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences Quiver.Hom HomotopicalAlgebra.BifibrantObject.HoCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Quotient.category HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.homRel CategoryTheory.Functor.obj CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.BifibrantObject.toHoCat EquivLike.toFunLike Equiv.instEquivLike homEquivLeft CategoryTheory.Functor.map HomotopicalAlgebra.BifibrantObject.homMk	—	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
homEquivLeft_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom HomotopicalAlgebra.BifibrantObject.HoCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Quotient.category HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.homRel CategoryTheory.Functor.obj CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.BifibrantObject.toHoCat HomotopicalAlgebra.RightHomotopyClass HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquivRight CategoryTheory.Functor.map HomotopicalAlgebra.BifibrantObject.homMk	—	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
homEquivRight_apply 📖	mathematical	—	DFunLike.coe Equiv HomotopicalAlgebra.RightHomotopyClass HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences Quiver.Hom HomotopicalAlgebra.BifibrantObject.HoCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Quotient.category HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.homRel CategoryTheory.Functor.obj CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.BifibrantObject.toHoCat EquivLike.toFunLike Equiv.instEquivLike homEquivRight CategoryTheory.Functor.map HomotopicalAlgebra.BifibrantObject.homMk	—	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
homEquivRight_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom HomotopicalAlgebra.BifibrantObject.HoCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Quotient.category HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.homRel CategoryTheory.Functor.obj CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.BifibrantObject.toHoCat HomotopicalAlgebra.RightHomotopyClass HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homEquivRight CategoryTheory.Functor.map HomotopicalAlgebra.BifibrantObject.homMk	—	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
ιCofibrantObject_map_toHoCat_map 📖	mathematical	—	CategoryTheory.Functor.map HomotopicalAlgebra.BifibrantObject.HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.homRel HomotopicalAlgebra.CofibrantObject.HoCat HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.cofibrantObjects HomotopicalAlgebra.CofibrantObject.homRel ιCofibrantObject CategoryTheory.Functor.obj CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.BifibrantObject.toHoCat HomotopicalAlgebra.CofibrantObject.toHoCat CategoryTheory.ObjectProperty.FullSubcategory.obj HomotopicalAlgebra.BifibrantObject.instIsCofibrantObjBifibrantObjects HomotopicalAlgebra.CofibrantObject.homMk CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	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
ιCofibrantObject_obj 📖	mathematical	—	CategoryTheory.Functor.obj HomotopicalAlgebra.BifibrantObject.HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.homRel HomotopicalAlgebra.CofibrantObject.HoCat HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.cofibrantObjects HomotopicalAlgebra.CofibrantObject.homRel ιCofibrantObject CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.BifibrantObject.toHoCat HomotopicalAlgebra.CofibrantObject.toHoCat HomotopicalAlgebra.BifibrantObject.ιCofibrantObject	—	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
ιFibrantObject_map_toHoCat_map 📖	mathematical	—	CategoryTheory.Functor.map HomotopicalAlgebra.BifibrantObject.HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.homRel HomotopicalAlgebra.FibrantObject.HoCat HomotopicalAlgebra.FibrantObject HomotopicalAlgebra.fibrantObjects HomotopicalAlgebra.FibrantObject.homRel ιFibrantObject CategoryTheory.Functor.obj CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.BifibrantObject.toHoCat HomotopicalAlgebra.FibrantObject.toHoCat CategoryTheory.ObjectProperty.FullSubcategory.obj HomotopicalAlgebra.BifibrantObject.instIsFibrantObjBifibrantObjects HomotopicalAlgebra.FibrantObject.homMk CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory	—	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
ιFibrantObject_obj 📖	mathematical	—	CategoryTheory.Functor.obj HomotopicalAlgebra.BifibrantObject.HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.homRel HomotopicalAlgebra.FibrantObject.HoCat HomotopicalAlgebra.FibrantObject HomotopicalAlgebra.fibrantObjects HomotopicalAlgebra.FibrantObject.homRel ιFibrantObject CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.BifibrantObject.toHoCat HomotopicalAlgebra.FibrantObject.toHoCat HomotopicalAlgebra.BifibrantObject.ιFibrantObject	—	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

HomotopicalAlgebra.CofibrantObject

Definitions

Name	Category	Theorems
bifibrantResolutionMap 📖	CompOp	7 math math: instWeakEquivalenceBifibrantObjectBifibrantResolutionMap, bifibrantResolutionMap_fac', bifibrantResolutionMap_fac, HoCat.bifibrantResolution_map, bifibrantResolutionMap_fac_assoc, HoCat.bifibrantResolution'_map, bifibrantResolutionMap_fac'_assoc
bifibrantResolutionObj 📖	CompOp	16 math math: instWeakEquivalenceBifibrantObjectBifibrantResolutionMap, bifibrantResolutionMap_fac', HoCat.bifibrantResolution'_obj, bifibrantResolutionMap_fac, exists_bifibrant_map, HoCat.bifibrantResolution_map, bifibrantResolutionMap_fac_assoc, HoCat.adjCounitIso_inv_app, HoCat.adjUnit_app, instWeakEquivalenceIBifibrantResolutionObj, HoCat.bifibrantResolution_obj, HoCat.bifibrantResolution'_map, instWeakEquivalenceHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, HoCat.adjCounit'_app, instCofibrationHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, bifibrantResolutionMap_fac'_assoc
iBifibrantResolutionObj 📖	CompOp	11 math math: bifibrantResolutionMap_fac', bifibrantResolutionMap_fac, exists_bifibrant_map, bifibrantResolutionMap_fac_assoc, HoCat.adjCounitIso_inv_app, HoCat.adjUnit_app, instWeakEquivalenceIBifibrantResolutionObj, instWeakEquivalenceHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, HoCat.adjCounit'_app, instCofibrationHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, bifibrantResolutionMap_fac'_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bifibrantResolutionMap_fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects CategoryTheory.Functor.obj HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.ιCofibrantObject bifibrantResolutionObj CategoryTheory.ObjectProperty.FullSubcategory.obj HomotopicalAlgebra.BifibrantObject.instIsCofibrantObjBifibrantObjects iBifibrantResolutionObj homMk HomotopicalAlgebra.bifibrantObjects_le_cofibrantObject CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory bifibrantResolutionMap	—	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 exists_bifibrant_map
bifibrantResolutionMap_fac' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HoCat CategoryTheory.Category.toCategoryStruct 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 HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.ιCofibrantObject bifibrantResolutionObj CategoryTheory.ObjectProperty.FullSubcategory.obj HomotopicalAlgebra.BifibrantObject.instIsCofibrantObjBifibrantObjects CategoryTheory.Functor.map iBifibrantResolutionObj homMk HomotopicalAlgebra.bifibrantObjects_le_cofibrantObject CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory bifibrantResolutionMap	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.Functor.congr_map CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.BifibrantObject.instIsCofibrantObjBifibrantObjects HomotopicalAlgebra.bifibrantObjects_le_cofibrantObject bifibrantResolutionMap_fac
bifibrantResolutionMap_fac'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HoCat CategoryTheory.Category.toCategoryStruct 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 HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.ιCofibrantObject bifibrantResolutionObj CategoryTheory.Functor.map iBifibrantResolutionObj CategoryTheory.ObjectProperty.FullSubcategory.obj HomotopicalAlgebra.BifibrantObject.instIsCofibrantObjBifibrantObjects homMk HomotopicalAlgebra.bifibrantObjects_le_cofibrantObject CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory bifibrantResolutionMap	—	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 HomotopicalAlgebra.BifibrantObject.instIsCofibrantObjBifibrantObjects HomotopicalAlgebra.bifibrantObjects_le_cofibrantObject CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' bifibrantResolutionMap_fac'
bifibrantResolutionMap_fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects CategoryTheory.Functor.obj HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.ιCofibrantObject bifibrantResolutionObj iBifibrantResolutionObj CategoryTheory.ObjectProperty.FullSubcategory.obj HomotopicalAlgebra.BifibrantObject.instIsCofibrantObjBifibrantObjects homMk HomotopicalAlgebra.bifibrantObjects_le_cofibrantObject CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory bifibrantResolutionMap	—	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 HomotopicalAlgebra.BifibrantObject.instIsCofibrantObjBifibrantObjects HomotopicalAlgebra.bifibrantObjects_le_cofibrantObject CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' bifibrantResolutionMap_fac
bifibrantResolutionObj_hom_ext 📖	—	CategoryTheory.CategoryStruct.comp HoCat CategoryTheory.Category.toCategoryStruct 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 HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.ιCofibrantObject bifibrantResolutionObj HomotopicalAlgebra.BifibrantObject.HoCat HomotopicalAlgebra.BifibrantObject.homRel HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject CategoryTheory.Functor.map iBifibrantResolutionObj HomotopicalAlgebra.BifibrantObject.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 HomotopicalAlgebra.BifibrantObject.toHoCat_obj_surjective CategoryTheory.Functor.map_surjective HomotopicalAlgebra.BifibrantObject.instFullHoCatToHoCat HomotopicalAlgebra.BifibrantObject.toHoCat_map_eq_iff HomotopicalAlgebra.BifibrantObject.homRel_iff_rightHomotopyRel HomotopicalAlgebra.RightHomotopyClass.mk_eq_mk_iff HomotopicalAlgebra.BifibrantObject.instIsFibrantObjBifibrantObjects HomotopicalAlgebra.RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalence instCofibrationHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj instWeakEquivalenceHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj HomotopicalAlgebra.BifibrantObject.instIsFibrantObjCofibrantObjectsObjCofibrantObjectιCofibrantObject homRel_iff_rightHomotopyRel toHoCat_map_eq_iff
exists_bifibrant 📖	mathematical	—	HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Quiver.Hom HomotopicalAlgebra.CofibrantObject CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects CategoryTheory.Functor.obj HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.ιCofibrantObject HomotopicalAlgebra.Cofibration ι CategoryTheory.Functor.map HomotopicalAlgebra.WeakEquivalence HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	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 HomotopicalAlgebra.ModelCategory.cm5a HomotopicalAlgebra.isCofibrant_of_cofibration CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition HomotopicalAlgebra.instIsMultiplicativeCofibrations HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemCofibrationsTrivialFibrations HomotopicalAlgebra.instCofibrationITrivialCofibrationsFibrations instIsCofibrantObjCofibrantObjects HomotopicalAlgebra.isFibrant_iff_of_isTerminal CategoryTheory.MorphismProperty.instRespectsIsoOfIsStableUnderRetracts HomotopicalAlgebra.ModelCategory.cm3b HomotopicalAlgebra.instFibrationPTrivialCofibrationsFibrations CategoryTheory.ObjectProperty.FullSubcategory.property HomotopicalAlgebra.bifibrantObjects_le_cofibrantObject
exists_bifibrant_map 📖	mathematical	—	Quiver.Hom HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects bifibrantResolutionObj CategoryTheory.CategoryStruct.comp HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.cofibrantObjects CategoryTheory.Functor.obj HomotopicalAlgebra.BifibrantObject.ιCofibrantObject iBifibrantResolutionObj CategoryTheory.Functor.map	—	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.Limits.terminal.comp_from exists_bifibrant HomotopicalAlgebra.BifibrantObject.instIsCofibrantObjBifibrantObjects HomotopicalAlgebra.BifibrantObject.instIsFibrantObjBifibrantObjects CategoryTheory.sq_hasLift_of_hasLiftingProperty HomotopicalAlgebra.ModelCategory.cm4a instCofibrationHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj instWeakEquivalenceHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj instIsFibrantObjιBifibrantObjectιCofibrantObject CategoryTheory.ObjectProperty.hom_ext HomotopicalAlgebra.bifibrantObjects_le_cofibrantObject CategoryTheory.CommSq.fac_left
instCofibrationHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj 📖	mathematical	—	HomotopicalAlgebra.Cofibration 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.Functor.obj HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.BifibrantObject.ιCofibrantObject bifibrantResolutionObj CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory iBifibrantResolutionObj	—	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 exists_bifibrant
instFaithfulHoCatHoCatιCofibrantObject 📖	mathematical	—	CategoryTheory.Functor.Faithful HomotopicalAlgebra.BifibrantObject.HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.homRel HoCat HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.cofibrantObjects homRel HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject	—	CategoryTheory.Functor.FullyFaithful.faithful instIsIsoFunctorHoCatCounitHoCatAdj
instFullHoCatHoCatιCofibrantObject 📖	mathematical	—	CategoryTheory.Functor.Full HomotopicalAlgebra.BifibrantObject.HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.homRel HoCat HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.cofibrantObjects homRel HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject	—	CategoryTheory.Functor.FullyFaithful.full instIsIsoFunctorHoCatCounitHoCatAdj
instIsFibrantObjιBifibrantObjectιCofibrantObject 📖	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.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects ι HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.ιCofibrantObject	—	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.ObjectProperty.FullSubcategory.property
instIsIsoFunctorHoCatAdjCounit' 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor HomotopicalAlgebra.BifibrantObject.HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.homRel CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp HoCat HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.cofibrantObjects homRel HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject HoCat.bifibrantResolution HoCat.adjCounit'	—	CategoryTheory.NatIso.isIso_of_isIso_app instIsIsoHoCatAppAdjCounit'
instIsIsoFunctorHoCatCounitHoCatAdj 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor HomotopicalAlgebra.BifibrantObject.HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.homRel CategoryTheory.Functor.category CategoryTheory.Functor.comp HoCat HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.cofibrantObjects homRel HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject HoCat.bifibrantResolution CategoryTheory.Functor.id CategoryTheory.Adjunction.counit HoCat.adj	—	CategoryTheory.Iso.isIso_hom
instIsIsoHoCatAppAdjCounit' 📖	mathematical	—	CategoryTheory.IsIso HomotopicalAlgebra.BifibrantObject.HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.homRel CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp HoCat HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.cofibrantObjects homRel HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject HoCat.bifibrantResolution CategoryTheory.NatTrans.app HoCat.adjCounit'	—	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 HomotopicalAlgebra.BifibrantObject.toHoCat_obj_surjective HomotopicalAlgebra.BifibrantObject.instIsCofibrantObjBifibrantObjects HomotopicalAlgebra.BifibrantObject.instIsFibrantObjBifibrantObjects instIsCofibrantObjCofibrantObjects HomotopicalAlgebra.BifibrantObject.instIsFibrantObjCofibrantObjectsObjCofibrantObjectιCofibrantObject HoCat.adjCounit'_app instWeakEquivalenceHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj HomotopicalAlgebra.BifibrantObject.instIsIsoHoCatMapToHoCatOfWeakEquivalence
instIsLocalizationHoCatHoCatBifibrantResolutionWeakEquivalences 📖	mathematical	—	CategoryTheory.Functor.IsLocalization HoCat HomotopicalAlgebra.BifibrantObject.HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects homRel HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.homRel HoCat.bifibrantResolution HomotopicalAlgebra.weakEquivalences instCategoryWithWeakEquivalencesHoCat	—	CategoryTheory.Adjunction.isLocalization_leftAdjoint instFullHoCatHoCatιCofibrantObject instFaithfulHoCatHoCatιCofibrantObject CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype toHoCat_obj_surjective CategoryTheory.Functor.map_surjective instFullHoCatToHoCat CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HoCat.bifibrantResolution_map CategoryTheory.Localization.inverts HomotopicalAlgebra.BifibrantObject.instIsLocalizationHoCatToHoCatWeakEquivalences HomotopicalAlgebra.weakEquivalence_iff instWeakEquivalenceBifibrantObjectBifibrantResolutionMap weakEquivalence_toHoCat_map_iff instWeakEquivalenceHoCatAppUnitHoCatAdj
instWeakEquivalenceBifibrantObjectBifibrantResolutionMap 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects bifibrantResolutionObj bifibrantResolutionMap HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	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 HomotopicalAlgebra.weakEquivalence_iff HomotopicalAlgebra.BifibrantObject.instIsCofibrantObjBifibrantObjects HomotopicalAlgebra.weakEquivalence_precomp_iff HomotopicalAlgebra.instHasTwoOutOfThreePropertyFullSubcategoryWeakEquivalences HomotopicalAlgebra.ModelCategory.cm2 instWeakEquivalenceIBifibrantResolutionObj HomotopicalAlgebra.bifibrantObjects_le_cofibrantObject bifibrantResolutionMap_fac
instWeakEquivalenceHoCatAppAdjUnit 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects homRel CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp HomotopicalAlgebra.BifibrantObject.HoCat HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.homRel HoCat.bifibrantResolution HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject CategoryTheory.NatTrans.app HoCat.adjUnit instCategoryWithWeakEquivalencesHoCat	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype toHoCat_obj_surjective CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HoCat.adjUnit_app weakEquivalence_toHoCat_map_iff HomotopicalAlgebra.weakEquivalence_iff_of_objectProperty instWeakEquivalenceHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj
instWeakEquivalenceHoCatAppUnitHoCatAdj 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects homRel CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp HomotopicalAlgebra.BifibrantObject.HoCat HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.homRel HoCat.bifibrantResolution HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit HoCat.adj instCategoryWithWeakEquivalencesHoCat	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype toHoCat_obj_surjective CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a instWeakEquivalenceHoCatAppAdjUnit
instWeakEquivalenceHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence 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.Functor.obj HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.BifibrantObject.ιCofibrantObject bifibrantResolutionObj CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory iBifibrantResolutionObj HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	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 exists_bifibrant
instWeakEquivalenceIBifibrantResolutionObj 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence 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.obj HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.ιCofibrantObject bifibrantResolutionObj iBifibrantResolutionObj HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences	—	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 HomotopicalAlgebra.weakEquivalence_iff_of_objectProperty instWeakEquivalenceHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj

HomotopicalAlgebra.CofibrantObject.HoCat

Definitions

Name	Category	Theorems
adj 📖	CompOp	2 math math: HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorHoCatCounitHoCatAdj, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppUnitHoCatAdj
adjCounit' 📖	CompOp	3 math math: HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorHoCatAdjCounit', HomotopicalAlgebra.CofibrantObject.instIsIsoHoCatAppAdjCounit', adjCounit'_app
adjCounitIso 📖	CompOp	1 math math: adjCounitIso_inv_app
adjUnit 📖	CompOp	2 math math: adjUnit_app, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppAdjUnit
bifibrantResolution 📖	CompOp	11 math math: HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorHoCatAdjCounit', HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorHoCatCounitHoCatAdj, bifibrantResolution_map, adjCounitIso_inv_app, adjUnit_app, bifibrantResolution_obj, HomotopicalAlgebra.CofibrantObject.instIsIsoHoCatAppAdjCounit', HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppAdjUnit, HomotopicalAlgebra.CofibrantObject.instIsLocalizationHoCatHoCatBifibrantResolutionWeakEquivalences, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppUnitHoCatAdj, adjCounit'_app
bifibrantResolution' 📖	CompOp	2 math math: bifibrantResolution'_obj, bifibrantResolution'_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjCounit'_app 📖	mathematical	—	CategoryTheory.NatTrans.app HomotopicalAlgebra.BifibrantObject.HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.homRel CategoryTheory.Functor.id CategoryTheory.Functor.comp HomotopicalAlgebra.CofibrantObject.HoCat HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.cofibrantObjects HomotopicalAlgebra.CofibrantObject.homRel HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject bifibrantResolution adjCounit' CategoryTheory.Functor.obj CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.BifibrantObject.toHoCat CategoryTheory.Functor.map CategoryTheory.ObjectProperty.FullSubcategory.obj HomotopicalAlgebra.BifibrantObject.instIsCofibrantObjBifibrantObjects HomotopicalAlgebra.BifibrantObject.instIsFibrantObjBifibrantObjects HomotopicalAlgebra.BifibrantObject.ιCofibrantObject HomotopicalAlgebra.CofibrantObject.bifibrantResolutionObj HomotopicalAlgebra.CofibrantObject.instIsCofibrantObjCofibrantObjects HomotopicalAlgebra.BifibrantObject.instIsFibrantObjCofibrantObjectsObjCofibrantObjectιCofibrantObject HomotopicalAlgebra.BifibrantObject.homMk CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory HomotopicalAlgebra.CofibrantObject.iBifibrantResolutionObj	—	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
adjCounitIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app HomotopicalAlgebra.BifibrantObject.HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.homRel CategoryTheory.Functor.id CategoryTheory.Functor.comp HomotopicalAlgebra.CofibrantObject.HoCat HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.cofibrantObjects HomotopicalAlgebra.CofibrantObject.homRel HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject bifibrantResolution CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category adjCounitIso CategoryTheory.Functor.obj CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.BifibrantObject.toHoCat CategoryTheory.Functor.map CategoryTheory.ObjectProperty.FullSubcategory.obj HomotopicalAlgebra.BifibrantObject.instIsCofibrantObjBifibrantObjects HomotopicalAlgebra.BifibrantObject.instIsFibrantObjBifibrantObjects HomotopicalAlgebra.BifibrantObject.ιCofibrantObject HomotopicalAlgebra.CofibrantObject.bifibrantResolutionObj HomotopicalAlgebra.CofibrantObject.instIsCofibrantObjCofibrantObjects HomotopicalAlgebra.BifibrantObject.instIsFibrantObjCofibrantObjectsObjCofibrantObjectιCofibrantObject HomotopicalAlgebra.BifibrantObject.homMk CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory HomotopicalAlgebra.CofibrantObject.iBifibrantResolutionObj	—	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
adjUnit_app 📖	mathematical	—	CategoryTheory.NatTrans.app HomotopicalAlgebra.CofibrantObject.HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects HomotopicalAlgebra.CofibrantObject.homRel CategoryTheory.Functor.id CategoryTheory.Functor.comp HomotopicalAlgebra.BifibrantObject.HoCat HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.homRel bifibrantResolution HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject adjUnit CategoryTheory.Functor.obj CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HomotopicalAlgebra.CofibrantObject.toHoCat CategoryTheory.Functor.map CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.BifibrantObject.ιCofibrantObject HomotopicalAlgebra.CofibrantObject.bifibrantResolutionObj HomotopicalAlgebra.CofibrantObject.iBifibrantResolutionObj	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype
bifibrantResolution'_map 📖	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 HomotopicalAlgebra.BifibrantObject.HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.homRel bifibrantResolution' HomotopicalAlgebra.BifibrantObject.toHoCat HomotopicalAlgebra.CofibrantObject.bifibrantResolutionObj HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype
bifibrantResolution'_obj 📖	mathematical	—	CategoryTheory.Functor.obj 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.BifibrantObject.HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.homRel bifibrantResolution' HomotopicalAlgebra.BifibrantObject.toHoCat HomotopicalAlgebra.CofibrantObject.bifibrantResolutionObj	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype
bifibrantResolution_map 📖	mathematical	—	CategoryTheory.Functor.map HomotopicalAlgebra.CofibrantObject.HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects HomotopicalAlgebra.CofibrantObject.homRel HomotopicalAlgebra.BifibrantObject.HoCat HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.homRel bifibrantResolution CategoryTheory.Functor.obj CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HomotopicalAlgebra.CofibrantObject.toHoCat CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.BifibrantObject.toHoCat HomotopicalAlgebra.CofibrantObject.bifibrantResolutionObj HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype
bifibrantResolution_obj 📖	mathematical	—	CategoryTheory.Functor.obj HomotopicalAlgebra.CofibrantObject.HoCat CategoryTheory.Quotient.category HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects HomotopicalAlgebra.CofibrantObject.homRel HomotopicalAlgebra.BifibrantObject.HoCat HomotopicalAlgebra.BifibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.BifibrantObject.homRel bifibrantResolution CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty HomotopicalAlgebra.CofibrantObject.toHoCat CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a HomotopicalAlgebra.BifibrantObject.toHoCat HomotopicalAlgebra.CofibrantObject.bifibrantResolutionObj	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype

---

← Back to Index