Path objects

We introduce a notion of path object for an object A : C in a model category. It consists of an object P, a weak equivalence ι : A ⟶ P equipped with two retractions p₀ and p₁. This notion shall be important in the definition of "right homotopies" in model categories.

This file dualizes the definitions in the file AlgebraicTopology.ModelCategory.Cylinder.

Implementation notes

The most important definition in this file is PathObject A. This structure extends another structure PrepathObject A (which does not assume that C has a notion of weak equivalences, which can be interesting in situations where we have not yet obtained the model category axioms).

The good properties of path objects are stated as typeclasses PathObject.IsGood and PathObject.IsVeryGood.

The existence of very good path objects in model categories is stated in the lemma PathObject.exists_very_good.

References

• [Daniel G. Quillen, Homotopical algebra][Quillen1967]
• https://ncatlab.org/nlab/show/path+space+object

structure HomotopicalAlgebra.PrepathObject {C : Type u} [CategoryTheory.Category.{v, u} C] (A : C) : Type (max u v)

A pre-path object for A : C is the data of a morphism ι : A ⟶ P equipped with two retractions.

• P : C

  the underlying object of a (pre)path object

• p₀ : self.P ⟶ A

  the first "projection" from the (pre)path object

• p₁ : self.P ⟶ A

  the second "projection" from the (pre)path object

• ι : A ⟶ self.P

  the diagonal of the (pre)path object

• ι_p₀ : CategoryTheory.CategoryStruct.comp self.ι self.p₀ = CategoryTheory.CategoryStruct.id A
• ι_p₁ : CategoryTheory.CategoryStruct.comp self.ι self.p₁ = CategoryTheory.CategoryStruct.id A

@[simp]

theorem HomotopicalAlgebra.PrepathObject.ι_p₁_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (self : PrepathObject A) {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp self.ι (CategoryTheory.CategoryStruct.comp self.p₁ h) = h

@[simp]

theorem HomotopicalAlgebra.PrepathObject.ι_p₀_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (self : PrepathObject A) {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp self.ι (CategoryTheory.CategoryStruct.comp self.p₀ h) = h

def HomotopicalAlgebra.PrepathObject.symm {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : PrepathObject A) : PrepathObject A

The pre-path object obtained by switching the two projections.

@[simp]

theorem HomotopicalAlgebra.PrepathObject.symm_p₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : PrepathObject A) : P.symm.p₁ = P.p₀

@[simp]

theorem HomotopicalAlgebra.PrepathObject.symm_P {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : PrepathObject A) : P.symm.P = P.P

@[simp]

theorem HomotopicalAlgebra.PrepathObject.symm_ι {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : PrepathObject A) : P.symm.ι = P.ι

@[simp]

theorem HomotopicalAlgebra.PrepathObject.symm_p₀ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : PrepathObject A) : P.symm.p₀ = P.p₁

noncomputable def HomotopicalAlgebra.PrepathObject.trans {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P P' : PrepathObject A) [CategoryTheory.Limits.HasPullback P.p₁ P'.p₀] : PrepathObject A

The gluing of two pre-path objects.

@[simp]

theorem HomotopicalAlgebra.PrepathObject.trans_ι {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P P' : PrepathObject A) [CategoryTheory.Limits.HasPullback P.p₁ P'.p₀] : (P.trans P').ι = CategoryTheory.Limits.pullback.lift P.ι P'.ι ⋯

@[simp]

theorem HomotopicalAlgebra.PrepathObject.trans_p₀ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P P' : PrepathObject A) [CategoryTheory.Limits.HasPullback P.p₁ P'.p₀] : (P.trans P').p₀ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst P.p₁ P'.p₀) P.p₀

@[simp]

theorem HomotopicalAlgebra.PrepathObject.trans_P {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P P' : PrepathObject A) [CategoryTheory.Limits.HasPullback P.p₁ P'.p₀] : (P.trans P').P = CategoryTheory.Limits.pullback P.p₁ P'.p₀

@[simp]

theorem HomotopicalAlgebra.PrepathObject.trans_p₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P P' : PrepathObject A) [CategoryTheory.Limits.HasPullback P.p₁ P'.p₀] : (P.trans P').p₁ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd P.p₁ P'.p₀) P'.p₁

noncomputable def HomotopicalAlgebra.PrepathObject.p {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : PrepathObject A) [CategoryTheory.Limits.HasBinaryProduct A A] : P.P ⟶ A ⨯ A

The map from P.P to the product of two copies of A, when P is a pre-path object for A. P shall be a good path object when this morphism is a fibration.

@[simp]

theorem HomotopicalAlgebra.PrepathObject.p_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : PrepathObject A) [CategoryTheory.Limits.HasBinaryProduct A A] : CategoryTheory.CategoryStruct.comp P.p CategoryTheory.Limits.prod.fst = P.p₀

@[simp]

theorem HomotopicalAlgebra.PrepathObject.p_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : PrepathObject A) [CategoryTheory.Limits.HasBinaryProduct A A] {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) = CategoryTheory.CategoryStruct.comp P.p₀ h

@[simp]

theorem HomotopicalAlgebra.PrepathObject.p_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : PrepathObject A) [CategoryTheory.Limits.HasBinaryProduct A A] : CategoryTheory.CategoryStruct.comp P.p CategoryTheory.Limits.prod.snd = P.p₁

@[simp]

theorem HomotopicalAlgebra.PrepathObject.p_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : PrepathObject A) [CategoryTheory.Limits.HasBinaryProduct A A] {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h) = CategoryTheory.CategoryStruct.comp P.p₁ h

@[simp]

theorem HomotopicalAlgebra.PrepathObject.symm_p {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : PrepathObject A) [CategoryTheory.Limits.HasBinaryProducts C] : P.symm.p = CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.Limits.prod.braiding A A).hom

theorem HomotopicalAlgebra.PrepathObject.symm_p_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : PrepathObject A) [CategoryTheory.Limits.HasBinaryProducts C] {Z : C} (h : A ⨯ A ⟶ Z) : CategoryTheory.CategoryStruct.comp P.symm.p h = CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.braiding A A).hom h)

structure HomotopicalAlgebra.PathObject {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryWithWeakEquivalences C] (A : C) extends HomotopicalAlgebra.PrepathObject A : Type (max u v)

In a category with weak equivalences, a path object is the data of a weak equivalence ι : A ⟶ P equipped with two retractions.

• P : C
• p₀ : self.P ⟶ A
• p₁ : self.P ⟶ A
• ι : A ⟶ self.P
• ι_p₀ : CategoryTheory.CategoryStruct.comp self.ι self.p₀ = CategoryTheory.CategoryStruct.id A
• ι_p₁ : CategoryTheory.CategoryStruct.comp self.ι self.p₁ = CategoryTheory.CategoryStruct.id A
• weakEquivalence_ι : WeakEquivalence self.ι

def HomotopicalAlgebra.PathObject.symm {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [CategoryWithWeakEquivalences C] (P : PathObject A) : PathObject A

The path object obtained by switching the two projections.

@[simp]

theorem HomotopicalAlgebra.PathObject.symm_P {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [CategoryWithWeakEquivalences C] (P : PathObject A) : P.symm.P = P.P

@[simp]

theorem HomotopicalAlgebra.PathObject.symm_ι {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [CategoryWithWeakEquivalences C] (P : PathObject A) : P.symm.ι = P.ι

@[simp]

theorem HomotopicalAlgebra.PathObject.symm_p₀ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [CategoryWithWeakEquivalences C] (P : PathObject A) : P.symm.p₀ = P.p₁

@[simp]

theorem HomotopicalAlgebra.PathObject.symm_p₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [CategoryWithWeakEquivalences C] (P : PathObject A) : P.symm.p₁ = P.p₀

@[simp]

theorem HomotopicalAlgebra.PathObject.symm_p {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [CategoryWithWeakEquivalences C] (P : PathObject A) [CategoryTheory.Limits.HasBinaryProducts C] : P.symm.p = CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.Limits.prod.braiding A A).hom

theorem HomotopicalAlgebra.PathObject.symm_p_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [CategoryWithWeakEquivalences C] (P : PathObject A) [CategoryTheory.Limits.HasBinaryProducts C] {Z : C} (h : A ⨯ A ⟶ Z) : CategoryTheory.CategoryStruct.comp P.symm.p h = CategoryTheory.CategoryStruct.comp P.p (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.braiding A A).hom h)

instance HomotopicalAlgebra.PathObject.instWeakEquivalenceP₀ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [CategoryWithWeakEquivalences C] (P : PathObject A) [(weakEquivalences C).HasTwoOutOfThreeProperty] [(weakEquivalences C).ContainsIdentities] : WeakEquivalence P.p₀

instance HomotopicalAlgebra.PathObject.instWeakEquivalenceP₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [CategoryWithWeakEquivalences C] (P : PathObject A) [(weakEquivalences C).HasTwoOutOfThreeProperty] [(weakEquivalences C).ContainsIdentities] : WeakEquivalence P.p₁

class HomotopicalAlgebra.PathObject.IsGood {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [CategoryWithWeakEquivalences C] (P : PathObject A) [CategoryTheory.Limits.HasBinaryProduct A A] [CategoryWithFibrations C] : Prop

A path object P is good if the morphism P.p : P.P ⟶ A ⨯ A is a fibration.

• fibration_p : Fibration P.p

class HomotopicalAlgebra.PathObject.IsVeryGood {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [CategoryWithWeakEquivalences C] (P : PathObject A) [CategoryTheory.Limits.HasBinaryProduct A A] [CategoryWithFibrations C] [CategoryWithCofibrations C] extends P.IsGood : Prop

A good path object P is very good if P.ι is a (trivial) cofibration.

• fibration_p : Fibration P.p
• cofibration_ι : Cofibration P.ι

instance HomotopicalAlgebra.PathObject.instFibrationP₀ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [CategoryWithWeakEquivalences C] (P : PathObject A) [CategoryTheory.Limits.HasBinaryProduct A A] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] [(fibrations C).IsStableUnderComposition] [(fibrations C).IsStableUnderBaseChange] [IsFibrant A] [P.IsGood] : Fibration P.p₀

instance HomotopicalAlgebra.PathObject.instFibrationP₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [CategoryWithWeakEquivalences C] (P : PathObject A) [CategoryTheory.Limits.HasBinaryProduct A A] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] [(fibrations C).IsStableUnderComposition] [(fibrations C).IsStableUnderBaseChange] [IsFibrant A] [P.IsGood] : Fibration P.p₁

instance HomotopicalAlgebra.PathObject.instIsFibrantP {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [CategoryWithWeakEquivalences C] (P : PathObject A) [CategoryTheory.Limits.HasBinaryProduct A A] [CategoryWithFibrations C] [CategoryTheory.Limits.HasTerminal C] [(fibrations C).IsStableUnderComposition] [(fibrations C).IsStableUnderBaseChange] [IsFibrant A] [P.IsGood] : IsFibrant P.P

instance HomotopicalAlgebra.PathObject.instIsGoodSymmOfRespectsIsoFibrations {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [CategoryWithWeakEquivalences C] (P : PathObject A) [CategoryTheory.Limits.HasBinaryProducts C] [CategoryWithFibrations C] [P.IsGood] [(fibrations C).RespectsIso] : P.symm.IsGood

instance HomotopicalAlgebra.PathObject.instIsCofibrantPOfIsVeryGood {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [CategoryWithWeakEquivalences C] (P : PathObject A) [CategoryWithFibrations C] [CategoryWithCofibrations C] [(cofibrations C).IsStableUnderComposition] [CategoryTheory.Limits.HasBinaryProduct A A] [CategoryTheory.Limits.HasInitial C] [IsCofibrant A] [P.IsVeryGood] : IsCofibrant P.P

instance HomotopicalAlgebra.PathObject.instIsVeryGoodSymmOfRespectsIsoFibrations {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [CategoryWithWeakEquivalences C] (P : PathObject A) [CategoryWithFibrations C] [CategoryWithCofibrations C] [(fibrations C).RespectsIso] [CategoryTheory.Limits.HasBinaryProducts C] [P.IsVeryGood] : P.symm.IsVeryGood

noncomputable def HomotopicalAlgebra.PathObject.ofFactorizationData {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} (h : (trivialCofibrations C).MapFactorizationData (fibrations C) (CategoryTheory.Limits.diag A)) : PathObject A

A path object for A can be obtained from a factorization of the obvious map A ⟶ A ⨯ A as a trivial cofibration followed by a fibration.

@[simp]

theorem HomotopicalAlgebra.PathObject.ofFactorizationData_P {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} (h : (trivialCofibrations C).MapFactorizationData (fibrations C) (CategoryTheory.Limits.diag A)) : (ofFactorizationData h).P = h.Z

@[simp]

theorem HomotopicalAlgebra.PathObject.ofFactorizationData_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} (h : (trivialCofibrations C).MapFactorizationData (fibrations C) (CategoryTheory.Limits.diag A)) : (ofFactorizationData h).ι = h.i

@[simp]

theorem HomotopicalAlgebra.PathObject.ofFactorizationData_p₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} (h : (trivialCofibrations C).MapFactorizationData (fibrations C) (CategoryTheory.Limits.diag A)) : (ofFactorizationData h).p₁ = CategoryTheory.CategoryStruct.comp h.p CategoryTheory.Limits.prod.snd

@[simp]

theorem HomotopicalAlgebra.PathObject.ofFactorizationData_p₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} (h : (trivialCofibrations C).MapFactorizationData (fibrations C) (CategoryTheory.Limits.diag A)) : (ofFactorizationData h).p₀ = CategoryTheory.CategoryStruct.comp h.p CategoryTheory.Limits.prod.fst

@[simp]

theorem HomotopicalAlgebra.PathObject.ofFactorizationData_p {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} (h : (trivialCofibrations C).MapFactorizationData (fibrations C) (CategoryTheory.Limits.diag A)) : (ofFactorizationData h).p = h.p

instance HomotopicalAlgebra.PathObject.instIsVeryGoodOfFactorizationData {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} (h : (trivialCofibrations C).MapFactorizationData (fibrations C) (CategoryTheory.Limits.diag A)) : (ofFactorizationData h).IsVeryGood

instance HomotopicalAlgebra.PathObject.instIsCofibrantPOfFactorizationDataOfIsStableUnderCompositionCofibrations {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} (h : (trivialCofibrations C).MapFactorizationData (fibrations C) (CategoryTheory.Limits.diag A)) [CategoryTheory.Limits.HasInitial C] [IsCofibrant A] [(cofibrations C).IsStableUnderComposition] : IsCofibrant (ofFactorizationData h).P

theorem HomotopicalAlgebra.PathObject.exists_very_good {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] (A : C) : ∃ (P : PathObject A), P.IsVeryGood

instance HomotopicalAlgebra.PathObject.instNonempty {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} : Nonempty (PathObject A)

noncomputable def HomotopicalAlgebra.PathObject.trans {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} [IsFibrant A] (P P' : PathObject A) [P'.IsGood] : PathObject A

The gluing of two good path objects.

@[simp]

theorem HomotopicalAlgebra.PathObject.trans_P {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} [IsFibrant A] (P P' : PathObject A) [P'.IsGood] : (P.trans P').P = CategoryTheory.Limits.pullback P.p₁ P'.p₀

@[simp]

theorem HomotopicalAlgebra.PathObject.trans_p₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} [IsFibrant A] (P P' : PathObject A) [P'.IsGood] : (P.trans P').p₀ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst P.p₁ P'.p₀) P.p₀

@[simp]

theorem HomotopicalAlgebra.PathObject.trans_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} [IsFibrant A] (P P' : PathObject A) [P'.IsGood] : (P.trans P').ι = CategoryTheory.Limits.pullback.lift P.ι P'.ι ⋯

@[simp]

theorem HomotopicalAlgebra.PathObject.trans_p₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} [IsFibrant A] (P P' : PathObject A) [P'.IsGood] : (P.trans P').p₁ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd P.p₁ P'.p₀) P'.p₁

instance HomotopicalAlgebra.PathObject.instIsGoodTrans {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} [IsFibrant A] (P P' : PathObject A) [P.IsGood] [P'.IsGood] : (P.trans P').IsGood