The model category structure on Over categories

Let C be a model category. For any S : C, we define a model category structure on the category Over S: a morphism X ⟶ Y in Over S is a cofibration (resp. a fibration, a weak equivalence) if the underlying morphism f.left : X.left ⟶ Y.left is. (Apart from the existence of (finite) limits from Limits.Constructions.Over.Basic, the verification of the axioms is straightforward.)

TODO

• Proceed to the dual construction for Under S.

instance HomotopicalAlgebra.instCategoryWithCofibrationsOver {C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) [CategoryWithCofibrations C] : CategoryWithCofibrations (CategoryTheory.Over S)

Equations

• HomotopicalAlgebra.instCategoryWithCofibrationsOver S = { cofibrations := (HomotopicalAlgebra.cofibrations C).over }

theorem HomotopicalAlgebra.cofibrations_over_def {C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) [CategoryWithCofibrations C] : cofibrations (CategoryTheory.Over S) = (cofibrations C).over

theorem HomotopicalAlgebra.cofibrations_over_iff {C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) [CategoryWithCofibrations C] {X Y : CategoryTheory.Over S} (f : X ⟶ Y) : Cofibration f ↔ Cofibration f.left

instance HomotopicalAlgebra.instCofibrationLeftDiscretePUnitOfOver {C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) [CategoryWithCofibrations C] {X Y : CategoryTheory.Over S} (f : X ⟶ Y) [Cofibration f] : Cofibration f.left

instance HomotopicalAlgebra.instIsStableUnderRetractsOverCofibrations {C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) [CategoryWithCofibrations C] [(cofibrations C).IsStableUnderRetracts] : (cofibrations (CategoryTheory.Over S)).IsStableUnderRetracts

instance HomotopicalAlgebra.instCategoryWithFibrationsOver {C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) [CategoryWithFibrations C] : CategoryWithFibrations (CategoryTheory.Over S)

Equations

• HomotopicalAlgebra.instCategoryWithFibrationsOver S = { fibrations := (HomotopicalAlgebra.fibrations C).over }

theorem HomotopicalAlgebra.fibrations_over_def {C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) [CategoryWithFibrations C] : fibrations (CategoryTheory.Over S) = (fibrations C).over

theorem HomotopicalAlgebra.fibrations_over_iff {C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) [CategoryWithFibrations C] {X Y : CategoryTheory.Over S} (f : X ⟶ Y) : Fibration f ↔ Fibration f.left

instance HomotopicalAlgebra.instFibrationLeftDiscretePUnitOfOver {C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) [CategoryWithFibrations C] {X Y : CategoryTheory.Over S} (f : X ⟶ Y) [Fibration f] : Fibration f.left

instance HomotopicalAlgebra.instIsStableUnderRetractsOverFibrations {C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) [CategoryWithFibrations C] [(fibrations C).IsStableUnderRetracts] : (fibrations (CategoryTheory.Over S)).IsStableUnderRetracts

instance HomotopicalAlgebra.instCategoryWithWeakEquivalencesOver {C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) [CategoryWithWeakEquivalences C] : CategoryWithWeakEquivalences (CategoryTheory.Over S)

Equations

• HomotopicalAlgebra.instCategoryWithWeakEquivalencesOver S = { weakEquivalences := (HomotopicalAlgebra.weakEquivalences C).over }

theorem HomotopicalAlgebra.weakEquivalences_over_def {C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) [CategoryWithWeakEquivalences C] : weakEquivalences (CategoryTheory.Over S) = (weakEquivalences C).over

theorem HomotopicalAlgebra.weakEquivalences_over_iff {C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) [CategoryWithWeakEquivalences C] {X Y : CategoryTheory.Over S} (f : X ⟶ Y) : WeakEquivalence f ↔ WeakEquivalence f.left

instance HomotopicalAlgebra.instWeakEquivalenceLeftDiscretePUnitOfOver {C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) [CategoryWithWeakEquivalences C] {X Y : CategoryTheory.Over S} (f : X ⟶ Y) [WeakEquivalence f] : WeakEquivalence f.left

instance HomotopicalAlgebra.instIsStableUnderRetractsOverWeakEquivalences {C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) [CategoryWithWeakEquivalences C] [(weakEquivalences C).IsStableUnderRetracts] : (weakEquivalences (CategoryTheory.Over S)).IsStableUnderRetracts

theorem HomotopicalAlgebra.trivialCofibrations_over_eq {C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] : trivialCofibrations (CategoryTheory.Over S) = (trivialCofibrations C).over

theorem HomotopicalAlgebra.trivialFibrations_over_eq {C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) [CategoryWithWeakEquivalences C] [CategoryWithFibrations C] : trivialFibrations (CategoryTheory.Over S) = (trivialFibrations C).over

instance HomotopicalAlgebra.instHasTwoOutOfThreePropertyOverWeakEquivalences {C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) [CategoryWithWeakEquivalences C] [(weakEquivalences C).HasTwoOutOfThreeProperty] : (weakEquivalences (CategoryTheory.Over S)).HasTwoOutOfThreeProperty

instance HomotopicalAlgebra.instHasFactorizationOverTrivialCofibrationsFibrations {C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] [(trivialCofibrations C).HasFactorization (fibrations C)] : (trivialCofibrations (CategoryTheory.Over S)).HasFactorization (fibrations (CategoryTheory.Over S))

instance HomotopicalAlgebra.instHasFactorizationOverCofibrationsTrivialFibrations {C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) [CategoryWithWeakEquivalences C] [CategoryWithCofibrations C] [CategoryWithFibrations C] [(cofibrations C).HasFactorization (trivialFibrations C)] : (cofibrations (CategoryTheory.Over S)).HasFactorization (trivialFibrations (CategoryTheory.Over S))

instance HomotopicalAlgebra.ModelCategory.over {C : Type u} [CategoryTheory.Category.{v, u} C] (S : C) [ModelCategory C] : ModelCategory (CategoryTheory.Over S)

Equations

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