The right derivability structure attached to a model category

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

References

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

instance HomotopicalAlgebra.FibrantObject.instWeakEquivalenceWWeakEquivalences {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X : C} (R : (localizerMorphism C).RightResolution X) : WeakEquivalence R.w

instance HomotopicalAlgebra.FibrantObject.instIsConnectedRightResolutionWeakEquivalencesLocalizerMorphism {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] (X : C) : CategoryTheory.IsConnected ((localizerMorphism C).RightResolution X)

instance HomotopicalAlgebra.FibrantObject.instHasRightResolutionsArrowArrowWeakEquivalencesArrowLocalizerMorphism {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : (localizerMorphism C).arrow.HasRightResolutions

instance HomotopicalAlgebra.FibrantObject.instIsRightDerivabilityStructureWeakEquivalencesLocalizerMorphism {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : (localizerMorphism C).IsRightDerivabilityStructure