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 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][Quillen1967]
- [Paul G. Goerss, John F. Jardine, Simplicial Homotopy Theory][goerss-jardine-2009]
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 : HomotopicalAlgebra.CategoryWithFibrations C
- categoryWithCofibrations : HomotopicalAlgebra.CategoryWithCofibrations C
- categoryWithWeakEquivalences : HomotopicalAlgebra.CategoryWithWeakEquivalences C
- cm2 : (HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty
- cm3a : (HomotopicalAlgebra.weakEquivalences C).IsStableUnderRetracts
- cm3b : (HomotopicalAlgebra.fibrations C).IsStableUnderRetracts
- cm3c : (HomotopicalAlgebra.cofibrations C).IsStableUnderRetracts
- cm4a {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [HomotopicalAlgebra.Cofibration i] [HomotopicalAlgebra.WeakEquivalence i] [HomotopicalAlgebra.Fibration p] : CategoryTheory.HasLiftingProperty i p
- cm4b {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [HomotopicalAlgebra.Cofibration i] [HomotopicalAlgebra.Fibration p] [HomotopicalAlgebra.WeakEquivalence p] : CategoryTheory.HasLiftingProperty i p
- cm5a : (HomotopicalAlgebra.trivialCofibrations C).HasFactorization (HomotopicalAlgebra.fibrations C)
- cm5b : (HomotopicalAlgebra.cofibrations C).HasFactorization (HomotopicalAlgebra.trivialFibrations C)