The fundamental lemma of homotopical algebra

Let C be a model category. Let L : C ⥤ H be a localization functor with respect to weak equivalences in C. We obtain the fundamental lemma of homotopical algebra: if X is cofibrant and Y fibrant, the map (X ⟶ Y) → (L.obj X ⟶ L.obj Y) identifies L.obj X ⟶ L.obj Y to the quotient of X ⟶ Y by the homotopy relation (in this case, the left and right homotopy relations coincide).

References

• Daniel G. Quillen, Homotopical algebra, I.1

def HomotopicalAlgebra.leftHomotopyClassToHom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {H : Type u_2} [CategoryTheory.Category.{v_2, u_2} H] (L : CategoryTheory.Functor C H) [L.IsLocalization (weakEquivalences C)] {X Y : C} : LeftHomotopyClass X Y → (L.obj X ⟶ L.obj Y)

The map LeftHomotopyClass X Y → (L.obj X ⟶ L.obj Y) when L is a localization functor with respect to weakEquivalences C.

Equations

• HomotopicalAlgebra.leftHomotopyClassToHom L = Quot.lift L.map ⋯

@[simp]

theorem HomotopicalAlgebra.leftHomotopyClassToHom_mk {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {H : Type u_2} [CategoryTheory.Category.{v_2, u_2} H] (L : CategoryTheory.Functor C H) [L.IsLocalization (weakEquivalences C)] {X Y : C} (f : X ⟶ Y) : leftHomotopyClassToHom L (LeftHomotopyClass.mk f) = L.map f

def HomotopicalAlgebra.rightHomotopyClassToHom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {H : Type u_2} [CategoryTheory.Category.{v_2, u_2} H] (L : CategoryTheory.Functor C H) [L.IsLocalization (weakEquivalences C)] {X Y : C} : RightHomotopyClass X Y → (L.obj X ⟶ L.obj Y)

The map RightHomotopyClass X Y → (L.obj X ⟶ L.obj Y) when L is a localization functor with respect to weakEquivalences C.

Equations

• HomotopicalAlgebra.rightHomotopyClassToHom L = Quot.lift L.map ⋯

@[simp]

theorem HomotopicalAlgebra.rightHomotopyClassToHom_mk {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {H : Type u_2} [CategoryTheory.Category.{v_2, u_2} H] (L : CategoryTheory.Functor C H) [L.IsLocalization (weakEquivalences C)] {X Y : C} (f : X ⟶ Y) : rightHomotopyClassToHom L (RightHomotopyClass.mk f) = L.map f

theorem HomotopicalAlgebra.bijective_leftHomotopyClassToHom_iff_bijective_rightHomotopyClassToHom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {H : Type u_2} [CategoryTheory.Category.{v_2, u_2} H] (L : CategoryTheory.Functor C H) [L.IsLocalization (weakEquivalences C)] (X Y : C) [IsCofibrant X] [IsFibrant Y] : Function.Bijective (leftHomotopyClassToHom L) ↔ Function.Bijective (rightHomotopyClassToHom L)

theorem HomotopicalAlgebra.bijective_rightHomotopyClassToHom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {H : Type u_2} [CategoryTheory.Category.{v_2, u_2} H] (L : CategoryTheory.Functor C H) [L.IsLocalization (weakEquivalences C)] (X Y : C) [IsCofibrant X] [IsFibrant Y] : Function.Bijective (rightHomotopyClassToHom L)

theorem HomotopicalAlgebra.bijective_leftHomotopyClassToHom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {H : Type u_2} [CategoryTheory.Category.{v_2, u_2} H] (L : CategoryTheory.Functor C H) [L.IsLocalization (weakEquivalences C)] (X Y : C) [IsCofibrant X] [IsFibrant Y] : Function.Bijective (leftHomotopyClassToHom L)

theorem HomotopicalAlgebra.map_surjective_of_isLocalization {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {H : Type u_2} [CategoryTheory.Category.{v_2, u_2} H] (L : CategoryTheory.Functor C H) [L.IsLocalization (weakEquivalences C)] (X Y : C) [IsCofibrant X] [IsFibrant Y] : Function.Surjective L.map

theorem HomotopicalAlgebra.RightHomotopyRel.iff_map_eq {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {H : Type u_2} [CategoryTheory.Category.{v_2, u_2} H] (L : CategoryTheory.Functor C H) [L.IsLocalization (weakEquivalences C)] (X Y : C) [IsCofibrant X] [IsFibrant Y] {f g : X ⟶ Y} : RightHomotopyRel f g ↔ L.map f = L.map g

theorem HomotopicalAlgebra.LeftHomotopyRel.iff_map_eq {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [ModelCategory C] {H : Type u_2} [CategoryTheory.Category.{v_2, u_2} H] (L : CategoryTheory.Functor C H) [L.IsLocalization (weakEquivalences C)] (X Y : C) [IsCofibrant X] [IsFibrant Y] {f g : X ⟶ Y} : LeftHomotopyRel f g ↔ L.map f = L.map g