DerivabilityStructureCofibrant

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

Statistics

Metric	Count
Definitions	0
Theorems instHasLeftResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism, instIsConnectedLeftResolutionWeakEquivalencesLocalizerMorphism, instIsLeftDerivabilityStructureWeakEquivalencesLocalizerMorphism, instWeakEquivalenceWWeakEquivalences	4
Total	4

HomotopicalAlgebra.CofibrantObject

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasLeftResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism 📖	mathematical	—	CategoryTheory.LocalizerMorphism.HasLeftResolutions CategoryTheory.Arrow 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.instCategoryArrow CategoryTheory.MorphismProperty.arrow HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences CategoryTheory.LocalizerMorphism.arrow localizerMorphism	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype instIsCofibrantResolutionObj HoCat.resolutionMap_fac HomotopicalAlgebra.mem_weakEquivalences instWeakEquivalencePResolutionObj
instIsConnectedLeftResolutionWeakEquivalencesLocalizerMorphism 📖	mathematical	—	CategoryTheory.IsConnected CategoryTheory.LocalizerMorphism.LeftResolution HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences localizerMorphism CategoryTheory.LocalizerMorphism.LeftResolution.instCategory	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype instIsCofibrantResolutionObj HomotopicalAlgebra.mem_weakEquivalences instWeakEquivalencePResolutionObj CategoryTheory.Limits.initial.to_comp CategoryTheory.Zigzag.of_hom CategoryTheory.ObjectProperty.FullSubcategory.property CategoryTheory.sq_hasLift_of_hasLiftingProperty HomotopicalAlgebra.ModelCategory.cm4b instIsCofibrantObjFunctorWeakEquivalencesLocalizerMorphism instFibrationPResolutionObj CategoryTheory.CommSq.fac_right CategoryTheory.zigzag_isConnected CategoryTheory.Zigzag.trans CategoryTheory.Zigzag.symm
instIsLeftDerivabilityStructureWeakEquivalencesLocalizerMorphism 📖	mathematical	—	CategoryTheory.LocalizerMorphism.IsLeftDerivabilityStructure HomotopicalAlgebra.CofibrantObject HomotopicalAlgebra.ModelCategory.categoryWithCofibrations CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.cofibrantObjects HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences localizerMorphism	—	CategoryTheory.LocalizerMorphism.IsLeftDerivabilityStructure.mk' CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype instIsConnectedLeftResolutionWeakEquivalencesLocalizerMorphism instHasLeftResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism CategoryTheory.MorphismProperty.IsMultiplicative.toContainsIdentities HomotopicalAlgebra.instIsMultiplicativeWeakEquivalencesOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsOfIsStableUnderComposition HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemTrivialCofibrationsFibrations HomotopicalAlgebra.ModelCategory.cm3a CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toIsStableUnderComposition HomotopicalAlgebra.ModelCategory.cm2 instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism
instWeakEquivalenceWWeakEquivalences 📖	mathematical	—	HomotopicalAlgebra.WeakEquivalence 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 CategoryTheory.LocalizerMorphism.functor HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences localizerMorphism CategoryTheory.LocalizerMorphism.LeftResolution.X₁ CategoryTheory.LocalizerMorphism.LeftResolution.w	—	CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits HomotopicalAlgebra.ModelCategory.cm1b Finite.of_fintype CategoryTheory.LocalizerMorphism.LeftResolution.hw

---

← Back to Index