Transport a model category via an equivalence

Given an equivalence of categories e : C ≌ D, we transport a model category structure on D in order to obtain a model category structure on C. More precisely, we assume that C has been equipped with notions of cofibrations, fibrations and weak equivalences and that these properties of morphisms are the inverse images of the corresponding properties of morphisms by the functor e.functor : C ⥤ D. Under these assumptions, we show that the model category axioms for C hold if they hold for D.

@[implicit_reducible]

def HomotopicalAlgebra.ModelCategory.transport {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [ModelCategory D] [CategoryWithCofibrations C] [CategoryWithFibrations C] [CategoryWithWeakEquivalences C] (e : C ≌ D) (h₁ : cofibrations C = (cofibrations D).inverseImage e.functor) (h₂ : fibrations C = (fibrations D).inverseImage e.functor) (h₃ : weakEquivalences C = (weakEquivalences D).inverseImage e.functor) : ModelCategory C

Transport of a model category structure on a category D via an equivalence of categories e : C ≌ D. We assume that the category C is already endowed with a CategoryWithFibrations instance (and similarly for cofibrations and weak equivalences), and that the three properties of morphisms (fibrations, cofibrations, weak equivalences) in C coincide with the inverse images by e.functor : C ⥤ D of the corresponding properties of morphisms in D.

Equations

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