Theorems · Theorem · category theory

HomotopicalAlgebra.ModelCategory.hasLiftingProperty_of_joyalTrickDual

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : HomotopicalAlgebra.CategoryWithFibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [(HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty]
  [(HomotopicalAlgebra.trivialCofibrations C).HasFactorization (HomotopicalAlgebra.fibrations C)]
  [CategoryTheory.Limits.HasPullbacks C] [(HomotopicalAlgebra.fibrations C).IsStableUnderComposition]
  [(HomotopicalAlgebra.fibrations C).IsStableUnderBaseChange],
  (∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [HomotopicalAlgebra.Cofibration i] [HomotopicalAlgebra.WeakEquivalence p]
      [HomotopicalAlgebra.Fibration p], CategoryTheory.HasLiftingProperty i p) →
    ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [HomotopicalAlgebra.Cofibration i] [HomotopicalAlgebra.Fibration p]
      [HomotopicalAlgebra.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.

Defined in

Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick

Cited by

0 results in Mathlib

Foundations

Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryHomotopicalAlgebra.CategoryWithCofibrationsHomotopicalAlgebra.CategoryWithFibrationsHomotopicalAlgebra.CategoryWithWeakEquivalencesCategoryTheory.MorphismProperty.HasTwoOutOfThreePropertyCategoryTheory.MorphismProperty.HasFactorizationCategoryTheory.Limits.HasPullbacksCategoryTheory.MorphismProperty.IsStableUnderCompositionCategoryTheory.MorphismProperty.IsStableUnderBaseChangeHomotopicalAlgebra.CofibrationHomotopicalAlgebra.FibrationHomotopicalAlgebra.WeakEquivalence