The homotopy category of fibrant objects

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

This file was obtained by dualizing the definitions in Mathlib/AlgebraicTopology/ModelCategory/CofibrantObjectHomotopy.lean.

References

• [Daniel G. Quillen, Homotopical algebra][Quillen1967]

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

The left homotopy relation on the category of fibrant objects.

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

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

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

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

@[reducible, inline]

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

The homotopy category of fibrant objects.

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

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

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

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

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

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

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

@[implicit_reducible]

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

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

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

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

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

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

instance HomotopicalAlgebra.FibrantObject.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 (FibrantObject C))

theorem HomotopicalAlgebra.FibrantObject.HoCat.exists_resolution {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] (X : C) : ∃ (X' : C) (_ : IsFibrant X') (i : X ⟶ X'), Cofibration i ∧ WeakEquivalence i

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

Given X : C, this is a fibrant object X' equipped with a trivial cofibration X ⟶ X' (see HoCat.iResolutionObj).

instance HomotopicalAlgebra.FibrantObject.instIsFibrantResolutionObj {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] (X : C) : IsFibrant (HoCat.resolutionObj X)

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

This is a trivial cofibration X ⟶ resolutionObj X where resolutionObj X is a choice of a fibrant resolution of X.

instance HomotopicalAlgebra.FibrantObject.instCofibrationIResolutionObj {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] (X : C) : Cofibration (HoCat.iResolutionObj X)

instance HomotopicalAlgebra.FibrantObject.instWeakEquivalenceIResolutionObj {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] (X : C) : WeakEquivalence (HoCat.iResolutionObj X)

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

theorem HomotopicalAlgebra.FibrantObject.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 (iResolutionObj X) g = CategoryTheory.CategoryStruct.comp f (iResolutionObj Y)

noncomputable def HomotopicalAlgebra.FibrantObject.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 fibrant resolutions. (This is functorial only up to homotopy, see HoCat.resolution.)

@[simp]

theorem HomotopicalAlgebra.FibrantObject.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 (iResolutionObj X) (resolutionMap f) = CategoryTheory.CategoryStruct.comp f (iResolutionObj Y)

@[simp]

theorem HomotopicalAlgebra.FibrantObject.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 : resolutionObj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (iResolutionObj X) (CategoryTheory.CategoryStruct.comp (resolutionMap f) h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (iResolutionObj Y) h)

@[simp]

theorem HomotopicalAlgebra.FibrantObject.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.FibrantObject.HoCat.resolutionObj_hom_ext {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : C} [IsFibrant Y] {f g : resolutionObj X ⟶ Y} (h : RightHomotopyRel (CategoryTheory.CategoryStruct.comp (iResolutionObj X) f) (CategoryTheory.CategoryStruct.comp (iResolutionObj X) g)) : toHoCat.map (homMk f) = toHoCat.map (homMk g)

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

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

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

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

@[simp]

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

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

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

@[simp]

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

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

instance HomotopicalAlgebra.FibrantObject.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.FibrantObject.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 FibrantObject.HoCat C ⥤ D, when D is a localization of C with respect to weak equivalences.

def HomotopicalAlgebra.FibrantObject.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 fibrant objects factors through the homotopy category of fibrant objects.

noncomputable def HomotopicalAlgebra.FibrantObject.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)] : L ⟶ resolution.comp (toLocalization L)

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

instance HomotopicalAlgebra.FibrantObject.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.FibrantObject.localizerMorphism (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : CategoryTheory.LocalizerMorphism (weakEquivalences (FibrantObject C)) (weakEquivalences C)

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

@[simp]

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

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

instance HomotopicalAlgebra.FibrantObject.instIsFibrantObjFunctorWeakEquivalencesLocalizerMorphism {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] (X : FibrantObject C) : IsFibrant ((localizerMorphism C).functor.obj X)

instance HomotopicalAlgebra.FibrantObject.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 (FibrantObject C))