Left homotopies in model categories

We introduce the types Precylinder.LeftHomotopy and Cylinder.LeftHomotopy of homotopies between morphisms X ⟶ Y relative to a (pre)cylinder of X. Given two morphisms f and g, we introduce the relation LeftHomotopyRel f g asserting the existence of a cylinder object P and a left homotopy P.LeftHomotopy f g, and we define the quotient type LeftHomotopyClass X Y. We show that if X is a cofibrant object in a model category, then LeftHomotopyRel is an equivalence relation on X ⟶ Y.

References

• [Daniel G. Quillen, Homotopical algebra, section I.1][Quillen1967]

structure HomotopicalAlgebra.Precylinder.LeftHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (P : Precylinder X) {Y : C} (f g : X ⟶ Y) : Type v

Given a precylinder P for X, two maps f and g in X ⟶ Y are homotopic relative to P when there is a morphism h : P.I ⟶ Y such that P.i₀ ≫ h = f and P.i₁ ≫ h = g.

• h : P.I ⟶ Y

  a morphism from the (pre)cylinder object to the target

• h₀ : CategoryTheory.CategoryStruct.comp P.i₀ self.h = f
• h₁ : CategoryTheory.CategoryStruct.comp P.i₁ self.h = g

@[simp]

theorem HomotopicalAlgebra.Precylinder.LeftHomotopy.h₁_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {P : Precylinder X} {Y : C} {f g : X ⟶ Y} (self : P.LeftHomotopy f g) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp P.i₁ (CategoryTheory.CategoryStruct.comp self.h h) = CategoryTheory.CategoryStruct.comp g h

@[simp]

theorem HomotopicalAlgebra.Precylinder.LeftHomotopy.h₀_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {P : Precylinder X} {Y : C} {f g : X ⟶ Y} (self : P.LeftHomotopy f g) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp P.i₀ (CategoryTheory.CategoryStruct.comp self.h h) = CategoryTheory.CategoryStruct.comp f h

def HomotopicalAlgebra.Precylinder.LeftHomotopy.refl {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (P : Precylinder X) {Y : C} (f : X ⟶ Y) : P.LeftHomotopy f f

f : X ⟶ Y is left homotopic to itself relative to any precylinder.

Equations

• HomotopicalAlgebra.Precylinder.LeftHomotopy.refl P f = { h := CategoryTheory.CategoryStruct.comp P.π f, h₀ := ⋯, h₁ := ⋯ }

@[simp]

theorem HomotopicalAlgebra.Precylinder.LeftHomotopy.refl_h {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (P : Precylinder X) {Y : C} (f : X ⟶ Y) : (refl P f).h = CategoryTheory.CategoryStruct.comp P.π f

def HomotopicalAlgebra.Precylinder.LeftHomotopy.symm {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {P : Precylinder X} {Y : C} {f g : X ⟶ Y} (h : P.LeftHomotopy f g) : P.symm.LeftHomotopy g f

If f and g are homotopic relative to a precylinder P, then g and f are homotopic relative to P.symm

Equations

• h.symm = { h := h.h, h₀ := ⋯, h₁ := ⋯ }

@[simp]

theorem HomotopicalAlgebra.Precylinder.LeftHomotopy.symm_h {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {P : Precylinder X} {Y : C} {f g : X ⟶ Y} (h : P.LeftHomotopy f g) : h.symm.h = h.h

noncomputable def HomotopicalAlgebra.Precylinder.LeftHomotopy.trans {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {P : Precylinder X} {Y : C} {f₀ f₁ f₂ : X ⟶ Y} (h : P.LeftHomotopy f₀ f₁) {P' : Precylinder X} (h' : P'.LeftHomotopy f₁ f₂) [CategoryTheory.Limits.HasPushout P.i₁ P'.i₀] : (P.trans P').LeftHomotopy f₀ f₂

If f₀ is homotopic to f₁ relative to a precylinder P, and f₁ is homotopic to f₂ relative to P', then f₀ is homotopic to f₂ relative to P.trans P'.

Equations

• h.trans h' = { h := CategoryTheory.Limits.pushout.desc h.h h'.h ⋯, h₀ := ⋯, h₁ := ⋯ }

@[simp]

theorem HomotopicalAlgebra.Precylinder.LeftHomotopy.trans_h {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {P : Precylinder X} {Y : C} {f₀ f₁ f₂ : X ⟶ Y} (h : P.LeftHomotopy f₀ f₁) {P' : Precylinder X} (h' : P'.LeftHomotopy f₁ f₂) [CategoryTheory.Limits.HasPushout P.i₁ P'.i₀] : (h.trans h').h = CategoryTheory.Limits.pushout.desc h.h h'.h ⋯

def HomotopicalAlgebra.Precylinder.LeftHomotopy.postcomp {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {P : Precylinder X} {Y : C} {f g : X ⟶ Y} (h : P.LeftHomotopy f g) {Z : C} (p : Y ⟶ Z) : P.LeftHomotopy (CategoryTheory.CategoryStruct.comp f p) (CategoryTheory.CategoryStruct.comp g p)

Left homotopies are compatible with postcomposition.

Equations

• h.postcomp p = { h := CategoryTheory.CategoryStruct.comp h.h p, h₀ := ⋯, h₁ := ⋯ }

@[simp]

theorem HomotopicalAlgebra.Precylinder.LeftHomotopy.postcomp_h {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {P : Precylinder X} {Y : C} {f g : X ⟶ Y} (h : P.LeftHomotopy f g) {Z : C} (p : Y ⟶ Z) : (h.postcomp p).h = CategoryTheory.CategoryStruct.comp h.h p

@[reducible, inline]

abbrev HomotopicalAlgebra.Cylinder.LeftHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryWithWeakEquivalences C] (P : Cylinder X) (f g : X ⟶ Y) : Type v

Given a cylinder P for X, two maps f and g in X ⟶ Y are homotopic relative to P when there is a morphism h : P.I ⟶ Y such that P.i₀ ≫ h = f and P.i₁ ≫ h = g.

Equations

• P.LeftHomotopy f g = P.LeftHomotopy f g

@[reducible, inline]

abbrev HomotopicalAlgebra.Cylinder.LeftHomotopy.refl {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryWithWeakEquivalences C] (P : Cylinder X) (f : X ⟶ Y) : P.LeftHomotopy f f

f : X ⟶ Y is left homotopic to itself relative to any cylinder.

Equations

• HomotopicalAlgebra.Cylinder.LeftHomotopy.refl P f = HomotopicalAlgebra.Precylinder.LeftHomotopy.refl P.toPrecylinder f

@[reducible, inline]

abbrev HomotopicalAlgebra.Cylinder.LeftHomotopy.symm {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryWithWeakEquivalences C] {P : Cylinder X} {f g : X ⟶ Y} (h : P.LeftHomotopy f g) : P.symm.LeftHomotopy g f

If f and g are homotopic relative to a cylinder P, then g and f are homotopic relative to P.symm.

Equations

• h.symm = HomotopicalAlgebra.Precylinder.LeftHomotopy.symm h

@[reducible, inline]

abbrev HomotopicalAlgebra.Cylinder.LeftHomotopy.postcomp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryWithWeakEquivalences C] {P : Cylinder X} {f g : X ⟶ Y} (h : P.LeftHomotopy f g) {Z : C} (p : Y ⟶ Z) : P.LeftHomotopy (CategoryTheory.CategoryStruct.comp f p) (CategoryTheory.CategoryStruct.comp g p)

Left homotopies are compatible with postcomposition.

Equations

• h.postcomp p = HomotopicalAlgebra.Precylinder.LeftHomotopy.postcomp h p

theorem HomotopicalAlgebra.Cylinder.LeftHomotopy.weakEquivalence_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryWithWeakEquivalences C] (P : Cylinder X) [(weakEquivalences C).HasTwoOutOfThreeProperty] [(weakEquivalences C).ContainsIdentities] {f₀ f₁ : X ⟶ Y} (h : P.LeftHomotopy f₀ f₁) : WeakEquivalence f₀ ↔ WeakEquivalence f₁

@[reducible, inline]

noncomputable abbrev HomotopicalAlgebra.Cylinder.LeftHomotopy.trans {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [ModelCategory C] {P : Cylinder X} [IsCofibrant X] {f₀ f₁ f₂ : X ⟶ Y} (h : P.LeftHomotopy f₀ f₁) {P' : Cylinder X} [P'.IsGood] (h' : P'.LeftHomotopy f₁ f₂) [CategoryTheory.Limits.HasPushout P.i₁ P'.i₀] : (P.trans P').LeftHomotopy f₀ f₂

If f₀ : X ⟶ Y is homotopic to f₁ relative to a cylinder P, and f₁ is homotopic to f₂ relative to a good cylinder P', then f₀ is homotopic to f₂ relative to the cylinder P.trans P' when X is cofibrant.

Equations

• h.trans h' = HomotopicalAlgebra.Precylinder.LeftHomotopy.trans h h'

theorem HomotopicalAlgebra.Cylinder.LeftHomotopy.exists_good_cylinder {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [ModelCategory C] {P : Cylinder X} {f g : X ⟶ Y} (h : P.LeftHomotopy f g) : ∃ (P' : Cylinder X), P'.IsGood ∧ Nonempty (P'.LeftHomotopy f g)

theorem HomotopicalAlgebra.Cylinder.LeftHomotopy.covering_homotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A E B : C} {P : Cylinder A} {f₀ f₁ : A ⟶ B} [IsCofibrant A] [P.IsGood] (h : P.LeftHomotopy f₀ f₁) (p : E ⟶ B) [Fibration p] (l₀ : A ⟶ E) (hl₀ : CategoryTheory.CategoryStruct.comp l₀ p = f₀ := by cat_disch) : ∃ (l₁ : A ⟶ E) (h' : P.LeftHomotopy l₀ l₁), CategoryTheory.CategoryStruct.comp h'.h p = h.h

The covering homotopy theorem: if p : E ⟶ B is a fibration, l₀ : A ⟶ E is a morphism, if there is a left homotopy h between the composition f₀ := l₀ ≫ p and a morphism f₁ : A ⟶ B, then there exists a morphism l₁ : A ⟶ E and a left homotopy h' from l₀ to l₁ which is compatible with h (in particular, l₁ ≫ p = f₁).

def HomotopicalAlgebra.LeftHomotopyRel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] : HomRel C

The left homotopy relation on morphisms in a category with weak equivalences.

Equations

• HomotopicalAlgebra.LeftHomotopyRel f g = ∃ (P : HomotopicalAlgebra.Cylinder X), Nonempty (P.LeftHomotopy f g)

theorem HomotopicalAlgebra.Cylinder.LeftHomotopy.leftHomotopyRel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] {X Y : C} {f g : X ⟶ Y} {P : Cylinder X} (h : P.LeftHomotopy f g) : LeftHomotopyRel f g

theorem HomotopicalAlgebra.LeftHomotopyRel.factorsThroughLocalization (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] : LeftHomotopyRel.FactorsThroughLocalization (weakEquivalences C)

theorem HomotopicalAlgebra.LeftHomotopyRel.refl {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [ModelCategory C] (f : X ⟶ Y) : LeftHomotopyRel f f

theorem HomotopicalAlgebra.LeftHomotopyRel.postcomp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryWithWeakEquivalences C] {f g : X ⟶ Y} (h : LeftHomotopyRel f g) {Z : C} (p : Y ⟶ Z) : LeftHomotopyRel (CategoryTheory.CategoryStruct.comp f p) (CategoryTheory.CategoryStruct.comp g p)

theorem HomotopicalAlgebra.LeftHomotopyRel.exists_good_cylinder {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [ModelCategory C] {f g : X ⟶ Y} (h : LeftHomotopyRel f g) : ∃ (P : Cylinder X), P.IsGood ∧ Nonempty (P.LeftHomotopy f g)

theorem HomotopicalAlgebra.LeftHomotopyRel.exists_very_good_cylinder {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [ModelCategory C] {f g : X ⟶ Y} [IsFibrant Y] (h : LeftHomotopyRel f g) : ∃ (P : Cylinder X), P.IsVeryGood ∧ Nonempty (P.LeftHomotopy f g)

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

theorem HomotopicalAlgebra.LeftHomotopyRel.trans {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [ModelCategory C] {f₀ f₁ f₂ : X ⟶ Y} [IsCofibrant X] (h : LeftHomotopyRel f₀ f₁) (h' : LeftHomotopyRel f₁ f₂) : LeftHomotopyRel f₀ f₂

theorem HomotopicalAlgebra.LeftHomotopyRel.equivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] (X Y : C) [IsCofibrant X] : Equivalence LeftHomotopyRel

theorem HomotopicalAlgebra.LeftHomotopyRel.precomp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [ModelCategory C] {f g : X ⟶ Y} [IsFibrant Y] (h : LeftHomotopyRel f g) {Z : C} (i : Z ⟶ X) : LeftHomotopyRel (CategoryTheory.CategoryStruct.comp i f) (CategoryTheory.CategoryStruct.comp i g)

def HomotopicalAlgebra.LeftHomotopyClass {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : C) [CategoryWithWeakEquivalences C] : Type v

In a category with weak equivalences, this is the quotient of the type of morphisms X ⟶ Y by the equivalence relation generated by left homotopies.

Equations

• HomotopicalAlgebra.LeftHomotopyClass X Y = Quot HomotopicalAlgebra.LeftHomotopyRel

def HomotopicalAlgebra.LeftHomotopyClass.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryWithWeakEquivalences C] : (X ⟶ Y) → LeftHomotopyClass X Y

Given f : X ⟶ Y, this is the class of f in the quotient LeftHomotopyClass X Y.

Equations

• HomotopicalAlgebra.LeftHomotopyClass.mk = Quot.mk HomotopicalAlgebra.LeftHomotopyRel

theorem HomotopicalAlgebra.LeftHomotopyClass.mk_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryWithWeakEquivalences C] : Function.Surjective mk

theorem HomotopicalAlgebra.LeftHomotopyClass.sound {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryWithWeakEquivalences C] {f g : X ⟶ Y} (h : LeftHomotopyRel f g) : mk f = mk g

def HomotopicalAlgebra.LeftHomotopyClass.postcomp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} [CategoryWithWeakEquivalences C] : LeftHomotopyClass X Y → (Y ⟶ Z) → LeftHomotopyClass X Z

The postcomposition map LeftHomotopyClass X Y → (Y ⟶ Z) → LeftHomotopyClass X Z.

Equations

• f.postcomp g = Quot.lift (fun (f : X ⟶ Y) => HomotopicalAlgebra.LeftHomotopyClass.mk (CategoryTheory.CategoryStruct.comp f g)) ⋯ f

@[simp]

theorem HomotopicalAlgebra.LeftHomotopyClass.postcomp_mk {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} [CategoryWithWeakEquivalences C] (f : X ⟶ Y) (g : Y ⟶ Z) : (mk f).postcomp g = mk (CategoryTheory.CategoryStruct.comp f g)

theorem HomotopicalAlgebra.LeftHomotopyClass.mk_eq_mk_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [ModelCategory C] [IsCofibrant X] (f g : X ⟶ Y) : mk f = mk g ↔ LeftHomotopyRel f g