The homotopy category of bifibrant objects

We construct the homotopy category BifibrantObject.HoCat C of bifibrant objects in a model category C and show that the functor BifibrantObject.toHoCat : BifibrantObject C ⥤ BifibrantObject.HoCat C is a localization functor with respect to weak equivalences. We also show that certain localizer morphisms are localized weak equivalences, which can be understood by saying that we obtain the same localized category (up to equivalence) by inverting weak equivalences in C, CofibrantObject C, FibrantObject C or BifibrantObject C.

def HomotopicalAlgebra.BifibrantObject.homRel (C : Type u) [CategoryTheory.Category.{v, u} C] [ModelCategory C] : HomRel (BifibrantObject C)

The homotopy relation on the category of bifibrant objects.

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

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

instance HomotopicalAlgebra.BifibrantObject.instIsStableUnderPostcompHomRel {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] : CategoryTheory.HomRel.IsStableUnderPostcomp (homRel C)

instance HomotopicalAlgebra.BifibrantObject.instIsStableUnderPrecompHomRel {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] : CategoryTheory.HomRel.IsStableUnderPrecomp (homRel C)

instance HomotopicalAlgebra.BifibrantObject.instCongruenceHomRel {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] : CategoryTheory.Congruence (homRel C)

@[reducible, inline]

abbrev HomotopicalAlgebra.BifibrantObject.HoCat (C : Type u) [CategoryTheory.Category.{v, u} C] [ModelCategory C] : Type u

The homotopy category of bifibrant objects.

def HomotopicalAlgebra.BifibrantObject.toHoCat {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] : CategoryTheory.Functor (BifibrantObject C) (HoCat C)

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

theorem HomotopicalAlgebra.BifibrantObject.toHoCat_obj_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] : Function.Surjective toHoCat.obj

instance HomotopicalAlgebra.BifibrantObject.instFullHoCatToHoCat {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] : toHoCat.Full

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

theorem HomotopicalAlgebra.BifibrantObject.toHoCat_map_eq_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X Y : BifibrantObject C} (f g : X ⟶ Y) : toHoCat.map f = toHoCat.map g ↔ homRel C f g

instance HomotopicalAlgebra.BifibrantObject.instLocallySmallHoCat {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] [CategoryTheory.LocallySmall.{w, v, u} C] : CategoryTheory.LocallySmall.{w, v, u} (HoCat C)

theorem HomotopicalAlgebra.BifibrantObject.inverts_iff_factors {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor (BifibrantObject C) D) : (weakEquivalences (BifibrantObject C)).IsInvertedBy F ↔ ∀ ⦃K L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g

def HomotopicalAlgebra.BifibrantObject.strictUniversalPropertyFixedTargetToHoCat {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget toHoCat (weakEquivalences (BifibrantObject C)) D

The strict universal property of the localization with respect to weak equivalences for the quotient functor toHoCat : BifibrantObject C ⥤ BifibrantObject.HoCat C.

instance HomotopicalAlgebra.BifibrantObject.instIsLocalizationHoCatToHoCatWeakEquivalences {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] : toHoCat.IsLocalization (weakEquivalences (BifibrantObject C))

instance HomotopicalAlgebra.BifibrantObject.instIsIsoHoCatMapToHoCatOfWeakEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X Y : BifibrantObject C} (f : X ⟶ Y) [hf : WeakEquivalence f] : CategoryTheory.IsIso (toHoCat.map f)

def HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRight {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X Y : C} [IsCofibrant X] [IsCofibrant Y] [IsFibrant X] [IsFibrant Y] : RightHomotopyClass X Y ≃ (toHoCat.obj (mk X) ⟶ toHoCat.obj (mk Y))

Right homotopy classes of maps between bifibrant objects identify to morphisms in the homotopy category BifibrantObject.HoCat.

@[simp]

theorem HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRight_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X Y : C} [IsCofibrant X] [IsCofibrant Y] [IsFibrant X] [IsFibrant Y] (f : X ⟶ Y) : homEquivRight (RightHomotopyClass.mk f) = toHoCat.map (homMk f)

@[simp]

theorem HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRight_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X Y : C} [IsCofibrant X] [IsCofibrant Y] [IsFibrant X] [IsFibrant Y] (f : X ⟶ Y) : homEquivRight.symm (toHoCat.map (homMk f)) = RightHomotopyClass.mk f

def HomotopicalAlgebra.BifibrantObject.HoCat.homEquivLeft {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X Y : C} [IsCofibrant X] [IsCofibrant Y] [IsFibrant X] [IsFibrant Y] : LeftHomotopyClass X Y ≃ (toHoCat.obj (mk X) ⟶ toHoCat.obj (mk Y))

Left homotopy classes of maps between bifibrant objects identify to morphisms in the homotopy category BifibrantObject.HoCat.

@[simp]

theorem HomotopicalAlgebra.BifibrantObject.HoCat.homEquivLeft_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X Y : C} [IsCofibrant X] [IsCofibrant Y] [IsFibrant X] [IsFibrant Y] (f : X ⟶ Y) : homEquivLeft (LeftHomotopyClass.mk f) = toHoCat.map (homMk f)

@[simp]

theorem HomotopicalAlgebra.BifibrantObject.HoCat.homEquivLeft_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X Y : C} [IsCofibrant X] [IsCofibrant Y] [IsFibrant X] [IsFibrant Y] (f : X ⟶ Y) : homEquivRight.symm (toHoCat.map (homMk f)) = RightHomotopyClass.mk f

def HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] : CategoryTheory.Functor (HoCat C) (FibrantObject.HoCat C)

The inclusion functor BifibrantObject.HoCat C ⥤ FibrantObject.HoCat C.

@[simp]

theorem HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] (X : BifibrantObject C) : ιFibrantObject.obj (toHoCat.obj X) = FibrantObject.toHoCat.obj (BifibrantObject.ιFibrantObject.obj X)

@[simp]

theorem HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject_map_toHoCat_map {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X Y : BifibrantObject C} (f : X ⟶ Y) : ιFibrantObject.map (toHoCat.map f) = FibrantObject.toHoCat.map (FibrantObject.homMk f.hom)

def HomotopicalAlgebra.BifibrantObject.toHoCatCompιFibrantObject {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] : toHoCat.comp HoCat.ιFibrantObject ≅ ιFibrantObject.comp FibrantObject.toHoCat

The isomorphism toHoCat ⋙ HoCat.ιFibrantObject ≅ ιFibrantObject ⋙ FibrantObject.toHoCat between functors BifibrantObject C ⥤ FibrantObject.HoCat C.

def HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] : CategoryTheory.Functor (HoCat C) (CofibrantObject.HoCat C)

The inclusion functor BifibrantObject.HoCat C ⥤ CofibrantObject.HoCat C.

@[simp]

theorem HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] (X : BifibrantObject C) : ιCofibrantObject.obj (toHoCat.obj X) = CofibrantObject.toHoCat.obj (BifibrantObject.ιCofibrantObject.obj X)

@[simp]

theorem HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject_map_toHoCat_map {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X Y : BifibrantObject C} (f : X ⟶ Y) : ιCofibrantObject.map (toHoCat.map f) = CofibrantObject.toHoCat.map (CofibrantObject.homMk f.hom)

def HomotopicalAlgebra.BifibrantObject.toHoCatCompιCofibrantObject {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] : toHoCat.comp HoCat.ιCofibrantObject ≅ ιCofibrantObject.comp CofibrantObject.toHoCat

The isomorphism toHoCat ⋙ HoCat.ιCofibrantObject ≅ ιCofibrantObject ⋙ CofibrantObject.toHoCat between functors BifibrantObject C ⥤ CofibrantObject.HoCat C.

theorem HomotopicalAlgebra.CofibrantObject.exists_bifibrant {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] (X : CofibrantObject C) : ∃ (Y : BifibrantObject C) (i : X ⟶ BifibrantObject.ιCofibrantObject.obj Y), Cofibration (ι.map i) ∧ WeakEquivalence (ι.map i)

noncomputable def HomotopicalAlgebra.CofibrantObject.bifibrantResolutionObj {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] (X : CofibrantObject C) : BifibrantObject C

Given X : CofibrantObject C, this is a choice of bifibrant resolution of X.

noncomputable def HomotopicalAlgebra.CofibrantObject.iBifibrantResolutionObj {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] (X : CofibrantObject C) : X ⟶ BifibrantObject.ιCofibrantObject.obj X.bifibrantResolutionObj

Given X : CofibrantObject C, this is a trivial cofibration from X to a choice of bifibrant resolution.

instance HomotopicalAlgebra.CofibrantObject.instCofibrationHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] (X : CofibrantObject C) : Cofibration X.iBifibrantResolutionObj.hom

instance HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHomFullSubcategoryCofibrantObjectsIBifibrantResolutionObj {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] (X : CofibrantObject C) : WeakEquivalence X.iBifibrantResolutionObj.hom

instance HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceIBifibrantResolutionObj {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] (X : CofibrantObject C) : WeakEquivalence X.iBifibrantResolutionObj

instance HomotopicalAlgebra.CofibrantObject.instIsFibrantObjιBifibrantObjectιCofibrantObject {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] (X : BifibrantObject C) : IsFibrant (ι.obj (BifibrantObject.ιCofibrantObject.obj X))

theorem HomotopicalAlgebra.CofibrantObject.exists_bifibrant_map {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X₁ X₂ : CofibrantObject C} (f : X₁ ⟶ X₂) : ∃ (g : X₁.bifibrantResolutionObj ⟶ X₂.bifibrantResolutionObj), CategoryTheory.CategoryStruct.comp X₁.iBifibrantResolutionObj (BifibrantObject.ιCofibrantObject.map g) = CategoryTheory.CategoryStruct.comp f X₂.iBifibrantResolutionObj

noncomputable def HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X₁ X₂ : CofibrantObject C} (f : X₁ ⟶ X₂) : X₁.bifibrantResolutionObj ⟶ X₂.bifibrantResolutionObj

Given a morphism in CofibrantObject C, this is a choice of morphism (well defined only up to homotopy) between the chosen bifibrant resolutions.

@[simp]

theorem HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X₁ X₂ : CofibrantObject C} (f : X₁ ⟶ X₂) : CategoryTheory.CategoryStruct.comp X₁.iBifibrantResolutionObj (homMk (bifibrantResolutionMap f).hom) = CategoryTheory.CategoryStruct.comp f X₂.iBifibrantResolutionObj

@[simp]

theorem HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X₁ X₂ : CofibrantObject C} (f : X₁ ⟶ X₂) {Z : CofibrantObject C} (h : mk X₂.bifibrantResolutionObj.obj ⟶ Z) : CategoryTheory.CategoryStruct.comp X₁.iBifibrantResolutionObj (CategoryTheory.CategoryStruct.comp (homMk (bifibrantResolutionMap f).hom) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f X₂.iBifibrantResolutionObj) h

instance HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceBifibrantObjectBifibrantResolutionMap {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X₁ X₂ : CofibrantObject C} (f : X₁ ⟶ X₂) [WeakEquivalence f] : WeakEquivalence (bifibrantResolutionMap f)

@[simp]

theorem HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac' {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X₁ X₂ : CofibrantObject C} (f : X₁ ⟶ X₂) : CategoryTheory.CategoryStruct.comp (toHoCat.map X₁.iBifibrantResolutionObj) (toHoCat.map (homMk (bifibrantResolutionMap f).hom)) = CategoryTheory.CategoryStruct.comp (toHoCat.map f) (toHoCat.map X₂.iBifibrantResolutionObj)

@[simp]

theorem HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X₁ X₂ : CofibrantObject C} (f : X₁ ⟶ X₂) {Z : HoCat C} (h : toHoCat.obj (mk X₂.bifibrantResolutionObj.obj) ⟶ Z) : CategoryTheory.CategoryStruct.comp (toHoCat.map X₁.iBifibrantResolutionObj) (CategoryTheory.CategoryStruct.comp (toHoCat.map (homMk (bifibrantResolutionMap f).hom)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (toHoCat.map f) (toHoCat.map X₂.iBifibrantResolutionObj)) h

theorem HomotopicalAlgebra.CofibrantObject.bifibrantResolutionObj_hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X : CofibrantObject C} {Y : BifibrantObject.HoCat C} {f g : BifibrantObject.toHoCat.obj X.bifibrantResolutionObj ⟶ Y} (h : CategoryTheory.CategoryStruct.comp (toHoCat.map X.iBifibrantResolutionObj) (BifibrantObject.HoCat.ιCofibrantObject.map f) = CategoryTheory.CategoryStruct.comp (toHoCat.map X.iBifibrantResolutionObj) (BifibrantObject.HoCat.ιCofibrantObject.map g)) : f = g

noncomputable def HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution' {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] : CategoryTheory.Functor (CofibrantObject C) (BifibrantObject.HoCat C)

The bifibrant resolution functor from the category of cofibrant objects to the homotopy category of bifibrant objects.

@[simp]

theorem HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution'_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] (X : CofibrantObject C) : bifibrantResolution'.obj X = BifibrantObject.toHoCat.obj X.bifibrantResolutionObj

@[simp]

theorem HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution'_map {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X✝ Y✝ : CofibrantObject C} (f : X✝ ⟶ Y✝) : bifibrantResolution'.map f = BifibrantObject.toHoCat.map (bifibrantResolutionMap f)

noncomputable def HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] : CategoryTheory.Functor (HoCat C) (BifibrantObject.HoCat C)

The bifibrant resolution functor from the homotopy category of cofibrant objects to the homotopy category of bifibrant objects.

@[simp]

theorem HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] (X : CofibrantObject C) : bifibrantResolution.obj (toHoCat.obj X) = BifibrantObject.toHoCat.obj X.bifibrantResolutionObj

@[simp]

theorem HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution_map {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X Y : CofibrantObject C} (f : X ⟶ Y) : bifibrantResolution.map (toHoCat.map f) = BifibrantObject.toHoCat.map (bifibrantResolutionMap f)

noncomputable def HomotopicalAlgebra.CofibrantObject.HoCat.adjUnit {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] : CategoryTheory.Functor.id (HoCat C) ⟶ bifibrantResolution.comp BifibrantObject.HoCat.ιCofibrantObject

Auxiliary definition for CofibrantObject.HoCat.adj.

theorem HomotopicalAlgebra.CofibrantObject.HoCat.adjUnit_app {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] (X : CofibrantObject C) : adjUnit.app (toHoCat.obj X) = toHoCat.map X.iBifibrantResolutionObj

instance HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppAdjUnit {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] (X : HoCat C) : WeakEquivalence (HoCat.adjUnit.app X)

noncomputable def HomotopicalAlgebra.CofibrantObject.HoCat.adjCounit' {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] : CategoryTheory.Functor.id (BifibrantObject.HoCat C) ⟶ BifibrantObject.HoCat.ιCofibrantObject.comp bifibrantResolution

Auxiliary definition for CofibrantObject.HoCat.adj.

theorem HomotopicalAlgebra.CofibrantObject.HoCat.adjCounit'_app {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] (X : BifibrantObject C) : adjCounit'.app (BifibrantObject.toHoCat.obj X) = BifibrantObject.toHoCat.map (BifibrantObject.homMk (mk X.obj).iBifibrantResolutionObj.hom)

instance HomotopicalAlgebra.CofibrantObject.instIsIsoHoCatAppAdjCounit' {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] (X : BifibrantObject.HoCat C) : CategoryTheory.IsIso (HoCat.adjCounit'.app X)

instance HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorHoCatAdjCounit' {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] : CategoryTheory.IsIso HoCat.adjCounit'

noncomputable def HomotopicalAlgebra.CofibrantObject.HoCat.adjCounitIso {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] : BifibrantObject.HoCat.ιCofibrantObject.comp bifibrantResolution ≅ CategoryTheory.Functor.id (BifibrantObject.HoCat C)

Auxiliary definition for CofibrantObject.HoCat.adj.

theorem HomotopicalAlgebra.CofibrantObject.HoCat.adjCounitIso_inv_app {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] (X : BifibrantObject C) : adjCounitIso.inv.app (BifibrantObject.toHoCat.obj X) = BifibrantObject.toHoCat.map (BifibrantObject.homMk (mk X.obj).iBifibrantResolutionObj.hom)

noncomputable def HomotopicalAlgebra.CofibrantObject.HoCat.adj {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] : bifibrantResolution ⊣ BifibrantObject.HoCat.ιCofibrantObject

The adjunction between the category CofibrantObject.HoCat C and BifibrantObject.HoCat C.

instance HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorHoCatCounitHoCatAdj {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] : CategoryTheory.IsIso HoCat.adj.counit

instance HomotopicalAlgebra.CofibrantObject.instFullHoCatHoCatιCofibrantObject {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] : BifibrantObject.HoCat.ιCofibrantObject.Full

instance HomotopicalAlgebra.CofibrantObject.instFaithfulHoCatHoCatιCofibrantObject {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] : BifibrantObject.HoCat.ιCofibrantObject.Faithful

instance HomotopicalAlgebra.CofibrantObject.instWeakEquivalenceHoCatAppUnitHoCatAdj {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] (X : HoCat C) : WeakEquivalence (HoCat.adj.unit.app X)

instance HomotopicalAlgebra.CofibrantObject.instIsLocalizationHoCatHoCatBifibrantResolutionWeakEquivalences {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] : HoCat.bifibrantResolution.IsLocalization (weakEquivalences (HoCat C))

def HomotopicalAlgebra.BifibrantObject.localizerMorphism (C : Type u) [CategoryTheory.Category.{v, u} C] [ModelCategory C] : CategoryTheory.LocalizerMorphism (weakEquivalences (BifibrantObject C)) (weakEquivalences C)

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

def HomotopicalAlgebra.BifibrantObject.ιCofibrantObjectLocalizerMorphism (C : Type u) [CategoryTheory.Category.{v, u} C] [ModelCategory C] : CategoryTheory.LocalizerMorphism (weakEquivalences (BifibrantObject C)) (weakEquivalences (CofibrantObject C))

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

@[simp]

theorem HomotopicalAlgebra.BifibrantObject.ιCofibrantObjectLocalizerMorphism_functor (C : Type u) [CategoryTheory.Category.{v, u} C] [ModelCategory C] : (ιCofibrantObjectLocalizerMorphism C).functor = ιCofibrantObject

def HomotopicalAlgebra.BifibrantObject.ιFibrantObjectLocalizerMorphism (C : Type u) [CategoryTheory.Category.{v, u} C] [ModelCategory C] : CategoryTheory.LocalizerMorphism (weakEquivalences (BifibrantObject C)) (weakEquivalences (FibrantObject C))

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

@[simp]

theorem HomotopicalAlgebra.BifibrantObject.ιFibrantObjectLocalizerMorphism_functor (C : Type u) [CategoryTheory.Category.{v, u} C] [ModelCategory C] : (ιFibrantObjectLocalizerMorphism C).functor = ιFibrantObject

instance HomotopicalAlgebra.BifibrantObject.instIsLocalizedEquivalenceCofibrantObjectWeakEquivalencesιCofibrantObjectLocalizerMorphism {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] : (ιCofibrantObjectLocalizerMorphism C).IsLocalizedEquivalence

instance HomotopicalAlgebra.BifibrantObject.instIsLocalizationCompCofibrantObjectιCofibrantObjectWeakEquivalences {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (L : CategoryTheory.Functor (CofibrantObject C) D) [L.IsLocalization (weakEquivalences (CofibrantObject C))] : (ιCofibrantObject.comp L).IsLocalization (weakEquivalences (BifibrantObject C))

instance HomotopicalAlgebra.BifibrantObject.instIsLocalizedEquivalenceWeakEquivalencesLocalizerMorphism {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] : (localizerMorphism C).IsLocalizedEquivalence

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

instance HomotopicalAlgebra.BifibrantObject.instIsLocalizedEquivalenceFibrantObjectWeakEquivalencesιFibrantObjectLocalizerMorphism {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] : (ιFibrantObjectLocalizerMorphism C).IsLocalizedEquivalence

instance HomotopicalAlgebra.BifibrantObject.instIsLocalizationCompFibrantObjectιFibrantObjectWeakEquivalences {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] (L : CategoryTheory.Functor (FibrantObject C) D) [L.IsLocalization (weakEquivalences (FibrantObject C))] : (ιFibrantObject.comp L).IsLocalization (weakEquivalences (BifibrantObject C))

theorem HomotopicalAlgebra.locallySmall_of_isLocalization {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (L : CategoryTheory.Functor C D) [L.IsLocalization (weakEquivalences C)] [CategoryTheory.LocallySmall.{w, v, u} C] : CategoryTheory.LocallySmall.{w, v_1, u_1} D