Bifibrant

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

Statistics

Metric	Count
Definitions BifibrantObject, homMk, mk, ι, ιCofibrantObject, ιFibrantObject, CofibrantObject, homMk, mk, ι, FibrantObject, homMk, mk, ι, bifibrantObjects, cofibrantObjects, fibrantObjects	17
Theorems homMk_homMk, homMk_homMk_assoc, homMk_id, homMk_surjective, instIsCofibrantObjBifibrantObjects, instIsCofibrantObjFibrantObjectsObjFibrantObjectιFibrantObject, instIsCofibrantObjι, instIsFibrantObjBifibrantObjects, instIsFibrantObjCofibrantObjectsObjCofibrantObjectιCofibrantObject, instIsFibrantObjι, mk_surjective, weakEquivalence_homMk_iff, homMk_homMk, homMk_homMk_assoc, homMk_id, homMk_surjective, instIsCofibrantObjCofibrantObjects, instIsCofibrantObjι, mk_surjective, weakEquivalence_homMk_iff, homMk_homMk, homMk_homMk_assoc, homMk_id, homMk_surjective, instIsFibrantObjFibrantObjects, instIsFibrantObjι, mk_surjective, weakEquivalence_homMk_iff, bifibrantObjects_le_cofibrantObject, bifibrantObjects_le_fibrantObject	30
Total	47

HomotopicalAlgebra

Definitions

Name	Category	Theorems
BifibrantObject 📖	CompOp	52 math math: BifibrantObject.weakEquivalence_homMk_iff, BifibrantObject.inverts_iff_factors, BifibrantObject.HoCat.ιCofibrantObject_obj, CofibrantObject.instWeakEquivalenceBifibrantObjectBifibrantResolutionMap, BifibrantObject.homMk_id, BifibrantObject.HoCat.homEquivRight_apply, CofibrantObject.instFaithfulHoCatHoCatιCofibrantObject, BifibrantObject.HoCat.homEquivLeft_symm_apply, CofibrantObject.bifibrantResolutionMap_fac', BifibrantObject.HoCat.homEquivLeft_apply, BifibrantObject.toHoCat_map_eq, BifibrantObject.instIsIsoHoCatMapToHoCatOfWeakEquivalence, BifibrantObject.instCongruenceHomRel, CofibrantObject.instIsFibrantObjιBifibrantObjectιCofibrantObject, CofibrantObject.HoCat.bifibrantResolution'_obj, BifibrantObject.instIsLocalizationHoCatToHoCatWeakEquivalences, BifibrantObject.instIsCofibrantObjFibrantObjectsObjFibrantObjectιFibrantObject, CofibrantObject.bifibrantResolutionMap_fac, CofibrantObject.exists_bifibrant_map, BifibrantObject.toHoCat_obj_surjective, BifibrantObject.HoCat.homEquivRight_symm_apply, CofibrantObject.instIsIsoFunctorHoCatAdjCounit', CofibrantObject.instIsIsoFunctorHoCatCounitHoCatAdj, BifibrantObject.instIsStableUnderPostcompHomRel, BifibrantObject.HoCat.ιFibrantObject_obj, CofibrantObject.HoCat.bifibrantResolution_map, CofibrantObject.bifibrantResolutionMap_fac_assoc, CofibrantObject.HoCat.adjCounitIso_inv_app, CofibrantObject.HoCat.adjUnit_app, CofibrantObject.instWeakEquivalenceIBifibrantResolutionObj, BifibrantObject.homMk_homMk, BifibrantObject.instIsFibrantObjCofibrantObjectsObjCofibrantObjectιCofibrantObject, CofibrantObject.HoCat.bifibrantResolution_obj, BifibrantObject.toHoCat_map_eq_iff, CofibrantObject.instIsIsoHoCatAppAdjCounit', BifibrantObject.instIsStableUnderPrecompHomRel, BifibrantObject.homMk_homMk_assoc, CofibrantObject.instWeakEquivalenceHoCatAppAdjUnit, CofibrantObject.instFullHoCatHoCatιCofibrantObject, CofibrantObject.instIsLocalizationHoCatHoCatBifibrantResolutionWeakEquivalences, CofibrantObject.exists_bifibrant, CofibrantObject.HoCat.bifibrantResolution'_map, CofibrantObject.instWeakEquivalenceHoCatAppUnitHoCatAdj, BifibrantObject.instIsCofibrantObjι, BifibrantObject.HoCat.ιCofibrantObject_map_toHoCat_map, CofibrantObject.instWeakEquivalenceHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, CofibrantObject.HoCat.adjCounit'_app, BifibrantObject.instFullHoCatToHoCat, CofibrantObject.instCofibrationHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, CofibrantObject.bifibrantResolutionMap_fac'_assoc, BifibrantObject.HoCat.ιFibrantObject_map_toHoCat_map, BifibrantObject.instIsFibrantObjι
CofibrantObject 📖	CompOp	59 math math: BifibrantObject.HoCat.ιCofibrantObject_obj, CofibrantObject.homRel_equivalence_of_isFibrant_tgt, CofibrantObject.instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism, CofibrantObject.toHoCat_map_eq_iff, CofibrantObject.instFaithfulHoCatHoCatιCofibrantObject, CofibrantObject.homMk_homMk, CofibrantObject.bifibrantResolutionMap_fac', CofibrantObject.instHasLeftResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism, CofibrantObject.instIsFibrantObjιBifibrantObjectιCofibrantObject, CofibrantObject.toHoCat_obj_surjective, CofibrantObject.HoCat.bifibrantResolution'_obj, CofibrantObject.instIsCofibrantObjι, CofibrantObject.instIsCofibrantObjFunctorWeakEquivalencesLocalizerMorphism, CofibrantObject.bifibrantResolutionMap_fac, CofibrantObject.exists_bifibrant_map, CofibrantObject.instFullHoCatToHoCat, CofibrantObject.instIsConnectedLeftResolutionWeakEquivalencesLocalizerMorphism, CofibrantObject.instIsLocalizationCompHoCatToHoCatWeakEquivalences, CofibrantObject.instIsLeftDerivabilityStructureWeakEquivalencesLocalizerMorphism, CofibrantObject.instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences, CofibrantObject.HoCat.resolutionObj_hom_ext, CofibrantObject.instIsIsoFunctorHoCatAdjCounit', CofibrantObject.instIsIsoFunctorHoCatCounitHoCatAdj, CofibrantObject.instIsIsoFunctorResolutionCompToLocalizationNatTrans, CofibrantObject.HoCat.bifibrantResolution_map, CofibrantObject.bifibrantResolutionMap_fac_assoc, CofibrantObject.HoCat.adjCounitIso_inv_app, CofibrantObject.HoCat.adjUnit_app, CofibrantObject.instWeakEquivalenceIBifibrantResolutionObj, BifibrantObject.instIsFibrantObjCofibrantObjectsObjCofibrantObjectιCofibrantObject, CofibrantObject.HoCat.bifibrantResolution_obj, CofibrantObject.instWeakEquivalenceWWeakEquivalences, CofibrantObject.localizerMorphism_functor, CofibrantObject.instIsStableUnderPrecompHomRel, CofibrantObject.instIsIsoHoCatAppAdjCounit', CofibrantObject.factorsThroughLocalization, CofibrantObject.homMk_homMk_assoc, CofibrantObject.instWeakEquivalenceHoCatAppιCompResolutionNatTrans, CofibrantObject.instWeakEquivalenceHoCatAppAdjUnit, CofibrantObject.instFullHoCatHoCatιCofibrantObject, CofibrantObject.instIsLocalizationHoCatHoCatBifibrantResolutionWeakEquivalences, CofibrantObject.instHasQuotientWeakEquivalencesHomRel, CofibrantObject.HoCat.ιCompResolutionNatTrans_app, CofibrantObject.instIsLocalizationCompιWeakEquivalences, CofibrantObject.exists_bifibrant, CofibrantObject.HoCat.bifibrantResolution'_map, CofibrantObject.instWeakEquivalenceHoCatAppUnitHoCatAdj, CofibrantObject.weakEquivalence_toHoCat_map_iff, CofibrantObject.HoCat.localizerMorphismResolution_functor, BifibrantObject.HoCat.ιCofibrantObject_map_toHoCat_map, CofibrantObject.instWeakEquivalenceHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, CofibrantObject.homMk_id, CofibrantObject.HoCat.adjCounit'_app, CofibrantObject.instIsStableUnderPostcompHomRel, CofibrantObject.weakEquivalence_homMk_iff, CofibrantObject.instCofibrationHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, CofibrantObject.bifibrantResolutionMap_fac'_assoc, CofibrantObject.instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism, CofibrantObject.toHoCat_map_eq
FibrantObject 📖	CompOp	34 math math: FibrantObject.instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences, FibrantObject.homMk_homMk, FibrantObject.instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism, FibrantObject.instIsLocalizationCompHoCatToHoCatWeakEquivalences, FibrantObject.toHoCat_map_eq_iff, FibrantObject.weakEquivalence_toHoCat_map_iff, FibrantObject.instHasRightResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism, FibrantObject.instWeakEquivalenceHoCatAppιCompResolutionNatTrans, FibrantObject.localizerMorphism_functor, FibrantObject.instFullHoCatToHoCat, FibrantObject.instIsLocalizationCompιWeakEquivalences, BifibrantObject.instIsCofibrantObjFibrantObjectsObjFibrantObjectιFibrantObject, FibrantObject.toHoCat_map_eq, FibrantObject.instIsConnectedRightResolutionWeakEquivalencesLocalizerMorphism, FibrantObject.HoCat.resolutionObj_hom_ext, FibrantObject.instIsFibrantObjι, FibrantObject.instIsStableUnderPrecompHomRel, FibrantObject.weakEquivalence_homMk_iff, BifibrantObject.HoCat.ιFibrantObject_obj, FibrantObject.homRel_equivalence_of_isCofibrant_src, FibrantObject.homMk_homMk_assoc, FibrantObject.instHasQuotientWeakEquivalencesHomRel, FibrantObject.instWeakEquivalenceWWeakEquivalences, FibrantObject.HoCat.ιCompResolutionNatTrans_app, FibrantObject.toHoCat_obj_surjective, FibrantObject.instIsIsoFunctorResolutionCompToLocalizationNatTrans, FibrantObject.homMk_id, FibrantObject.instIsFibrantObjFunctorWeakEquivalencesLocalizerMorphism, FibrantObject.factorsThroughLocalization, FibrantObject.HoCat.localizerMorphismResolution_functor, FibrantObject.instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism, FibrantObject.instIsRightDerivabilityStructureWeakEquivalencesLocalizerMorphism, FibrantObject.instIsStableUnderPostcompHomRel, BifibrantObject.HoCat.ιFibrantObject_map_toHoCat_map
bifibrantObjects 📖	CompOp	58 math math: BifibrantObject.weakEquivalence_homMk_iff, BifibrantObject.inverts_iff_factors, BifibrantObject.HoCat.ιCofibrantObject_obj, BifibrantObject.instIsFibrantObjBifibrantObjects, CofibrantObject.instWeakEquivalenceBifibrantObjectBifibrantResolutionMap, BifibrantObject.homMk_id, BifibrantObject.HoCat.homEquivRight_apply, CofibrantObject.instFaithfulHoCatHoCatιCofibrantObject, BifibrantObject.HoCat.homEquivLeft_symm_apply, CofibrantObject.bifibrantResolutionMap_fac', BifibrantObject.HoCat.homEquivLeft_apply, BifibrantObject.toHoCat_map_eq, BifibrantObject.instIsIsoHoCatMapToHoCatOfWeakEquivalence, BifibrantObject.instCongruenceHomRel, CofibrantObject.instIsFibrantObjιBifibrantObjectιCofibrantObject, CofibrantObject.HoCat.bifibrantResolution'_obj, BifibrantObject.instIsLocalizationHoCatToHoCatWeakEquivalences, BifibrantObject.instIsCofibrantObjFibrantObjectsObjFibrantObjectιFibrantObject, CofibrantObject.bifibrantResolutionMap_fac, CofibrantObject.exists_bifibrant_map, BifibrantObject.toHoCat_obj_surjective, BifibrantObject.HoCat.homEquivRight_symm_apply, CofibrantObject.instIsIsoFunctorHoCatAdjCounit', CofibrantObject.instIsIsoFunctorHoCatCounitHoCatAdj, BifibrantObject.instIsStableUnderPostcompHomRel, BifibrantObject.HoCat.ιFibrantObject_obj, CofibrantObject.HoCat.bifibrantResolution_map, CofibrantObject.bifibrantResolutionMap_fac_assoc, BifibrantObject.homRel_iff_leftHomotopyRel, CofibrantObject.HoCat.adjCounitIso_inv_app, CofibrantObject.HoCat.adjUnit_app, CofibrantObject.instWeakEquivalenceIBifibrantResolutionObj, BifibrantObject.homMk_homMk, BifibrantObject.instIsFibrantObjCofibrantObjectsObjCofibrantObjectιCofibrantObject, CofibrantObject.HoCat.bifibrantResolution_obj, BifibrantObject.toHoCat_map_eq_iff, CofibrantObject.instIsIsoHoCatAppAdjCounit', BifibrantObject.instIsStableUnderPrecompHomRel, BifibrantObject.homMk_homMk_assoc, CofibrantObject.instWeakEquivalenceHoCatAppAdjUnit, CofibrantObject.instFullHoCatHoCatιCofibrantObject, bifibrantObjects_le_fibrantObject, BifibrantObject.instIsCofibrantObjBifibrantObjects, CofibrantObject.instIsLocalizationHoCatHoCatBifibrantResolutionWeakEquivalences, CofibrantObject.exists_bifibrant, CofibrantObject.HoCat.bifibrantResolution'_map, CofibrantObject.instWeakEquivalenceHoCatAppUnitHoCatAdj, BifibrantObject.instIsCofibrantObjι, bifibrantObjects_le_cofibrantObject, BifibrantObject.HoCat.ιCofibrantObject_map_toHoCat_map, BifibrantObject.homRel_iff_rightHomotopyRel, CofibrantObject.instWeakEquivalenceHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, CofibrantObject.HoCat.adjCounit'_app, BifibrantObject.instFullHoCatToHoCat, CofibrantObject.instCofibrationHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, CofibrantObject.bifibrantResolutionMap_fac'_assoc, BifibrantObject.HoCat.ιFibrantObject_map_toHoCat_map, BifibrantObject.instIsFibrantObjι
cofibrantObjects 📖	CompOp	62 math math: BifibrantObject.HoCat.ιCofibrantObject_obj, CofibrantObject.homRel_equivalence_of_isFibrant_tgt, CofibrantObject.instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism, CofibrantObject.toHoCat_map_eq_iff, CofibrantObject.instFaithfulHoCatHoCatιCofibrantObject, CofibrantObject.homMk_homMk, CofibrantObject.bifibrantResolutionMap_fac', CofibrantObject.instHasLeftResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism, CofibrantObject.instIsFibrantObjιBifibrantObjectιCofibrantObject, CofibrantObject.toHoCat_obj_surjective, CofibrantObject.HoCat.bifibrantResolution'_obj, CofibrantObject.instIsCofibrantObjι, CofibrantObject.instIsCofibrantObjFunctorWeakEquivalencesLocalizerMorphism, CofibrantObject.bifibrantResolutionMap_fac, CofibrantObject.exists_bifibrant_map, CofibrantObject.instFullHoCatToHoCat, CofibrantObject.instIsConnectedLeftResolutionWeakEquivalencesLocalizerMorphism, CofibrantObject.instIsLocalizationCompHoCatToHoCatWeakEquivalences, CofibrantObject.instIsLeftDerivabilityStructureWeakEquivalencesLocalizerMorphism, CofibrantObject.instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences, CofibrantObject.HoCat.resolutionObj_hom_ext, CofibrantObject.instIsIsoFunctorHoCatAdjCounit', CofibrantObject.instIsIsoFunctorHoCatCounitHoCatAdj, CofibrantObject.instIsIsoFunctorResolutionCompToLocalizationNatTrans, CofibrantObject.HoCat.bifibrantResolution_map, CofibrantObject.bifibrantResolutionMap_fac_assoc, CofibrantObject.HoCat.adjCounitIso_inv_app, CofibrantObject.HoCat.adjUnit_app, CofibrantObject.instWeakEquivalenceIBifibrantResolutionObj, BifibrantObject.instIsFibrantObjCofibrantObjectsObjCofibrantObjectιCofibrantObject, CofibrantObject.HoCat.bifibrantResolution_obj, CofibrantObject.instWeakEquivalenceWWeakEquivalences, CofibrantObject.localizerMorphism_functor, CofibrantObject.instIsStableUnderPrecompHomRel, CofibrantObject.instIsIsoHoCatAppAdjCounit', CofibrantObject.factorsThroughLocalization, CofibrantObject.homMk_homMk_assoc, CofibrantObject.instWeakEquivalenceHoCatAppιCompResolutionNatTrans, CofibrantObject.instWeakEquivalenceHoCatAppAdjUnit, CofibrantObject.instFullHoCatHoCatιCofibrantObject, CofibrantObject.instIsLocalizationHoCatHoCatBifibrantResolutionWeakEquivalences, CofibrantObject.instHasQuotientWeakEquivalencesHomRel, CofibrantObject.HoCat.ιCompResolutionNatTrans_app, CofibrantObject.instIsLocalizationCompιWeakEquivalences, CofibrantObject.exists_bifibrant, CofibrantObject.HoCat.bifibrantResolution'_map, CofibrantObject.instWeakEquivalenceHoCatAppUnitHoCatAdj, CofibrantObject.weakEquivalence_toHoCat_map_iff, bifibrantObjects_le_cofibrantObject, CofibrantObject.HoCat.localizerMorphismResolution_functor, BifibrantObject.HoCat.ιCofibrantObject_map_toHoCat_map, CofibrantObject.instWeakEquivalenceHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, CofibrantObject.instIsCofibrantObjCofibrantObjects, CofibrantObject.homMk_id, CofibrantObject.HoCat.adjCounit'_app, CofibrantObject.instIsStableUnderPostcompHomRel, CofibrantObject.weakEquivalence_homMk_iff, CofibrantObject.instCofibrationHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, CofibrantObject.homRel_iff_rightHomotopyRel, CofibrantObject.bifibrantResolutionMap_fac'_assoc, CofibrantObject.instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism, CofibrantObject.toHoCat_map_eq
fibrantObjects 📖	CompOp	37 math math: FibrantObject.instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences, FibrantObject.homMk_homMk, FibrantObject.instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism, FibrantObject.instIsLocalizationCompHoCatToHoCatWeakEquivalences, FibrantObject.toHoCat_map_eq_iff, FibrantObject.weakEquivalence_toHoCat_map_iff, FibrantObject.homRel_iff_leftHomotopyRel, FibrantObject.instHasRightResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism, FibrantObject.instWeakEquivalenceHoCatAppιCompResolutionNatTrans, FibrantObject.localizerMorphism_functor, FibrantObject.instFullHoCatToHoCat, FibrantObject.instIsLocalizationCompιWeakEquivalences, BifibrantObject.instIsCofibrantObjFibrantObjectsObjFibrantObjectιFibrantObject, FibrantObject.toHoCat_map_eq, FibrantObject.instIsConnectedRightResolutionWeakEquivalencesLocalizerMorphism, FibrantObject.HoCat.resolutionObj_hom_ext, FibrantObject.instIsFibrantObjι, FibrantObject.instIsStableUnderPrecompHomRel, FibrantObject.weakEquivalence_homMk_iff, BifibrantObject.HoCat.ιFibrantObject_obj, FibrantObject.homRel_equivalence_of_isCofibrant_src, FibrantObject.homMk_homMk_assoc, FibrantObject.instHasQuotientWeakEquivalencesHomRel, FibrantObject.instWeakEquivalenceWWeakEquivalences, FibrantObject.HoCat.ιCompResolutionNatTrans_app, FibrantObject.toHoCat_obj_surjective, FibrantObject.instIsFibrantObjFibrantObjects, FibrantObject.instIsIsoFunctorResolutionCompToLocalizationNatTrans, bifibrantObjects_le_fibrantObject, FibrantObject.homMk_id, FibrantObject.instIsFibrantObjFunctorWeakEquivalencesLocalizerMorphism, FibrantObject.factorsThroughLocalization, FibrantObject.HoCat.localizerMorphismResolution_functor, FibrantObject.instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism, FibrantObject.instIsRightDerivabilityStructureWeakEquivalencesLocalizerMorphism, FibrantObject.instIsStableUnderPostcompHomRel, BifibrantObject.HoCat.ιFibrantObject_map_toHoCat_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bifibrantObjects_le_cofibrantObject 📖	mathematical	—	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le bifibrantObjects cofibrantObjects	—	—
bifibrantObjects_le_fibrantObject 📖	mathematical	—	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le bifibrantObjects fibrantObjects	—	—

HomotopicalAlgebra.BifibrantObject

Definitions

Name	Category	Theorems
homMk 📖	CompOp	11 math math: weakEquivalence_homMk_iff, homMk_id, HoCat.homEquivRight_apply, HoCat.homEquivLeft_symm_apply, HoCat.homEquivLeft_apply, HoCat.homEquivRight_symm_apply, homMk_surjective, HomotopicalAlgebra.CofibrantObject.HoCat.adjCounitIso_inv_app, homMk_homMk, homMk_homMk_assoc, HomotopicalAlgebra.CofibrantObject.HoCat.adjCounit'_app
mk 📖	CompOp	—
ι 📖	CompOp	2 math math: instIsCofibrantObjι, instIsFibrantObjι
ιCofibrantObject 📖	CompOp	15 math math: HoCat.ιCofibrantObject_obj, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac', HomotopicalAlgebra.CofibrantObject.instIsFibrantObjιBifibrantObjectιCofibrantObject, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac, HomotopicalAlgebra.CofibrantObject.exists_bifibrant_map, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac_assoc, HomotopicalAlgebra.CofibrantObject.HoCat.adjCounitIso_inv_app, HomotopicalAlgebra.CofibrantObject.HoCat.adjUnit_app, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceIBifibrantResolutionObj, instIsFibrantObjCofibrantObjectsObjCofibrantObjectιCofibrantObject, HomotopicalAlgebra.CofibrantObject.exists_bifibrant, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, HomotopicalAlgebra.CofibrantObject.HoCat.adjCounit'_app, HomotopicalAlgebra.CofibrantObject.instCofibrationHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac'_assoc
ιFibrantObject 📖	CompOp	2 math math: instIsCofibrantObjFibrantObjectsObjFibrantObjectιFibrantObject, HoCat.ιFibrantObject_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homMk_homMk 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomotopicalAlgebra.BifibrantObject CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects homMk	—	—
homMk_homMk_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomotopicalAlgebra.BifibrantObject CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects homMk	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homMk_homMk
homMk_id 📖	mathematical	—	homMk CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct HomotopicalAlgebra.BifibrantObject CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects	—	—
homMk_surjective 📖	mathematical	—	homMk	—	—
instIsCofibrantObjBifibrantObjects 📖	mathematical	—	HomotopicalAlgebra.IsCofibrant CategoryTheory.ObjectProperty.FullSubcategory.obj HomotopicalAlgebra.bifibrantObjects	—	CategoryTheory.ObjectProperty.FullSubcategory.property
instIsCofibrantObjFibrantObjectsObjFibrantObjectιFibrantObject 📖	mathematical	—	HomotopicalAlgebra.IsCofibrant CategoryTheory.ObjectProperty.FullSubcategory.obj HomotopicalAlgebra.fibrantObjects CategoryTheory.Functor.obj HomotopicalAlgebra.BifibrantObject CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.FibrantObject ιFibrantObject	—	CategoryTheory.ObjectProperty.FullSubcategory.property
instIsCofibrantObjι 📖	mathematical	—	HomotopicalAlgebra.IsCofibrant CategoryTheory.Functor.obj HomotopicalAlgebra.BifibrantObject CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects ι	—	CategoryTheory.ObjectProperty.FullSubcategory.property
instIsFibrantObjBifibrantObjects 📖	mathematical	—	HomotopicalAlgebra.IsFibrant CategoryTheory.ObjectProperty.FullSubcategory.obj HomotopicalAlgebra.bifibrantObjects	—	CategoryTheory.ObjectProperty.FullSubcategory.property
instIsFibrantObjCofibrantObjectsObjCofibrantObjectιCofibrantObject 📖	mathematical	—	HomotopicalAlgebra.IsFibrant CategoryTheory.ObjectProperty.FullSubcategory.obj HomotopicalAlgebra.cofibrantObjects CategoryTheory.Functor.obj HomotopicalAlgebra.BifibrantObject CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects HomotopicalAlgebra.CofibrantObject ιCofibrantObject	—	CategoryTheory.ObjectProperty.FullSubcategory.property
instIsFibrantObjι 📖	mathematical	—	HomotopicalAlgebra.IsFibrant CategoryTheory.Functor.obj HomotopicalAlgebra.BifibrantObject CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects ι	—	CategoryTheory.ObjectProperty.FullSubcategory.property
mk_surjective 📖	—	—	—	—	CategoryTheory.ObjectProperty.FullSubcategory.property
weakEquivalence_homMk_iff 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence HomotopicalAlgebra.BifibrantObject CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.bifibrantObjects homMk HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory	—	—

HomotopicalAlgebra.CofibrantObject

Definitions

Name	Category	Theorems
homMk 📖	CompOp	11 math math: homMk_homMk, bifibrantResolutionMap_fac', bifibrantResolutionMap_fac, HoCat.resolutionObj_hom_ext, homMk_surjective, bifibrantResolutionMap_fac_assoc, homMk_homMk_assoc, HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject_map_toHoCat_map, homMk_id, weakEquivalence_homMk_iff, bifibrantResolutionMap_fac'_assoc
mk 📖	CompOp	—
ι 📖	CompOp	8 math math: instIsFibrantObjιBifibrantObjectιCofibrantObject, instIsCofibrantObjι, instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences, localizerMorphism_functor, instWeakEquivalenceHoCatAppιCompResolutionNatTrans, HoCat.ιCompResolutionNatTrans_app, instIsLocalizationCompιWeakEquivalences, exists_bifibrant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homMk_homMk 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomotopicalAlgebra.CofibrantObject CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects homMk	—	—
homMk_homMk_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomotopicalAlgebra.CofibrantObject CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects homMk	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homMk_homMk
homMk_id 📖	mathematical	—	homMk CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct HomotopicalAlgebra.CofibrantObject CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects	—	—
homMk_surjective 📖	mathematical	—	homMk	—	—
instIsCofibrantObjCofibrantObjects 📖	mathematical	—	HomotopicalAlgebra.IsCofibrant CategoryTheory.ObjectProperty.FullSubcategory.obj HomotopicalAlgebra.cofibrantObjects	—	CategoryTheory.ObjectProperty.FullSubcategory.property
instIsCofibrantObjι 📖	mathematical	—	HomotopicalAlgebra.IsCofibrant CategoryTheory.Functor.obj HomotopicalAlgebra.CofibrantObject CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects ι	—	CategoryTheory.ObjectProperty.FullSubcategory.property
mk_surjective 📖	—	—	—	—	CategoryTheory.ObjectProperty.FullSubcategory.property
weakEquivalence_homMk_iff 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence HomotopicalAlgebra.CofibrantObject CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects homMk HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory	—	—

HomotopicalAlgebra.FibrantObject

Definitions

Name	Category	Theorems
homMk 📖	CompOp	7 math math: homMk_homMk, HoCat.resolutionObj_hom_ext, weakEquivalence_homMk_iff, homMk_homMk_assoc, homMk_surjective, homMk_id, HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject_map_toHoCat_map
mk 📖	CompOp	—
ι 📖	CompOp	6 math math: instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences, instWeakEquivalenceHoCatAppιCompResolutionNatTrans, localizerMorphism_functor, instIsLocalizationCompιWeakEquivalences, instIsFibrantObjι, HoCat.ιCompResolutionNatTrans_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homMk_homMk 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomotopicalAlgebra.FibrantObject CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects homMk	—	—
homMk_homMk_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomotopicalAlgebra.FibrantObject CategoryTheory.Category.toCategoryStruct CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects homMk	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homMk_homMk
homMk_id 📖	mathematical	—	homMk CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct HomotopicalAlgebra.FibrantObject CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects	—	—
homMk_surjective 📖	mathematical	—	homMk	—	—
instIsFibrantObjFibrantObjects 📖	mathematical	—	HomotopicalAlgebra.IsFibrant CategoryTheory.ObjectProperty.FullSubcategory.obj HomotopicalAlgebra.fibrantObjects	—	CategoryTheory.ObjectProperty.FullSubcategory.property
instIsFibrantObjι 📖	mathematical	—	HomotopicalAlgebra.IsFibrant CategoryTheory.Functor.obj HomotopicalAlgebra.FibrantObject CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects ι	—	CategoryTheory.ObjectProperty.FullSubcategory.property
mk_surjective 📖	—	—	—	—	CategoryTheory.ObjectProperty.FullSubcategory.property
weakEquivalence_homMk_iff 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence HomotopicalAlgebra.FibrantObject CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects homMk HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory	—	—

---

← Back to Index