Model categories

We introduce a typeclass ModelCategory C expressing that C is equipped with classes of morphisms named "fibrations", "cofibrations" and "weak equivalences" with satisfy the axioms of (closed) model categories as they appear for example in Simplicial Homotopy Theory by Goerss and Jardine. We also provide an alternate constructor ModelCategory.mk' which uses a formulation of the axioms using weak factorizations systems.

As a given category C may have several model category structures, it is advisable to define only local instances of ModelCategory, or to set these instances on type synonyms.

References

• Daniel G. Quillen, Homotopical algebra
• Paul G. Goerss, John F. Jardine, Simplicial Homotopy Theory
• https://ncatlab.org/nlab/show/model+category

class HomotopicalAlgebra.ModelCategory (C : Type u) [CategoryTheory.Category.{v, u} C] : Type (max u v)

A model category is a category equipped with classes of morphisms named cofibrations, fibrations and weak equivalences which satisfies the axioms CM1/CM2/CM3/CM4/CM5 of (closed) model categories.

• categoryWithFibrations : CategoryWithFibrations C
• categoryWithCofibrations : CategoryWithCofibrations C
• categoryWithWeakEquivalences : CategoryWithWeakEquivalences C
• cm1a : CategoryTheory.Limits.HasFiniteLimits C
• cm1b : CategoryTheory.Limits.HasFiniteColimits C
• cm2 : (weakEquivalences C).HasTwoOutOfThreeProperty
• cm3a : (weakEquivalences C).IsStableUnderRetracts
• cm3b : (fibrations C).IsStableUnderRetracts
• cm3c : (cofibrations C).IsStableUnderRetracts
• cm4a {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [Fibration p] : CategoryTheory.HasLiftingProperty i p
• cm4b {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [Fibration p] [WeakEquivalence p] : CategoryTheory.HasLiftingProperty i p
• cm5a : (trivialCofibrations C).HasFactorization (fibrations C)
• cm5b : (cofibrations C).HasFactorization (trivialFibrations C)

instance HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemTrivialCofibrationsFibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [ModelCategory C] : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)

instance HomotopicalAlgebra.ModelCategory.instIsWeakFactorizationSystemCofibrationsTrivialFibrations (C : Type u) [CategoryTheory.Category.{v, u} C] [ModelCategory C] : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)

def HomotopicalAlgebra.ModelCategory.mk' (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithFibrations C] [CategoryWithCofibrations C] [CategoryWithWeakEquivalences C] [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.HasFiniteColimits C] [(weakEquivalences C).HasTwoOutOfThreeProperty] [(cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)] [(trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)] : ModelCategory C

Constructor for ModelCategory C which assumes a formulation of axioms using weak factorizations systems.

Equations

• One or more equations did not get rendered due to their size.