The left derivability structure attached to a model category

We show that the inclusion of the full subcategory of cofibrant objects in a model category is a left derivability structure. This is the dual to Corollaire 10.10 in the paper by Kahn and Maltsiniotis.

References

• Bruno Kahn and Georges Maltsiniotis, Structures de dérivabilité

instance HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceWWeakEquivalences {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [ModelCategory C] {X : C} (R : (localizerMorphism C).LeftResolution X) : WeakEquivalence R.w

instance HomotopicalAlgebra.CofibrantObject.instIsConnectedLeftResolutionWeakEquivalencesLocalizerMorphism {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [ModelCategory C] (X : C) : CategoryTheory.IsConnected ((localizerMorphism C).LeftResolution X)

instance HomotopicalAlgebra.CofibrantObject.instHasLeftResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [ModelCategory C] : (localizerMorphism C).arrow.HasLeftResolutions

instance HomotopicalAlgebra.CofibrantObject.instIsLeftDerivabilityStructureWeakEquivalencesLocalizerMorphism {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [ModelCategory C] : (localizerMorphism C).IsLeftDerivabilityStructure