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.

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

The homotopy relation on the category of bifibrant objects.

Equations

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

theorem HomotopicalAlgebra.BifibrantObject.homRel_iff_rightHomotopyRel {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} 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_1} [CategoryTheory.Category.{v_1, u_1} 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_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : CategoryTheory.HomRel.IsStableUnderPostcomp (homRel C)

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

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

@[reducible, inline]

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

The homotopy category of bifibrant objects.

Equations

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

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

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

Equations

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

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

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

theorem HomotopicalAlgebra.BifibrantObject.toHoCat_map_eq {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} 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_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {X Y : BifibrantObject C} (f g : X ⟶ Y) : toHoCat.map f = toHoCat.map g ↔ homRel C f g

theorem HomotopicalAlgebra.BifibrantObject.inverts_iff_factors {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} 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_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} 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.

Equations

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

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

instance HomotopicalAlgebra.BifibrantObject.instIsIsoHoCatMapToHoCatOfWeakEquivalence {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} 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_1} [CategoryTheory.Category.{v_1, u_1} 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.

Equations

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

@[simp]

theorem HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRight_apply {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} 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_1} [CategoryTheory.Category.{v_1, u_1} 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_1} [CategoryTheory.Category.{v_1, u_1} 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.

Equations

• HomotopicalAlgebra.BifibrantObject.HoCat.homEquivLeft = HomotopicalAlgebra.leftHomotopyClassEquivRightHomotopyClass.trans HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRight

@[simp]

theorem HomotopicalAlgebra.BifibrantObject.HoCat.homEquivLeft_apply {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} 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_1} [CategoryTheory.Category.{v_1, u_1} 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_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : CategoryTheory.Functor (HoCat C) (FibrantObject.HoCat C)

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

Equations

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

@[simp]

theorem HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject_obj {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} 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_1} [CategoryTheory.Category.{v_1, u_1} 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_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : toHoCat.comp HoCat.ιFibrantObject ≅ ιFibrantObject.comp FibrantObject.toHoCat

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

Equations

• HomotopicalAlgebra.BifibrantObject.toHoCatCompιFibrantObject = CategoryTheory.Iso.refl (HomotopicalAlgebra.BifibrantObject.toHoCat.comp HomotopicalAlgebra.BifibrantObject.HoCat.ιFibrantObject)

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

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

Equations

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

@[simp]

theorem HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject_obj {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} 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_1} [CategoryTheory.Category.{v_1, u_1} 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_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : toHoCat.comp HoCat.ιCofibrantObject ≅ ιCofibrantObject.comp CofibrantObject.toHoCat

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

Equations

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

theorem HomotopicalAlgebra.CofibrantObject.exists_bifibrant {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} 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_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] (X : CofibrantObject C) : BifibrantObject C

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

Equations

• X.bifibrantResolutionObj = ⋯.choose

noncomputable def HomotopicalAlgebra.CofibrantObject.iBifibrantResolutionObj {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} 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.

Equations

• X.iBifibrantResolutionObj = ⋯.choose

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

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

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

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

theorem HomotopicalAlgebra.CofibrantObject.exists_bifibrant_map {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} 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_1} [CategoryTheory.Category.{v_1, u_1} 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.

Equations

• HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap f = ⋯.choose

@[simp]

theorem HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} 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_1} [CategoryTheory.Category.{v_1, u_1} 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 f (CategoryTheory.CategoryStruct.comp X₂.iBifibrantResolutionObj h)

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

@[simp]

theorem HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap_fac' {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} 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_1} [CategoryTheory.Category.{v_1, u_1} 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 (toHoCat.map f) (CategoryTheory.CategoryStruct.comp (toHoCat.map X₂.iBifibrantResolutionObj) h)

theorem HomotopicalAlgebra.CofibrantObject.bifibrantResolutionObj_hom_ext {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} 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_1} [CategoryTheory.Category.{v_1, u_1} 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.

Equations

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

@[simp]

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

@[simp]

theorem HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution'_map {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} 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_1} [CategoryTheory.Category.{v_1, u_1} 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.

Equations

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

@[simp]

theorem HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution_obj {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} 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_1} [CategoryTheory.Category.{v_1, u_1} 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_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : CategoryTheory.Functor.id (HoCat C) ⟶ bifibrantResolution.comp BifibrantObject.HoCat.ιCofibrantObject

Auxiliary definition for CofibrantObject.HoCat.adj.

Equations

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

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

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

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

Auxiliary definition for CofibrantObject.HoCat.adj.

Equations

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

theorem HomotopicalAlgebra.CofibrantObject.HoCat.adjCounit'_app {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} 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_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] (X : BifibrantObject.HoCat C) : CategoryTheory.IsIso (HoCat.adjCounit'.app X)

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

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

Auxiliary definition for CofibrantObject.HoCat.adj.

Equations

• HomotopicalAlgebra.CofibrantObject.HoCat.adjCounitIso = (CategoryTheory.asIso HomotopicalAlgebra.CofibrantObject.HoCat.adjCounit').symm

theorem HomotopicalAlgebra.CofibrantObject.HoCat.adjCounitIso_inv_app {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} 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_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] : bifibrantResolution ⊣ BifibrantObject.HoCat.ιCofibrantObject

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

Equations

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

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

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

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

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

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