A trick by Joyal

In order to construct a model category, we may sometimes have basically proven all the axioms with the exception of the left lifting property of cofibrations with respect to trivial fibrations. A trick by Joyal allows to obtain this lifting property under suitable assumptions, namely that cofibrations are stable under composition and cobase change. (The dual result is also formalized.)

References

• John F. Jardine, Simplicial presheaves

theorem HomotopicalAlgebra.ModelCategory.hasLiftingProperty_of_joyalTrick {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryWithCofibrations C] [CategoryWithFibrations C] [CategoryWithWeakEquivalences C] [(weakEquivalences C).HasTwoOutOfThreeProperty] [(cofibrations C).HasFactorization (trivialFibrations C)] [CategoryTheory.Limits.HasPushouts C] [(cofibrations C).IsStableUnderComposition] [(cofibrations C).IsStableUnderCobaseChange] (h : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [Fibration p], CategoryTheory.HasLiftingProperty i p) {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [Fibration p] [WeakEquivalence p] : CategoryTheory.HasLiftingProperty i p

Joyal's trick: that cofibrations have the left lifting property with respect to trivial fibrations follows from the left lifting property of trivial cofibrations with respect to fibrations and a few other consequences of the model categories axioms.

theorem HomotopicalAlgebra.ModelCategory.hasLiftingProperty_of_joyalTrickDual {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryWithCofibrations C] [CategoryWithFibrations C] [CategoryWithWeakEquivalences C] [(weakEquivalences C).HasTwoOutOfThreeProperty] [(trivialCofibrations C).HasFactorization (fibrations C)] [CategoryTheory.Limits.HasPullbacks C] [(fibrations C).IsStableUnderComposition] [(fibrations C).IsStableUnderBaseChange] (h : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [Fibration p], CategoryTheory.HasLiftingProperty i p) {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [Fibration p] [WeakEquivalence i] : CategoryTheory.HasLiftingProperty i p

Joyal's trick (dual): that trivial cofibrations have the left lifting property with respect to fibrations follows from the left lifting property of cofibrations with respect to trivial fibrations and a few other consequences of the model categories axioms.