The homotopy category of cofibrant objects

Let C be a model category. By using the right homotopy relation, we introduce the homotopy category CofibrantObject.HoCat C of cofibrant objects in C, and we define a cofibrant resolution functor CofibrantObject.HoCat.resolution : C ⥤ CofibrantObject.HoCat C.

References

• Daniel G. Quillen, Homotopical algebra

def HomotopicalAlgebra.CofibrantObject.homRel (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : HomRel (CofibrantObject C)

The right homotopy relation on the category of cofibrant objects.

Equations

• HomotopicalAlgebra.CofibrantObject.homRel C f g = HomotopicalAlgebra.RightHomotopyRel f.hom g.hom

theorem HomotopicalAlgebra.CofibrantObject.homRel_iff_rightHomotopyRel {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : CofibrantObject C} {f g : X ⟶ Y} : homRel C f g ↔ RightHomotopyRel f.hom g.hom

instance HomotopicalAlgebra.CofibrantObject.instIsStableUnderPostcompHomRel {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : CategoryTheory.HomRel.IsStableUnderPostcomp (homRel C)

instance HomotopicalAlgebra.CofibrantObject.instIsStableUnderPrecompHomRel {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : CategoryTheory.HomRel.IsStableUnderPrecomp (homRel C)

theorem HomotopicalAlgebra.CofibrantObject.homRel_equivalence_of_isFibrant_tgt {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : CofibrantObject C} [IsFibrant Y.obj] : Equivalence fun (x1 x2 : X ⟶ Y) => homRel C x1 x2

@[reducible, inline]

abbrev HomotopicalAlgebra.CofibrantObject.HoCat (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : Type u_1

The homotopy category of cofibrant objects.

Equations

• HomotopicalAlgebra.CofibrantObject.HoCat C = CategoryTheory.Quotient (HomotopicalAlgebra.CofibrantObject.homRel C)

def HomotopicalAlgebra.CofibrantObject.toHoCat {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : CategoryTheory.Functor (CofibrantObject C) (HoCat C)

The quotient functor from the category of cofibrant objects to its homotopy category.

Equations

• HomotopicalAlgebra.CofibrantObject.toHoCat = CategoryTheory.Quotient.functor (HomotopicalAlgebra.CofibrantObject.homRel C)

theorem HomotopicalAlgebra.CofibrantObject.toHoCat_obj_surjective {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : Function.Surjective toHoCat.obj

instance HomotopicalAlgebra.CofibrantObject.instFullHoCatToHoCat {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : toHoCat.Full

theorem HomotopicalAlgebra.CofibrantObject.toHoCat_map_eq {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : CofibrantObject C} {f g : X ⟶ Y} (h : homRel C f g) : toHoCat.map f = toHoCat.map g

theorem HomotopicalAlgebra.CofibrantObject.toHoCat_map_eq_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : CofibrantObject C} [IsFibrant Y.obj] (f g : X ⟶ Y) : toHoCat.map f = toHoCat.map g ↔ homRel C f g

instance HomotopicalAlgebra.CofibrantObject.instHasQuotientWeakEquivalencesHomRel {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : (weakEquivalences (CofibrantObject C)).HasQuotient (homRel C)

@[instance_reducible]

instance HomotopicalAlgebra.CofibrantObject.instCategoryWithWeakEquivalencesHoCat {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : CategoryWithWeakEquivalences (HoCat C)

Equations

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

theorem HomotopicalAlgebra.CofibrantObject.weakEquivalence_toHoCat_map_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : CofibrantObject C} (f : X ⟶ Y) : WeakEquivalence (toHoCat.map f) ↔ WeakEquivalence f

def HomotopicalAlgebra.CofibrantObject.toHoCatLocalizerMorphism (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : CategoryTheory.LocalizerMorphism (weakEquivalences (CofibrantObject C)) (weakEquivalences (HoCat C))

The functor CofibrantObject C ⥤ HoCat C, considered as a localizer morphism.

Equations

• HomotopicalAlgebra.CofibrantObject.toHoCatLocalizerMorphism C = { functor := HomotopicalAlgebra.CofibrantObject.toHoCat, map := ⋯ }

theorem HomotopicalAlgebra.CofibrantObject.factorsThroughLocalization (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : (homRel C).FactorsThroughLocalization (weakEquivalences (CofibrantObject C))

instance HomotopicalAlgebra.CofibrantObject.instIsLocalizedEquivalenceHoCatWeakEquivalencesToHoCatLocalizerMorphism {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : (toHoCatLocalizerMorphism C).IsLocalizedEquivalence

instance HomotopicalAlgebra.CofibrantObject.instIsLocalizationCompHoCatToHoCatWeakEquivalences {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor (HoCat C) D) [L.IsLocalization (weakEquivalences (HoCat C))] : (toHoCat.comp L).IsLocalization (weakEquivalences (CofibrantObject C))

theorem HomotopicalAlgebra.CofibrantObject.HoCat.exists_resolution {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] (X : C) : ∃ (X' : C) (_ : IsCofibrant X') (p : X' ⟶ X), Fibration p ∧ WeakEquivalence p

noncomputable def HomotopicalAlgebra.CofibrantObject.HoCat.resolutionObj {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] (X : C) : C

Given X : C, this is a cofibrant object X' equipped with a trivial fibration X' ⟶ X (see HoCat.pResolutionObj).

Equations

• HomotopicalAlgebra.CofibrantObject.HoCat.resolutionObj X = ⋯.choose

instance HomotopicalAlgebra.CofibrantObject.instIsCofibrantResolutionObj {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] (X : C) : IsCofibrant (HoCat.resolutionObj X)

noncomputable def HomotopicalAlgebra.CofibrantObject.HoCat.pResolutionObj {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] (X : C) : resolutionObj X ⟶ X

This is a trivial fibration resolutionObj X ⟶ X where resolutionObj X is a choice of a cofibrant resolution of X.

Equations

• HomotopicalAlgebra.CofibrantObject.HoCat.pResolutionObj X = ⋯.choose

instance HomotopicalAlgebra.CofibrantObject.instFibrationPResolutionObj {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] (X : C) : Fibration (HoCat.pResolutionObj X)

instance HomotopicalAlgebra.CofibrantObject.instWeakEquivalencePResolutionObj {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] (X : C) : WeakEquivalence (HoCat.pResolutionObj X)

theorem HomotopicalAlgebra.CofibrantObject.HoCat.exists_resolution_map {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : C} (f : X ⟶ Y) : ∃ (g : resolutionObj X ⟶ resolutionObj Y), CategoryTheory.CategoryStruct.comp g (pResolutionObj Y) = CategoryTheory.CategoryStruct.comp (pResolutionObj X) f

noncomputable def HomotopicalAlgebra.CofibrantObject.HoCat.resolutionMap {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : C} (f : X ⟶ Y) : resolutionObj X ⟶ resolutionObj Y

A lifting of a morphism f : X ⟶ Y on cofibrant resolutions. (This is functorial only up to homotopy, see HoCat.resolution.)

Equations

• HomotopicalAlgebra.CofibrantObject.HoCat.resolutionMap f = ⋯.choose

@[simp]

theorem HomotopicalAlgebra.CofibrantObject.HoCat.resolutionMap_fac {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (resolutionMap f) (pResolutionObj Y) = CategoryTheory.CategoryStruct.comp (pResolutionObj X) f

@[simp]

theorem HomotopicalAlgebra.CofibrantObject.HoCat.resolutionMap_fac_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : C} (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (resolutionMap f) (CategoryTheory.CategoryStruct.comp (pResolutionObj Y) h) = CategoryTheory.CategoryStruct.comp (pResolutionObj X) (CategoryTheory.CategoryStruct.comp f h)

@[simp]

theorem HomotopicalAlgebra.CofibrantObject.HoCat.weakEquivalence_resolutionMap_iff {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : C} (f : X ⟶ Y) : WeakEquivalence (resolutionMap f) ↔ WeakEquivalence f

theorem HomotopicalAlgebra.CofibrantObject.HoCat.resolutionObj_hom_ext {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X : C} [IsCofibrant X] {Y : C} {f g : X ⟶ resolutionObj Y} (h : LeftHomotopyRel (CategoryTheory.CategoryStruct.comp f (pResolutionObj Y)) (CategoryTheory.CategoryStruct.comp g (pResolutionObj Y))) : toHoCat.map (homMk f) = toHoCat.map (homMk g)

noncomputable def HomotopicalAlgebra.CofibrantObject.HoCat.resolution {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : CategoryTheory.Functor C (HoCat C)

A cofibrant resolution functor from a model category to the homotopy category of cofibrant objects.

Equations

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

noncomputable def HomotopicalAlgebra.CofibrantObject.HoCat.localizerMorphismResolution (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : CategoryTheory.LocalizerMorphism (weakEquivalences C) (weakEquivalences (HoCat C))

The cofibrant resolution functor HoCat.resolution, as a localizer morphism.

Equations

• HomotopicalAlgebra.CofibrantObject.HoCat.localizerMorphismResolution C = { functor := HomotopicalAlgebra.CofibrantObject.HoCat.resolution, map := ⋯ }

@[simp]

theorem HomotopicalAlgebra.CofibrantObject.HoCat.localizerMorphismResolution_functor (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : (localizerMorphismResolution C).functor = resolution

noncomputable def HomotopicalAlgebra.CofibrantObject.HoCat.ιCompResolutionNatTrans {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : ι.comp resolution ⟶ toHoCat

The map HoCat.pResolutionObj, when applied to already cofibrant objects, gives a natural transformation ι ⋙ HoCat.resolution ⟶ toHoCat.

Equations

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

@[simp]

theorem HomotopicalAlgebra.CofibrantObject.HoCat.ιCompResolutionNatTrans_app {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] (X : CofibrantObject C) : ιCompResolutionNatTrans.app X = toHoCat.map { hom := pResolutionObj (ι.obj X) }

instance HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppιCompResolutionNatTrans {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] (X : CofibrantObject C) : WeakEquivalence (HoCat.ιCompResolutionNatTrans.app X)

instance HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorWhiskerRightHoCatιCompResolutionNatTransOfIsLocalizationWeakEquivalences {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor (HoCat C) D) [L.IsLocalization (weakEquivalences (HoCat C))] : CategoryTheory.IsIso (CategoryTheory.Functor.whiskerRight HoCat.ιCompResolutionNatTrans L)

def HomotopicalAlgebra.CofibrantObject.HoCat.toLocalization {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) [L.IsLocalization (weakEquivalences C)] : CategoryTheory.Functor (HoCat C) D

The induced functor CofibrantObject.HoCat C ⥤ D, when D is a localization of C with respect to weak equivalences.

Equations

• HomotopicalAlgebra.CofibrantObject.HoCat.toLocalization L = CategoryTheory.Quotient.lift (HomotopicalAlgebra.CofibrantObject.homRel C) (HomotopicalAlgebra.CofibrantObject.ι.comp L) ⋯

def HomotopicalAlgebra.CofibrantObject.HoCat.toHoCatCompToLocalizationIso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) [L.IsLocalization (weakEquivalences C)] : toHoCat.comp (toLocalization L) ≅ ι.comp L

The isomorphism toHoCat ⋙ toLocalization L ≅ ι ⋙ L which expresses that if L : C ⥤ D is a localization functor, then its restriction on the full subcategory of cofibrant objects factors through the homotopy category of cofibrant objects.

Equations

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

@[deprecated HomotopicalAlgebra.CofibrantObject.HoCat.toHoCatCompToLocalizationIso (since := "2026-01-31")]

def HomotopicalAlgebra.CofibrantObject.HoCat.toπCompToLocalizationIso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) [L.IsLocalization (weakEquivalences C)] : toHoCat.comp (toLocalization L) ≅ ι.comp L

Alias of HomotopicalAlgebra.CofibrantObject.HoCat.toHoCatCompToLocalizationIso.

---

The isomorphism toHoCat ⋙ toLocalization L ≅ ι ⋙ L which expresses that if L : C ⥤ D is a localization functor, then its restriction on the full subcategory of cofibrant objects factors through the homotopy category of cofibrant objects.

Equations

• @HomotopicalAlgebra.CofibrantObject.HoCat.toπCompToLocalizationIso = @HomotopicalAlgebra.CofibrantObject.HoCat.toHoCatCompToLocalizationIso

noncomputable def HomotopicalAlgebra.CofibrantObject.HoCat.resolutionCompToLocalizationNatTrans {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) [L.IsLocalization (weakEquivalences C)] : resolution.comp (toLocalization L) ⟶ L

The natural isomorphism HoCat.resolution ⋙ HoCat.toLocalization L ⟶ L when L : C ⥤ D is a localization functor.

Equations

• HomotopicalAlgebra.CofibrantObject.HoCat.resolutionCompToLocalizationNatTrans L = { app := fun (X : C) => L.map (HomotopicalAlgebra.CofibrantObject.HoCat.pResolutionObj X), naturality := ⋯ }

instance HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorResolutionCompToLocalizationNatTrans {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) [L.IsLocalization (weakEquivalences C)] : CategoryTheory.IsIso (HoCat.resolutionCompToLocalizationNatTrans L)

def HomotopicalAlgebra.CofibrantObject.localizerMorphism (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : CategoryTheory.LocalizerMorphism (weakEquivalences (CofibrantObject C)) (weakEquivalences C)

The inclusion CofibrantObject C ⥤ C, as a localizer morphism.

Equations

• HomotopicalAlgebra.CofibrantObject.localizerMorphism C = { functor := HomotopicalAlgebra.CofibrantObject.ι, map := ⋯ }

@[simp]

theorem HomotopicalAlgebra.CofibrantObject.localizerMorphism_functor (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : (localizerMorphism C).functor = ι

instance HomotopicalAlgebra.CofibrantObject.instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : (localizerMorphism C).IsLocalizedEquivalence

instance HomotopicalAlgebra.CofibrantObject.instIsCofibrantObjFunctorWeakEquivalencesLocalizerMorphism {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] (X : CofibrantObject C) : IsCofibrant ((localizerMorphism C).functor.obj X)

instance HomotopicalAlgebra.CofibrantObject.instIsLocalizationCompιWeakEquivalences {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) [L.IsLocalization (weakEquivalences C)] : (ι.comp L).IsLocalization (weakEquivalences (CofibrantObject C))