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.