Cylinders

We introduce a notion of cylinder for an object A : C in a model category. It consists of an object I, a weak equivalence π : I ⟶ A equipped with two sections i₀ and i₁. This notion shall be important in the definition of "left homotopies" in model categories.

Implementation notes

The most important definition in this file is Cylinder A. This structure extends another structure Precylinder 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 cylinders are stated as typeclasses Cylinder.IsGood and Cylinder.IsVeryGood.

The existence of very good cylinder objects in model categories is stated in the lemma Cylinder.exists_very_good.

References

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

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

A precylinder for A : C is the data of a morphism π : I ⟶ A equipped with two sections.

• I : C

  the underlying object of a (pre)cylinder

• i₀ : A ⟶ self.I

  the first "inclusion" in the (pre)cylinder

• i₁ : A ⟶ self.I

  the second "inclusion" in the (pre)cylinder

• π : self.I ⟶ A

  the codiagonal of the (pre)cylinder

• i₀_π : CategoryTheory.CategoryStruct.comp self.i₀ self.π = CategoryTheory.CategoryStruct.id A
• i₁_π : CategoryTheory.CategoryStruct.comp self.i₁ self.π = CategoryTheory.CategoryStruct.id A

@[simp]

theorem HomotopicalAlgebra.Precylinder.i₀_π_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (self : Precylinder A) {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp self.i₀ (CategoryTheory.CategoryStruct.comp self.π h) = h

@[simp]

theorem HomotopicalAlgebra.Precylinder.i₁_π_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (self : Precylinder A) {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp self.i₁ (CategoryTheory.CategoryStruct.comp self.π h) = h

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

The precylinder object obtained by switching the two inclusions.

@[simp]

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

@[simp]

theorem HomotopicalAlgebra.Precylinder.symm_i₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : Precylinder A) : P.symm.i₁ = P.i₀

@[simp]

theorem HomotopicalAlgebra.Precylinder.symm_i₀ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : Precylinder A) : P.symm.i₀ = P.i₁

@[simp]

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

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

The gluing of two precylinders.

@[simp]

theorem HomotopicalAlgebra.Precylinder.trans_I {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P P' : Precylinder A) [CategoryTheory.Limits.HasPushout P.i₁ P'.i₀] : (P.trans P').I = CategoryTheory.Limits.pushout P.i₁ P'.i₀

@[simp]

theorem HomotopicalAlgebra.Precylinder.trans_i₀ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P P' : Precylinder A) [CategoryTheory.Limits.HasPushout P.i₁ P'.i₀] : (P.trans P').i₀ = CategoryTheory.CategoryStruct.comp P.i₀ (CategoryTheory.Limits.pushout.inl P.i₁ P'.i₀)

@[simp]

theorem HomotopicalAlgebra.Precylinder.trans_π {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P P' : Precylinder A) [CategoryTheory.Limits.HasPushout P.i₁ P'.i₀] : (P.trans P').π = CategoryTheory.Limits.pushout.desc P.π P'.π ⋯

@[simp]

theorem HomotopicalAlgebra.Precylinder.trans_i₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P P' : Precylinder A) [CategoryTheory.Limits.HasPushout P.i₁ P'.i₀] : (P.trans P').i₁ = CategoryTheory.CategoryStruct.comp P'.i₁ (CategoryTheory.Limits.pushout.inr P.i₁ P'.i₀)

noncomputable def HomotopicalAlgebra.Precylinder.i {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : Precylinder A) [CategoryTheory.Limits.HasBinaryCoproduct A A] : A ⨿ A ⟶ P.I

the map from the coproduct of two copies of A to P.I, when P is a cylinder object for A. P shall be a good cylinder object when this morphism is a cofibration.

@[simp]

theorem HomotopicalAlgebra.Precylinder.inl_i {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : Precylinder A) [CategoryTheory.Limits.HasBinaryCoproduct A A] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl P.i = P.i₀

@[simp]

theorem HomotopicalAlgebra.Precylinder.inl_i_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : Precylinder A) [CategoryTheory.Limits.HasBinaryCoproduct A A] {Z : C} (h : P.I ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp P.i h) = CategoryTheory.CategoryStruct.comp P.i₀ h

@[simp]

theorem HomotopicalAlgebra.Precylinder.inr_i {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : Precylinder A) [CategoryTheory.Limits.HasBinaryCoproduct A A] : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr P.i = P.i₁

@[simp]

theorem HomotopicalAlgebra.Precylinder.inr_i_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : Precylinder A) [CategoryTheory.Limits.HasBinaryCoproduct A A] {Z : C} (h : P.I ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.CategoryStruct.comp P.i h) = CategoryTheory.CategoryStruct.comp P.i₁ h

@[simp]

theorem HomotopicalAlgebra.Precylinder.symm_i {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : Precylinder A) [CategoryTheory.Limits.HasBinaryCoproducts C] : P.symm.i = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.braiding A A).hom P.i

theorem HomotopicalAlgebra.Precylinder.symm_i_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} (P : Precylinder A) [CategoryTheory.Limits.HasBinaryCoproducts C] {Z : C} (h : P.symm.I ⟶ Z) : CategoryTheory.CategoryStruct.comp P.symm.i h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.braiding A A).hom (CategoryTheory.CategoryStruct.comp P.i h)

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

In a category with weak equivalences, a cylinder is the data of a weak equivalence π : I ⟶ A equipped with two sections

• I : C
• i₀ : A ⟶ self.I
• i₁ : A ⟶ self.I
• π : self.I ⟶ A
• i₀_π : CategoryTheory.CategoryStruct.comp self.i₀ self.π = CategoryTheory.CategoryStruct.id A
• i₁_π : CategoryTheory.CategoryStruct.comp self.i₁ self.π = CategoryTheory.CategoryStruct.id A
• weakEquivalence_π : WeakEquivalence self.π

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

The cylinder object obtained by switching the two inclusions.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem HomotopicalAlgebra.Cylinder.symm_i {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [CategoryWithWeakEquivalences C] (P : Cylinder A) [CategoryTheory.Limits.HasBinaryCoproducts C] : P.symm.i = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.braiding A A).hom P.i

theorem HomotopicalAlgebra.Cylinder.symm_i_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [CategoryWithWeakEquivalences C] (P : Cylinder A) [CategoryTheory.Limits.HasBinaryCoproducts C] {Z : C} (h : P.symm.I ⟶ Z) : CategoryTheory.CategoryStruct.comp P.symm.i h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.braiding A A).hom (CategoryTheory.CategoryStruct.comp P.i h)

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

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

class HomotopicalAlgebra.Cylinder.IsGood {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [CategoryWithWeakEquivalences C] (P : Cylinder A) [CategoryTheory.Limits.HasBinaryCoproduct A A] [CategoryWithCofibrations C] : Prop

A cylinder object P is good if the morphism P.i : A ⨿ A ⟶ P.I is a cofibration.

• cofibration_i : Cofibration P.i

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

A good cylinder object P is very good if P.π is a (trivial) fibration.

• cofibration_i : Cofibration P.i
• fibration_π : Fibration P.π

instance HomotopicalAlgebra.Cylinder.instCofibrationI₀ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [CategoryWithWeakEquivalences C] (P : Cylinder A) [CategoryTheory.Limits.HasBinaryCoproduct A A] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [(cofibrations C).IsStableUnderComposition] [(cofibrations C).IsStableUnderCobaseChange] [IsCofibrant A] [P.IsGood] : Cofibration P.i₀

instance HomotopicalAlgebra.Cylinder.instCofibrationI₁ {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [CategoryWithWeakEquivalences C] (P : Cylinder A) [CategoryTheory.Limits.HasBinaryCoproduct A A] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [(cofibrations C).IsStableUnderComposition] [(cofibrations C).IsStableUnderCobaseChange] [IsCofibrant A] [P.IsGood] : Cofibration P.i₁

instance HomotopicalAlgebra.Cylinder.instIsCofibrantI {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [CategoryWithWeakEquivalences C] (P : Cylinder A) [CategoryTheory.Limits.HasBinaryCoproduct A A] [CategoryWithCofibrations C] [CategoryTheory.Limits.HasInitial C] [(cofibrations C).IsStableUnderComposition] [(cofibrations C).IsStableUnderCobaseChange] [IsCofibrant A] [P.IsGood] : IsCofibrant P.I

instance HomotopicalAlgebra.Cylinder.instIsGoodSymmOfRespectsIsoCofibrations {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [CategoryWithWeakEquivalences C] (P : Cylinder A) [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryWithCofibrations C] [P.IsGood] [(cofibrations C).RespectsIso] : P.symm.IsGood

instance HomotopicalAlgebra.Cylinder.instIsFibrantIOfIsVeryGood {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [CategoryWithWeakEquivalences C] (P : Cylinder A) [CategoryWithCofibrations C] [CategoryWithFibrations C] [(fibrations C).IsStableUnderComposition] [CategoryTheory.Limits.HasBinaryCoproduct A A] [CategoryTheory.Limits.HasTerminal C] [IsFibrant A] [P.IsVeryGood] : IsFibrant P.I

instance HomotopicalAlgebra.Cylinder.instIsVeryGoodSymmOfRespectsIsoCofibrations {C : Type u} [CategoryTheory.Category.{v, u} C] {A : C} [CategoryWithWeakEquivalences C] (P : Cylinder A) [CategoryWithCofibrations C] [CategoryWithFibrations C] [(cofibrations C).RespectsIso] [CategoryTheory.Limits.HasBinaryCoproducts C] [P.IsVeryGood] : P.symm.IsVeryGood

noncomputable def HomotopicalAlgebra.Cylinder.ofFactorizationData {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} (h : (cofibrations C).MapFactorizationData (trivialFibrations C) (CategoryTheory.Limits.codiag A)) : Cylinder A

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

@[simp]

theorem HomotopicalAlgebra.Cylinder.ofFactorizationData_i₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} (h : (cofibrations C).MapFactorizationData (trivialFibrations C) (CategoryTheory.Limits.codiag A)) : (ofFactorizationData h).i₀ = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h.i

@[simp]

theorem HomotopicalAlgebra.Cylinder.ofFactorizationData_π {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} (h : (cofibrations C).MapFactorizationData (trivialFibrations C) (CategoryTheory.Limits.codiag A)) : (ofFactorizationData h).π = h.p

@[simp]

theorem HomotopicalAlgebra.Cylinder.ofFactorizationData_I {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} (h : (cofibrations C).MapFactorizationData (trivialFibrations C) (CategoryTheory.Limits.codiag A)) : (ofFactorizationData h).I = h.Z

@[simp]

theorem HomotopicalAlgebra.Cylinder.ofFactorizationData_i₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} (h : (cofibrations C).MapFactorizationData (trivialFibrations C) (CategoryTheory.Limits.codiag A)) : (ofFactorizationData h).i₁ = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h.i

@[simp]

theorem HomotopicalAlgebra.Cylinder.ofFactorizationData_i {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} (h : (cofibrations C).MapFactorizationData (trivialFibrations C) (CategoryTheory.Limits.codiag A)) : (ofFactorizationData h).i = h.i

instance HomotopicalAlgebra.Cylinder.instIsVeryGoodOfFactorizationData {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} (h : (cofibrations C).MapFactorizationData (trivialFibrations C) (CategoryTheory.Limits.codiag A)) : (ofFactorizationData h).IsVeryGood

instance HomotopicalAlgebra.Cylinder.instIsFibrantIOfFactorizationDataOfIsStableUnderCompositionFibrations {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} (h : (cofibrations C).MapFactorizationData (trivialFibrations C) (CategoryTheory.Limits.codiag A)) [CategoryTheory.Limits.HasTerminal C] [IsFibrant A] [(fibrations C).IsStableUnderComposition] : IsFibrant (ofFactorizationData h).I

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

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

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

The gluing of two good cylinders.

@[simp]

theorem HomotopicalAlgebra.Cylinder.trans_i₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} [IsCofibrant A] (P P' : Cylinder A) [P'.IsGood] : (P.trans P').i₁ = CategoryTheory.CategoryStruct.comp P'.i₁ (CategoryTheory.Limits.pushout.inr P.i₁ P'.i₀)

@[simp]

theorem HomotopicalAlgebra.Cylinder.trans_i₀ {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} [IsCofibrant A] (P P' : Cylinder A) [P'.IsGood] : (P.trans P').i₀ = CategoryTheory.CategoryStruct.comp P.i₀ (CategoryTheory.Limits.pushout.inl P.i₁ P'.i₀)

@[simp]

theorem HomotopicalAlgebra.Cylinder.trans_π {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} [IsCofibrant A] (P P' : Cylinder A) [P'.IsGood] : (P.trans P').π = CategoryTheory.Limits.pushout.desc P.π P'.π ⋯

@[simp]

theorem HomotopicalAlgebra.Cylinder.trans_I {C : Type u} [CategoryTheory.Category.{v, u} C] [ModelCategory C] {A : C} [IsCofibrant A] (P P' : Cylinder A) [P'.IsGood] : (P.trans P').I = CategoryTheory.Limits.pushout P.i₁ P'.i₀

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