Theorems · Theorem · category theory

HomotopicalAlgebra.PathObject.RightHomotopy.homotopy_extension

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A B X : C}
  {P : HomotopicalAlgebra.PathObject B} {f₀ f₁ : A ⟶ B} [HomotopicalAlgebra.IsFibrant B] [P.IsGood]
  (h : P.RightHomotopy f₀ f₁) (i : A ⟶ X) [HomotopicalAlgebra.Cofibration i] (l₀ : X ⟶ B),
  autoParam (CategoryTheory.CategoryStruct.comp i l₀ = f₀)
      HomotopicalAlgebra.PathObject.RightHomotopy.homotopy_extension._auto_1 →
    ∃ l₁ h', 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₁).

Defined in

Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy

Cited by

0 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryHomotopicalAlgebra.ModelCategoryHomotopicalAlgebra.IsFibrantHomotopicalAlgebra.PathObject.IsGoodHomotopicalAlgebra.Cofibration