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.

Equations

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

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.

Equations

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

@[implicit_reducible]

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.

Equations

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

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.

Equations

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

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.

Equations

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

@[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.

Equations

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

@[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.

Equations

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

@[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.

Equations

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

@[implicit_reducible]

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.

Equations

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

@[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.

Equations

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

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.

Equations

• X.bifibrantResolutionObj = ⋯.choose

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.

Equations

• X.iBifibrantResolutionObj = ⋯.choose

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.

Equations

• HomotopicalAlgebra.CofibrantObject.bifibrantResolutionMap f = ⋯.choose

@[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 f (CategoryTheory.CategoryStruct.comp 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 (toHoCat.map f) (CategoryTheory.CategoryStruct.comp (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

@[implicit_reducible]

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.

Equations

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

@[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)

@[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

@[implicit_reducible]

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.

Equations

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

@[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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

@[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.

Equations

• HomotopicalAlgebra.BifibrantObject.ιFibrantObjectLocalizerMorphism C = { functor := HomotopicalAlgebra.BifibrantObject.ιFibrantObject, map := ⋯ }

@[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