DerivabilityStructureFibrant

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

Statistics

Metric	Count
Definitions	0
Theorems instHasRightResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism, instIsConnectedRightResolutionWeakEquivalencesLocalizerMorphism, instIsRightDerivabilityStructureWeakEquivalencesLocalizerMorphism, instWeakEquivalenceWWeakEquivalences	4
Total	4

HomotopicalAlgebra.FibrantObject

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasRightResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism 📖	mathematical	—	CategoryTheory.LocalizerMorphism.HasRightResolutions CategoryTheory.Arrow HomotopicalAlgebra.FibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects CategoryTheory.instCategoryArrow CategoryTheory.MorphismProperty.arrow HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences CategoryTheory.LocalizerMorphism.arrow localizerMorphism	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype instIsFibrantResolutionObj HoCat.resolutionMap_fac HomotopicalAlgebra.mem_weakEquivalences instWeakEquivalenceIResolutionObj
instIsConnectedRightResolutionWeakEquivalencesLocalizerMorphism 📖	mathematical	—	CategoryTheory.IsConnected CategoryTheory.LocalizerMorphism.RightResolution HomotopicalAlgebra.FibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences localizerMorphism CategoryTheory.LocalizerMorphism.RightResolution.instCategory	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype instIsFibrantResolutionObj HomotopicalAlgebra.mem_weakEquivalences instWeakEquivalenceIResolutionObj CategoryTheory.Limits.terminal.comp_from CategoryTheory.Zigzag.of_inv CategoryTheory.ObjectProperty.FullSubcategory.property CategoryTheory.sq_hasLift_of_hasLiftingProperty HomotopicalAlgebra.ModelCategory.cm4a instCofibrationIResolutionObj instIsFibrantObjFunctorWeakEquivalencesLocalizerMorphism CategoryTheory.CommSq.fac_left CategoryTheory.zigzag_isConnected CategoryTheory.Zigzag.trans CategoryTheory.Zigzag.symm
instIsRightDerivabilityStructureWeakEquivalencesLocalizerMorphism 📖	mathematical	—	CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure HomotopicalAlgebra.FibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences localizerMorphism	—	CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.mk' CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype instIsConnectedRightResolutionWeakEquivalencesLocalizerMorphism instHasRightResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism 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.FibrantObject HomotopicalAlgebra.ModelCategory.categoryWithFibrations CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype Fintype.instPEmpty CategoryTheory.ObjectProperty.FullSubcategory.category HomotopicalAlgebra.fibrantObjects CategoryTheory.LocalizerMorphism.functor HomotopicalAlgebra.weakEquivalences HomotopicalAlgebra.instCategoryWithWeakEquivalencesFullSubcategory HomotopicalAlgebra.ModelCategory.categoryWithWeakEquivalences localizerMorphism CategoryTheory.LocalizerMorphism.RightResolution.X₁ CategoryTheory.LocalizerMorphism.RightResolution.w	—	CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.Limits.hasFiniteProducts_of_hasFiniteLimits HomotopicalAlgebra.ModelCategory.cm1a Finite.of_fintype CategoryTheory.LocalizerMorphism.RightResolution.hw

---

← Back to Index