Right homotopies in model categories

We introduce the types PrepathObject.RightHomotopy and PathObject.RightHomotopy of homotopies between morphisms X ⟶ Y relative to a (pre)path object of Y. Given two morphisms f and g, we introduce the relation RightHomotopyRel f g asserting the existence of a path object P and a right homotopy P.RightHomotopy f g, and we define the quotient type RightHomotopyClass X Y. We show that if Y is a fibrant object in a model category, then RightHomotopyRel is an equivalence relation on X ⟶ Y.

(This file dualizes the definitions in Mathlib/AlgebraicTopology/ModelCategory/LeftHomotopy.lean.)

References

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

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

Given a pre-path object P for Y, two maps f and g in X ⟶ Y are homotopic relative to P when there is a morphism h : X ⟶ P.P such that h ≫ P.p₀ = f and h ≫ P.p₁ = g.

• h : X ⟶ P.P

  a morphism from the source to the pre-path object

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

@[simp]

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

@[simp]

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

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

f : X ⟶ Y is right homotopic to itself relative to any pre-path object.

@[simp]

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

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

If f and g are homotopic relative to a pre-path object P, then g and f are homotopic relative to P.symm

@[simp]

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

noncomputable def HomotopicalAlgebra.PrepathObject.RightHomotopy.trans {C : Type u} [CategoryTheory.Category.{v, u} C] {Y : C} {P : PrepathObject Y} {X : C} {f₀ f₁ f₂ : X ⟶ Y} (h : P.RightHomotopy f₀ f₁) {P' : PrepathObject Y} (h' : P'.RightHomotopy f₁ f₂) [CategoryTheory.Limits.HasPullback P.p₁ P'.p₀] : (P.trans P').RightHomotopy f₀ f₂

If f₀ is homotopic to f₁ relative to a pre-path object P, and f₁ is homotopic to f₂ relative to P', then f₀ is homotopic to f₂ relative to P.trans P'.

@[simp]

theorem HomotopicalAlgebra.PrepathObject.RightHomotopy.trans_h {C : Type u} [CategoryTheory.Category.{v, u} C] {Y : C} {P : PrepathObject Y} {X : C} {f₀ f₁ f₂ : X ⟶ Y} (h : P.RightHomotopy f₀ f₁) {P' : PrepathObject Y} (h' : P'.RightHomotopy f₁ f₂) [CategoryTheory.Limits.HasPullback P.p₁ P'.p₀] : (h.trans h').h = CategoryTheory.Limits.pullback.lift h.h h'.h ⋯

def HomotopicalAlgebra.PrepathObject.RightHomotopy.precomp {C : Type u} [CategoryTheory.Category.{v, u} C] {Y : C} {P : PrepathObject Y} {X : C} {f g : X ⟶ Y} (h : P.RightHomotopy f g) {Z : C} (i : Z ⟶ X) : P.RightHomotopy (CategoryTheory.CategoryStruct.comp i f) (CategoryTheory.CategoryStruct.comp i g)

Right homotopies are compatible with precomposition.

@[simp]

theorem HomotopicalAlgebra.PrepathObject.RightHomotopy.precomp_h {C : Type u} [CategoryTheory.Category.{v, u} C] {Y : C} {P : PrepathObject Y} {X : C} {f g : X ⟶ Y} (h : P.RightHomotopy f g) {Z : C} (i : Z ⟶ X) : (h.precomp i).h = CategoryTheory.CategoryStruct.comp i h.h

@[reducible, inline]

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

Given a path object 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.

@[reducible, inline]

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

f : X ⟶ Y is right homotopic to itself relative to any path object.

@[reducible, inline]

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

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

@[reducible, inline]

abbrev HomotopicalAlgebra.PathObject.RightHomotopy.precomp {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryWithWeakEquivalences C] {P : PathObject Y} {f g : X ⟶ Y} (h : P.RightHomotopy f g) {Z : C} (i : Z ⟶ X) : P.RightHomotopy (CategoryTheory.CategoryStruct.comp i f) (CategoryTheory.CategoryStruct.comp i g)

Right homotopies are compatible with precomposition.

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

@[reducible, inline]

noncomputable abbrev HomotopicalAlgebra.PathObject.RightHomotopy.trans {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [ModelCategory C] {P : PathObject Y} [IsFibrant Y] {f₀ f₁ f₂ : X ⟶ Y} (h : P.RightHomotopy f₀ f₁) {P' : PathObject Y} [P'.IsGood] (h' : P'.RightHomotopy f₁ f₂) [CategoryTheory.Limits.HasPullback P.p₁ P'.p₀] : (P.trans P').RightHomotopy f₀ f₂

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

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

theorem HomotopicalAlgebra.PathObject.RightHomotopy.homotopy_extension {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A B X : C} {P : PathObject B} {f₀ f₁ : A ⟶ B} [IsFibrant B] [P.IsGood] (h : P.RightHomotopy f₀ f₁) (i : A ⟶ X) [Cofibration i] (l₀ : X ⟶ B) (hl₀ : CategoryTheory.CategoryStruct.comp i l₀ = f₀ := by cat_disch) : ∃ (l₁ : X ⟶ B) (h' : P.RightHomotopy l₀ l₁), CategoryTheory.CategoryStruct.comp i h'.h = h.h

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

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

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

theorem HomotopicalAlgebra.PathObject.RightHomotopy.rightHomotopyRel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] {X Y : C} {f g : X ⟶ Y} {P : PathObject Y} (h : P.RightHomotopy f g) : RightHomotopyRel f g

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

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

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

theorem HomotopicalAlgebra.RightHomotopyRel.exists_good_pathObject {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [ModelCategory C] {f g : X ⟶ Y} (h : RightHomotopyRel f g) : ∃ (P : PathObject Y), P.IsGood ∧ Nonempty (P.RightHomotopy f g)

theorem HomotopicalAlgebra.RightHomotopyRel.exists_very_good_pathObject {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [ModelCategory C] {f g : X ⟶ Y} [IsCofibrant X] (h : RightHomotopyRel f g) : ∃ (P : PathObject Y), P.IsVeryGood ∧ Nonempty (P.RightHomotopy f g)

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

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

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

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

def HomotopicalAlgebra.RightHomotopyClass {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 right homotopies.

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

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

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

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

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

The precomposition map RightHomotopyClass Y Z → (X ⟶ Y) → RightHomotopyClass X Z.

@[simp]

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

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