Homotopies in model categories

In this file, we relate left and right homotopies between morphisms X ⟶ Y in model categories. In particular, if X is cofibrant and Y is fibrant, these notions coincide (for arbitrary choices of good cylinders or good path objects).

Using the factorization lemma by K. S. Brown, we deduce versions of the Whitehead theorem (LeftHomotopyClass.whitehead and RightHomotopyClass.whitehead) which assert that when both X and Y are fibrant and cofibrant, then any weak equivalence X ⟶ Y is a homotopy equivalence.

References

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

noncomputable def HomotopicalAlgebra.LeftHomotopyRel.rightHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X Y : C} {f g : X ⟶ Y} [IsCofibrant X] (h : LeftHomotopyRel f g) (Q : PathObject Y) [Q.IsGood] : Q.RightHomotopy f g

When two morphisms X ⟶ Y with X cofibrant are related by a left homotopy, this is a choice of a right homotopy relative to any good path object for Y.

Equations

• h.rightHomotopy Q = { h := CategoryTheory.CategoryStruct.comp ⋯.choose.i₁ ⋯.lift, h₀ := ⋯, h₁ := ⋯ }

theorem HomotopicalAlgebra.LeftHomotopyRel.rightHomotopyRel {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X Y : C} {f g : X ⟶ Y} [IsCofibrant X] (h : LeftHomotopyRel f g) : RightHomotopyRel f g

noncomputable def HomotopicalAlgebra.RightHomotopyRel.leftHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X Y : C} {f g : X ⟶ Y} [IsFibrant Y] (h : RightHomotopyRel f g) (Q : Cylinder X) [Q.IsGood] : Q.LeftHomotopy f g

When two morphisms X ⟶ Y with Y fibrant are related by a right homotopy, this is a choice of a left homotopy relative to any good cylinder object for X.

Equations

• h.leftHomotopy Q = { h := CategoryTheory.CategoryStruct.comp ⋯.lift ⋯.choose.p₁, h₀ := ⋯, h₁ := ⋯ }

theorem HomotopicalAlgebra.RightHomotopyRel.leftHomotopyRel {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X Y : C} {f g : X ⟶ Y} [IsFibrant Y] (h : RightHomotopyRel f g) : LeftHomotopyRel f g

theorem HomotopicalAlgebra.leftHomotopyRel_iff_rightHomotopyRel {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X Y : C} (f g : X ⟶ Y) [IsCofibrant X] [IsFibrant Y] : LeftHomotopyRel f g ↔ RightHomotopyRel f g

theorem HomotopicalAlgebra.LeftHomotopyClass.postcomp_bijective_of_fibration_of_weakEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] (X : C) {Y Z : C} [IsCofibrant X] (g : Y ⟶ Z) [Fibration g] [WeakEquivalence g] : Function.Bijective fun (f : LeftHomotopyClass X Y) => f.postcomp g

theorem HomotopicalAlgebra.LeftHomotopyClass.postcomp_bijective_of_weakEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] (X : C) {Y Z : C} [IsCofibrant X] (g : Y ⟶ Z) [IsFibrant Y] [IsFibrant Z] [WeakEquivalence g] : Function.Bijective fun (f : LeftHomotopyClass X Y) => f.postcomp g

theorem HomotopicalAlgebra.RightHomotopyClass.precomp_bijective_of_cofibration_of_weakEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X Y : C} (Z : C) [IsFibrant Z] (f : X ⟶ Y) [Cofibration f] [WeakEquivalence f] : Function.Bijective fun (g : RightHomotopyClass Y Z) => g.precomp f

theorem HomotopicalAlgebra.RightHomotopyClass.precomp_bijective_of_weakEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X Y : C} (Z : C) [IsFibrant Z] (f : X ⟶ Y) [IsCofibrant X] [IsCofibrant Y] [WeakEquivalence f] : Function.Bijective fun (g : RightHomotopyClass Y Z) => g.precomp f

theorem HomotopicalAlgebra.RightHomotopyClass.whitehead {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X Y : C} [IsCofibrant X] [IsCofibrant Y] [IsFibrant X] [IsFibrant Y] (f : X ⟶ Y) [WeakEquivalence f] : ∃ (g : Y ⟶ X), RightHomotopyRel (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id X) ∧ RightHomotopyRel (CategoryTheory.CategoryStruct.comp g f) (CategoryTheory.CategoryStruct.id Y)

theorem HomotopicalAlgebra.LeftHomotopyClass.whitehead {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X Y : C} [IsCofibrant X] [IsCofibrant Y] [IsFibrant X] [IsFibrant Y] (f : X ⟶ Y) [WeakEquivalence f] : ∃ (g : Y ⟶ X), LeftHomotopyRel (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id X) ∧ LeftHomotopyRel (CategoryTheory.CategoryStruct.comp g f) (CategoryTheory.CategoryStruct.id Y)

def HomotopicalAlgebra.leftHomotopyClassEquivRightHomotopyClass {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X Y : C} [IsCofibrant X] [IsFibrant Y] : LeftHomotopyClass X Y ≃ RightHomotopyClass X Y

Left homotopy classes of maps X ⟶ Y identify to right homotopy classes when X is cofibrant and Y is fibrant.

Equations

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

@[simp]

theorem HomotopicalAlgebra.leftHomotopyClassEquivRightHomotopyClass_mk {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X Y : C} [IsCofibrant X] [IsFibrant Y] (f : X ⟶ Y) : leftHomotopyClassEquivRightHomotopyClass (LeftHomotopyClass.mk f) = RightHomotopyClass.mk f

@[simp]

theorem HomotopicalAlgebra.leftHomotopyClassEquivRightHomotopyClass_symm_mk {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {X Y : C} [IsCofibrant X] [IsFibrant Y] (f : X ⟶ Y) : leftHomotopyClassEquivRightHomotopyClass.symm (RightHomotopyClass.mk f) = LeftHomotopyClass.mk f