Basic

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

Statistics

Metric	Count
Definitions ModelCategory, categoryWithCofibrations, categoryWithFibrations, categoryWithWeakEquivalences, mk'	5
Theorems cm1a, cm1b, cm2, cm3a, cm3b, cm3c, cm4a, cm4b, cm5a, cm5b, instIsWeakFactorizationSystemCofibrationsTrivialFibrations, instIsWeakFactorizationSystemTrivialCofibrationsFibrations	12
Total	17

HomotopicalAlgebra

Definitions

Name	Category	Theorems
ModelCategory 📖	CompData	—

HomotopicalAlgebra.ModelCategory

Definitions

Name	Category	Theorems
categoryWithCofibrations 📖	CompOp	122 math math: HomotopicalAlgebra.BifibrantObject.inverts_iff_factors, HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject_obj, HomotopicalAlgebra.CofibrantObject.homRel_equivalence_of_isFibrant_tgt, HomotopicalAlgebra.CofibrantObject.instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism, HomotopicalAlgebra.CofibrantObject.toHoCat_map_eq_iff, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceBifibrantObjectBifibrantResolutionMap, HomotopicalAlgebra.FibrantBrownFactorization.i_r_assoc, HomotopicalAlgebra.LeftHomotopyRel.exists_good_cylinder, HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRight_apply, HomotopicalAlgebra.CofibrantObject.instFaithfulHoCatHoCatιCofibrantObject, HomotopicalAlgebra.BifibrantObject.HoCat.homEquivLeft_symm_apply, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac', HomotopicalAlgebra.BifibrantObject.HoCat.homEquivLeft_apply, HomotopicalAlgebra.Cylinder.ofFactorizationData_i₀, HomotopicalAlgebra.FibrantBrownFactorization.instWeakEquivalenceR, HomotopicalAlgebra.Cylinder.LeftHomotopy.exists_good_cylinder, HomotopicalAlgebra.Cylinder.ofFactorizationData_i₁, HomotopicalAlgebra.FibrantBrownFactorization.mk'_i, HomotopicalAlgebra.LeftHomotopyRel.exists_very_good_cylinder, HomotopicalAlgebra.CofibrantBrownFactorization.instWeakEquivalenceICofibrationsTrivialFibrations, HomotopicalAlgebra.FibrantBrownFactorization.instWeakEquivalencePTrivialCofibrationsFibrations, HomotopicalAlgebra.BifibrantObject.toHoCat_map_eq, HomotopicalAlgebra.CofibrantObject.instHasLeftResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism, HomotopicalAlgebra.instHasFactorizationOppositeCofibrationsTrivialFibrationsOfTrivialCofibrationsFibrations, HomotopicalAlgebra.BifibrantObject.instIsIsoHoCatMapToHoCatOfWeakEquivalence, HomotopicalAlgebra.FibrantBrownFactorization.mk'_Z, HomotopicalAlgebra.BifibrantObject.instCongruenceHomRel, HomotopicalAlgebra.Cylinder.ofFactorizationData_I, HomotopicalAlgebra.CofibrantObject.instIsFibrantObjιBifibrantObjectιCofibrantObject, HomotopicalAlgebra.CofibrantObject.toHoCat_obj_surjective, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution'_obj, HomotopicalAlgebra.instHasFactorizationOppositeTrivialCofibrationsFibrationsOfCofibrationsTrivialFibrations, HomotopicalAlgebra.PathObject.exists_very_good, cm3c, HomotopicalAlgebra.PathObject.ofFactorizationData_p, HomotopicalAlgebra.BifibrantObject.instIsLocalizationHoCatToHoCatWeakEquivalences, HomotopicalAlgebra.CofibrantObject.instIsCofibrantObjFunctorWeakEquivalencesLocalizerMorphism, HomotopicalAlgebra.RightHomotopyRel.exists_very_good_pathObject, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac, HomotopicalAlgebra.PathObject.instIsCofibrantPOfFactorizationDataOfIsStableUnderCompositionCofibrations, HomotopicalAlgebra.CofibrantObject.exists_bifibrant_map, HomotopicalAlgebra.CofibrantObject.instFullHoCatToHoCat, HomotopicalAlgebra.Cylinder.ofFactorizationData_i, HomotopicalAlgebra.BifibrantObject.toHoCat_obj_surjective, HomotopicalAlgebra.CofibrantObject.instIsConnectedLeftResolutionWeakEquivalencesLocalizerMorphism, HomotopicalAlgebra.CofibrantObject.instIsCofibrantResolutionObj, instIsWeakFactorizationSystemTrivialCofibrationsFibrations, HomotopicalAlgebra.PathObject.ofFactorizationData_p₁, HomotopicalAlgebra.CofibrantBrownFactorization.s_p, HomotopicalAlgebra.CofibrantObject.instIsLocalizationCompHoCatToHoCatWeakEquivalences, HomotopicalAlgebra.FibrantObject.HoCat.exists_resolution, HomotopicalAlgebra.CofibrantObject.instIsLeftDerivabilityStructureWeakEquivalencesLocalizerMorphism, HomotopicalAlgebra.Cylinder.exists_very_good, HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences, HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRight_symm_apply, HomotopicalAlgebra.CofibrantObject.HoCat.resolutionObj_hom_ext, HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorHoCatAdjCounit', HomotopicalAlgebra.PathObject.instIsVeryGoodOfFactorizationData, HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorHoCatCounitHoCatAdj, HomotopicalAlgebra.FibrantBrownFactorization.fibration_r, HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorResolutionCompToLocalizationNatTrans, HomotopicalAlgebra.BifibrantObject.instIsStableUnderPostcompHomRel, HomotopicalAlgebra.FibrantObject.instCofibrationIResolutionObj, HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject_obj, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution_map, HomotopicalAlgebra.PathObject.ofFactorizationData_P, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac_assoc, HomotopicalAlgebra.BifibrantObject.homRel_iff_leftHomotopyRel, HomotopicalAlgebra.CofibrantBrownFactorization.cofibration_s, HomotopicalAlgebra.CofibrantObject.HoCat.adjCounitIso_inv_app, HomotopicalAlgebra.CofibrantObject.HoCat.adjUnit_app, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceIBifibrantResolutionObj, HomotopicalAlgebra.Cylinder.ofFactorizationData_π, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution_obj, HomotopicalAlgebra.CofibrantBrownFactorization.mk'_s, HomotopicalAlgebra.BifibrantObject.toHoCat_map_eq_iff, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceWWeakEquivalences, cm5b, HomotopicalAlgebra.CofibrantObject.localizerMorphism_functor, HomotopicalAlgebra.CofibrantObject.instIsStableUnderPrecompHomRel, HomotopicalAlgebra.CofibrantBrownFactorization.mk'_p, HomotopicalAlgebra.CofibrantBrownFactorization.s_p_assoc, cm5a, HomotopicalAlgebra.Cylinder.instIsVeryGoodOfFactorizationData, HomotopicalAlgebra.CofibrantObject.instIsIsoHoCatAppAdjCounit', HomotopicalAlgebra.BifibrantObject.instIsStableUnderPrecompHomRel, HomotopicalAlgebra.CofibrantObject.factorsThroughLocalization, HomotopicalAlgebra.FibrantBrownFactorization.mk'_r, HomotopicalAlgebra.instIsStableUnderRetractsOppositeFibrationsOfCofibrations, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppιCompResolutionNatTrans, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppAdjUnit, HomotopicalAlgebra.PathObject.ofFactorizationData_p₀, HomotopicalAlgebra.CofibrantBrownFactorization.mk'_Z, HomotopicalAlgebra.CofibrantObject.instFullHoCatHoCatιCofibrantObject, HomotopicalAlgebra.CofibrantObject.instIsLocalizationHoCatHoCatBifibrantResolutionWeakEquivalences, HomotopicalAlgebra.CofibrantObject.instHasQuotientWeakEquivalencesHomRel, HomotopicalAlgebra.CofibrantObject.HoCat.ιCompResolutionNatTrans_app, HomotopicalAlgebra.Cylinder.instIsGoodTrans, HomotopicalAlgebra.CofibrantObject.instIsLocalizationCompιWeakEquivalences, HomotopicalAlgebra.CofibrantObject.exists_bifibrant, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution'_map, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppUnitHoCatAdj, HomotopicalAlgebra.FibrantBrownFactorization.mk'_p, HomotopicalAlgebra.CofibrantObject.weakEquivalence_toHoCat_map_iff, HomotopicalAlgebra.PathObject.ofFactorizationData_ι, HomotopicalAlgebra.CofibrantObject.HoCat.localizerMorphismResolution_functor, HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject_map_toHoCat_map, HomotopicalAlgebra.BifibrantObject.homRel_iff_rightHomotopyRel, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, HomotopicalAlgebra.CofibrantBrownFactorization.instWeakEquivalenceS, HomotopicalAlgebra.CofibrantObject.HoCat.adjCounit'_app, HomotopicalAlgebra.FibrantBrownFactorization.i_r, HomotopicalAlgebra.BifibrantObject.instFullHoCatToHoCat, HomotopicalAlgebra.CofibrantObject.instIsStableUnderPostcompHomRel, instIsWeakFactorizationSystemCofibrationsTrivialFibrations, HomotopicalAlgebra.CofibrantObject.instCofibrationHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, HomotopicalAlgebra.CofibrantBrownFactorization.mk'_i, HomotopicalAlgebra.CofibrantObject.homRel_iff_rightHomotopyRel, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac'_assoc, HomotopicalAlgebra.CofibrantObject.instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism, HomotopicalAlgebra.CofibrantObject.toHoCat_map_eq, HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject_map_toHoCat_map
categoryWithFibrations 📖	CompOp	122 math math: HomotopicalAlgebra.FibrantObject.instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences, HomotopicalAlgebra.BifibrantObject.inverts_iff_factors, HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject_obj, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceBifibrantObjectBifibrantResolutionMap, HomotopicalAlgebra.FibrantBrownFactorization.i_r_assoc, HomotopicalAlgebra.FibrantObject.instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism, HomotopicalAlgebra.FibrantObject.instIsLocalizationCompHoCatToHoCatWeakEquivalences, HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRight_apply, HomotopicalAlgebra.CofibrantObject.instFaithfulHoCatHoCatιCofibrantObject, HomotopicalAlgebra.BifibrantObject.HoCat.homEquivLeft_symm_apply, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac', HomotopicalAlgebra.FibrantObject.toHoCat_map_eq_iff, HomotopicalAlgebra.BifibrantObject.HoCat.homEquivLeft_apply, HomotopicalAlgebra.FibrantObject.weakEquivalence_toHoCat_map_iff, HomotopicalAlgebra.Cylinder.ofFactorizationData_i₀, HomotopicalAlgebra.FibrantBrownFactorization.instWeakEquivalenceR, HomotopicalAlgebra.Cylinder.ofFactorizationData_i₁, HomotopicalAlgebra.FibrantBrownFactorization.mk'_i, HomotopicalAlgebra.LeftHomotopyRel.exists_very_good_cylinder, HomotopicalAlgebra.CofibrantBrownFactorization.instWeakEquivalenceICofibrationsTrivialFibrations, HomotopicalAlgebra.FibrantObject.homRel_iff_leftHomotopyRel, HomotopicalAlgebra.FibrantBrownFactorization.instWeakEquivalencePTrivialCofibrationsFibrations, HomotopicalAlgebra.FibrantObject.instHasRightResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism, HomotopicalAlgebra.BifibrantObject.toHoCat_map_eq, HomotopicalAlgebra.instHasFactorizationOppositeCofibrationsTrivialFibrationsOfTrivialCofibrationsFibrations, HomotopicalAlgebra.BifibrantObject.instIsIsoHoCatMapToHoCatOfWeakEquivalence, HomotopicalAlgebra.FibrantBrownFactorization.mk'_Z, HomotopicalAlgebra.CofibrantObject.instFibrationPResolutionObj, HomotopicalAlgebra.BifibrantObject.instCongruenceHomRel, HomotopicalAlgebra.Cylinder.ofFactorizationData_I, HomotopicalAlgebra.CofibrantObject.instIsFibrantObjιBifibrantObjectιCofibrantObject, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution'_obj, cm3b, HomotopicalAlgebra.FibrantObject.instWeakEquivalenceHoCatAppιCompResolutionNatTrans, HomotopicalAlgebra.instHasFactorizationOppositeTrivialCofibrationsFibrationsOfCofibrationsTrivialFibrations, HomotopicalAlgebra.PathObject.exists_very_good, HomotopicalAlgebra.PathObject.ofFactorizationData_p, HomotopicalAlgebra.FibrantObject.localizerMorphism_functor, HomotopicalAlgebra.FibrantObject.instFullHoCatToHoCat, HomotopicalAlgebra.BifibrantObject.instIsLocalizationHoCatToHoCatWeakEquivalences, HomotopicalAlgebra.FibrantObject.instIsLocalizationCompιWeakEquivalences, HomotopicalAlgebra.RightHomotopyRel.exists_very_good_pathObject, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac, HomotopicalAlgebra.CofibrantObject.exists_bifibrant_map, HomotopicalAlgebra.Cylinder.ofFactorizationData_i, HomotopicalAlgebra.BifibrantObject.toHoCat_obj_surjective, HomotopicalAlgebra.FibrantObject.toHoCat_map_eq, instIsWeakFactorizationSystemTrivialCofibrationsFibrations, HomotopicalAlgebra.PathObject.ofFactorizationData_p₁, HomotopicalAlgebra.Cylinder.instIsFibrantIOfFactorizationDataOfIsStableUnderCompositionFibrations, HomotopicalAlgebra.CofibrantBrownFactorization.s_p, HomotopicalAlgebra.FibrantObject.instIsConnectedRightResolutionWeakEquivalencesLocalizerMorphism, HomotopicalAlgebra.PathObject.instIsGoodTrans, HomotopicalAlgebra.RightHomotopyRel.exists_good_pathObject, HomotopicalAlgebra.Cylinder.exists_very_good, HomotopicalAlgebra.FibrantObject.HoCat.resolutionObj_hom_ext, HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRight_symm_apply, HomotopicalAlgebra.FibrantObject.instIsStableUnderPrecompHomRel, HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorHoCatAdjCounit', HomotopicalAlgebra.PathObject.instIsVeryGoodOfFactorizationData, HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorHoCatCounitHoCatAdj, HomotopicalAlgebra.FibrantBrownFactorization.fibration_r, HomotopicalAlgebra.BifibrantObject.instIsStableUnderPostcompHomRel, HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject_obj, HomotopicalAlgebra.PathObject.RightHomotopy.exists_good_pathObject, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution_map, HomotopicalAlgebra.PathObject.ofFactorizationData_P, HomotopicalAlgebra.FibrantObject.homRel_equivalence_of_isCofibrant_src, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac_assoc, HomotopicalAlgebra.BifibrantObject.homRel_iff_leftHomotopyRel, HomotopicalAlgebra.CofibrantBrownFactorization.cofibration_s, HomotopicalAlgebra.CofibrantObject.HoCat.adjCounitIso_inv_app, HomotopicalAlgebra.CofibrantObject.HoCat.adjUnit_app, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceIBifibrantResolutionObj, HomotopicalAlgebra.Cylinder.ofFactorizationData_π, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution_obj, HomotopicalAlgebra.CofibrantBrownFactorization.mk'_s, HomotopicalAlgebra.FibrantObject.instIsFibrantResolutionObj, HomotopicalAlgebra.BifibrantObject.toHoCat_map_eq_iff, HomotopicalAlgebra.FibrantObject.instHasQuotientWeakEquivalencesHomRel, cm5b, HomotopicalAlgebra.FibrantObject.instWeakEquivalenceWWeakEquivalences, HomotopicalAlgebra.FibrantObject.HoCat.ιCompResolutionNatTrans_app, HomotopicalAlgebra.CofibrantBrownFactorization.mk'_p, HomotopicalAlgebra.CofibrantBrownFactorization.s_p_assoc, cm5a, HomotopicalAlgebra.FibrantObject.toHoCat_obj_surjective, HomotopicalAlgebra.Cylinder.instIsVeryGoodOfFactorizationData, HomotopicalAlgebra.CofibrantObject.instIsIsoHoCatAppAdjCounit', HomotopicalAlgebra.BifibrantObject.instIsStableUnderPrecompHomRel, HomotopicalAlgebra.FibrantBrownFactorization.mk'_r, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppAdjUnit, HomotopicalAlgebra.PathObject.ofFactorizationData_p₀, HomotopicalAlgebra.CofibrantBrownFactorization.mk'_Z, HomotopicalAlgebra.FibrantObject.instIsIsoFunctorResolutionCompToLocalizationNatTrans, HomotopicalAlgebra.CofibrantObject.instFullHoCatHoCatιCofibrantObject, HomotopicalAlgebra.CofibrantObject.instIsLocalizationHoCatHoCatBifibrantResolutionWeakEquivalences, HomotopicalAlgebra.instIsStableUnderRetractsOppositeCofibrationsOfFibrations, HomotopicalAlgebra.FibrantObject.instIsFibrantObjFunctorWeakEquivalencesLocalizerMorphism, HomotopicalAlgebra.CofibrantObject.exists_bifibrant, HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution'_map, HomotopicalAlgebra.FibrantObject.factorsThroughLocalization, HomotopicalAlgebra.CofibrantObject.HoCat.exists_resolution, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppUnitHoCatAdj, HomotopicalAlgebra.FibrantBrownFactorization.mk'_p, HomotopicalAlgebra.PathObject.ofFactorizationData_ι, HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject_map_toHoCat_map, HomotopicalAlgebra.BifibrantObject.homRel_iff_rightHomotopyRel, HomotopicalAlgebra.FibrantObject.HoCat.localizerMorphismResolution_functor, HomotopicalAlgebra.FibrantObject.instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, HomotopicalAlgebra.CofibrantBrownFactorization.instWeakEquivalenceS, HomotopicalAlgebra.FibrantObject.instIsRightDerivabilityStructureWeakEquivalencesLocalizerMorphism, HomotopicalAlgebra.CofibrantObject.HoCat.adjCounit'_app, HomotopicalAlgebra.FibrantBrownFactorization.i_r, HomotopicalAlgebra.BifibrantObject.instFullHoCatToHoCat, instIsWeakFactorizationSystemCofibrationsTrivialFibrations, HomotopicalAlgebra.CofibrantObject.instCofibrationHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, HomotopicalAlgebra.CofibrantBrownFactorization.mk'_i, HomotopicalAlgebra.FibrantObject.instIsStableUnderPostcompHomRel, HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac'_assoc, HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject_map_toHoCat_map
categoryWithWeakEquivalences 📖	CompOp	123 math math: HomotopicalAlgebra.BifibrantObject.inverts_iff_factors, HomotopicalAlgebra.LeftHomotopyClass.mk_eq_mk_iff, HomotopicalAlgebra.CofibrantObject.instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceBifibrantObjectBifibrantResolutionMap, HomotopicalAlgebra.FibrantBrownFactorization.i_r_assoc, HomotopicalAlgebra.FibrantObject.instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism, HomotopicalAlgebra.LeftHomotopyClass.whitehead, HomotopicalAlgebra.FibrantObject.instIsLocalizationCompHoCatToHoCatWeakEquivalences, HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRight_apply, HomotopicalAlgebra.BifibrantObject.HoCat.homEquivLeft_symm_apply, HomotopicalAlgebra.PathObject.instNonempty, HomotopicalAlgebra.BifibrantObject.HoCat.homEquivLeft_apply, HomotopicalAlgebra.FibrantObject.weakEquivalence_toHoCat_map_iff, HomotopicalAlgebra.Cylinder.ofFactorizationData_i₀, HomotopicalAlgebra.FibrantBrownFactorization.instWeakEquivalenceR, HomotopicalAlgebra.Cylinder.LeftHomotopy.exists_good_cylinder, HomotopicalAlgebra.Cylinder.ofFactorizationData_i₁, HomotopicalAlgebra.FibrantBrownFactorization.mk'_i, HomotopicalAlgebra.CofibrantBrownFactorization.instWeakEquivalenceICofibrationsTrivialFibrations, HomotopicalAlgebra.FibrantObject.homRel_iff_leftHomotopyRel, HomotopicalAlgebra.FibrantBrownFactorization.instWeakEquivalencePTrivialCofibrationsFibrations, HomotopicalAlgebra.FibrantObject.instHasRightResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism, HomotopicalAlgebra.leftHomotopyClassEquivRightHomotopyClass_symm_mk, HomotopicalAlgebra.Cylinder.LeftHomotopy.covering_homotopy, HomotopicalAlgebra.CofibrantObject.instHasLeftResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism, HomotopicalAlgebra.instHasFactorizationOppositeCofibrationsTrivialFibrationsOfTrivialCofibrationsFibrations, HomotopicalAlgebra.FibrantBrownFactorization.mk'_Z, HomotopicalAlgebra.CofibrantObject.HoCat.weakEquivalence_resolutionMap_iff, HomotopicalAlgebra.FibrantObject.instWeakEquivalenceIResolutionObj, HomotopicalAlgebra.Cylinder.ofFactorizationData_I, HomotopicalAlgebra.LeftHomotopyClass.postcomp_bijective_of_weakEquivalence, HomotopicalAlgebra.LeftHomotopyClass.postcomp_bijective_of_fibration_of_weakEquivalence, HomotopicalAlgebra.instHasFactorizationOppositeTrivialCofibrationsFibrationsOfCofibrationsTrivialFibrations, HomotopicalAlgebra.PathObject.exists_very_good, HomotopicalAlgebra.PathObject.ofFactorizationData_p, HomotopicalAlgebra.FibrantObject.localizerMorphism_functor, HomotopicalAlgebra.BifibrantObject.instIsLocalizationHoCatToHoCatWeakEquivalences, HomotopicalAlgebra.FibrantObject.instIsLocalizationCompιWeakEquivalences, HomotopicalAlgebra.CofibrantObject.instIsCofibrantObjFunctorWeakEquivalencesLocalizerMorphism, HomotopicalAlgebra.Cylinder.trans_π, HomotopicalAlgebra.PathObject.instIsCofibrantPOfFactorizationDataOfIsStableUnderCompositionCofibrations, HomotopicalAlgebra.Cylinder.ofFactorizationData_i, HomotopicalAlgebra.CofibrantObject.instIsConnectedLeftResolutionWeakEquivalencesLocalizerMorphism, instIsWeakFactorizationSystemTrivialCofibrationsFibrations, HomotopicalAlgebra.PathObject.ofFactorizationData_p₁, HomotopicalAlgebra.Cylinder.instIsFibrantIOfFactorizationDataOfIsStableUnderCompositionFibrations, HomotopicalAlgebra.CofibrantBrownFactorization.s_p, HomotopicalAlgebra.FibrantObject.instIsConnectedRightResolutionWeakEquivalencesLocalizerMorphism, HomotopicalAlgebra.CofibrantObject.instIsLocalizationCompHoCatToHoCatWeakEquivalences, HomotopicalAlgebra.PathObject.instIsGoodTrans, HomotopicalAlgebra.FibrantObject.HoCat.exists_resolution, HomotopicalAlgebra.CofibrantObject.instIsLeftDerivabilityStructureWeakEquivalencesLocalizerMorphism, HomotopicalAlgebra.PathObject.trans_p₀, HomotopicalAlgebra.Cylinder.exists_very_good, HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRight_symm_apply, HomotopicalAlgebra.PathObject.instIsVeryGoodOfFactorizationData, HomotopicalAlgebra.FibrantBrownFactorization.fibration_r, HomotopicalAlgebra.FibrantObject.HoCat.weakEquivalence_resolutionMap_iff, HomotopicalAlgebra.RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalence, HomotopicalAlgebra.instIsStableUnderRetractsOppositeWeakEquivalences, HomotopicalAlgebra.PathObject.RightHomotopy.exists_good_pathObject, HomotopicalAlgebra.PathObject.ofFactorizationData_P, HomotopicalAlgebra.Cylinder.trans_i₀, HomotopicalAlgebra.BifibrantObject.homRel_iff_leftHomotopyRel, HomotopicalAlgebra.CofibrantBrownFactorization.cofibration_s, cm3a, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceIBifibrantResolutionObj, HomotopicalAlgebra.Cylinder.ofFactorizationData_π, HomotopicalAlgebra.PathObject.trans_ι, HomotopicalAlgebra.CofibrantBrownFactorization.mk'_s, HomotopicalAlgebra.FibrantObject.instHasQuotientWeakEquivalencesHomRel, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceWWeakEquivalences, cm5b, HomotopicalAlgebra.FibrantObject.instWeakEquivalenceWWeakEquivalences, HomotopicalAlgebra.RightHomotopyRel.equivalence, HomotopicalAlgebra.CofibrantObject.localizerMorphism_functor, HomotopicalAlgebra.CofibrantBrownFactorization.mk'_p, cm2, HomotopicalAlgebra.CofibrantBrownFactorization.s_p_assoc, cm5a, HomotopicalAlgebra.CofibrantObject.instWeakEquivalencePResolutionObj, HomotopicalAlgebra.Cylinder.instIsVeryGoodOfFactorizationData, HomotopicalAlgebra.Cylinder.trans_I, HomotopicalAlgebra.CofibrantObject.factorsThroughLocalization, HomotopicalAlgebra.FibrantBrownFactorization.mk'_r, HomotopicalAlgebra.RightHomotopyClass.precomp_bijective_of_weakEquivalence, HomotopicalAlgebra.RightHomotopyClass.whitehead, HomotopicalAlgebra.leftHomotopyRel_iff_rightHomotopyRel, HomotopicalAlgebra.Cylinder.trans_i₁, HomotopicalAlgebra.PathObject.ofFactorizationData_p₀, HomotopicalAlgebra.LeftHomotopyRel.equivalence, HomotopicalAlgebra.CofibrantBrownFactorization.mk'_Z, HomotopicalAlgebra.RightHomotopyClass.mk_eq_mk_iff, HomotopicalAlgebra.CofibrantObject.instHasQuotientWeakEquivalencesHomRel, HomotopicalAlgebra.FibrantObject.instIsFibrantObjFunctorWeakEquivalencesLocalizerMorphism, HomotopicalAlgebra.Cylinder.instIsGoodTrans, HomotopicalAlgebra.CofibrantObject.instIsLocalizationCompιWeakEquivalences, HomotopicalAlgebra.CofibrantObject.exists_bifibrant, HomotopicalAlgebra.FibrantObject.factorsThroughLocalization, HomotopicalAlgebra.CofibrantObject.HoCat.exists_resolution, HomotopicalAlgebra.FibrantBrownFactorization.mk'_p, HomotopicalAlgebra.CofibrantObject.weakEquivalence_toHoCat_map_iff, HomotopicalAlgebra.PathObject.ofFactorizationData_ι, HomotopicalAlgebra.LeftHomotopyRel.refl, HomotopicalAlgebra.CofibrantObject.HoCat.localizerMorphismResolution_functor, HomotopicalAlgebra.instHasTwoOutOfThreePropertyOppositeWeakEquivalences, HomotopicalAlgebra.BifibrantObject.homRel_iff_rightHomotopyRel, HomotopicalAlgebra.FibrantObject.HoCat.localizerMorphismResolution_functor, HomotopicalAlgebra.FibrantObject.instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism, HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj, HomotopicalAlgebra.CofibrantBrownFactorization.instWeakEquivalenceS, HomotopicalAlgebra.leftHomotopyClassEquivRightHomotopyClass_mk, HomotopicalAlgebra.FibrantObject.instIsRightDerivabilityStructureWeakEquivalencesLocalizerMorphism, HomotopicalAlgebra.FibrantBrownFactorization.i_r, HomotopicalAlgebra.RightHomotopyRel.refl, HomotopicalAlgebra.PathObject.RightHomotopy.homotopy_extension, instIsWeakFactorizationSystemCofibrationsTrivialFibrations, HomotopicalAlgebra.PathObject.trans_p₁, HomotopicalAlgebra.CofibrantBrownFactorization.mk'_i, HomotopicalAlgebra.PathObject.trans_P, HomotopicalAlgebra.CofibrantObject.homRel_iff_rightHomotopyRel, HomotopicalAlgebra.CofibrantObject.instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism, HomotopicalAlgebra.Cylinder.instNonempty
mk' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cm1a 📖	mathematical	—	CategoryTheory.Limits.HasFiniteLimits	—	—
cm1b 📖	mathematical	—	CategoryTheory.Limits.HasFiniteColimits	—	—
cm2 📖	mathematical	—	CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty HomotopicalAlgebra.weakEquivalences categoryWithWeakEquivalences	—	—
cm3a 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderRetracts HomotopicalAlgebra.weakEquivalences categoryWithWeakEquivalences	—	—
cm3b 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderRetracts HomotopicalAlgebra.fibrations categoryWithFibrations	—	—
cm3c 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderRetracts HomotopicalAlgebra.cofibrations categoryWithCofibrations	—	—
cm4a 📖	mathematical	—	CategoryTheory.HasLiftingProperty	—	—
cm4b 📖	mathematical	—	CategoryTheory.HasLiftingProperty	—	—
cm5a 📖	mathematical	—	CategoryTheory.MorphismProperty.HasFactorization HomotopicalAlgebra.trivialCofibrations categoryWithCofibrations categoryWithWeakEquivalences HomotopicalAlgebra.fibrations categoryWithFibrations	—	—
cm5b 📖	mathematical	—	CategoryTheory.MorphismProperty.HasFactorization HomotopicalAlgebra.cofibrations categoryWithCofibrations HomotopicalAlgebra.trivialFibrations categoryWithFibrations categoryWithWeakEquivalences	—	—
instIsWeakFactorizationSystemCofibrationsTrivialFibrations 📖	mathematical	—	CategoryTheory.MorphismProperty.IsWeakFactorizationSystem HomotopicalAlgebra.cofibrations categoryWithCofibrations HomotopicalAlgebra.trivialFibrations categoryWithFibrations categoryWithWeakEquivalences	—	CategoryTheory.MorphismProperty.IsWeakFactorizationSystem.mk' cm5b cm3c HomotopicalAlgebra.instIsStableUnderRetractsTrivialFibrationsOfFibrationsOfWeakEquivalences cm3b cm3a HomotopicalAlgebra.mem_trivialFibrations_iff cm4b HomotopicalAlgebra.cofibration_iff
instIsWeakFactorizationSystemTrivialCofibrationsFibrations 📖	mathematical	—	CategoryTheory.MorphismProperty.IsWeakFactorizationSystem HomotopicalAlgebra.trivialCofibrations categoryWithCofibrations categoryWithWeakEquivalences HomotopicalAlgebra.fibrations categoryWithFibrations	—	CategoryTheory.MorphismProperty.IsWeakFactorizationSystem.mk' cm5a HomotopicalAlgebra.instIsStableUnderRetractsTrivialCofibrationsOfCofibrationsOfWeakEquivalences cm3c cm3a cm3b HomotopicalAlgebra.mem_trivialCofibrations_iff cm4a HomotopicalAlgebra.fibration_iff

---

← Back to Index