English
If f and g are right-homotopic and X is cofibrant (in a Model category), then there exists a path object P for Y that is very good and P.RightHomotopy f g is nonempty.
Русский
Если f и g правой гомотопии эквивалентны и X ко-фибрилен в модельной категории, то существует путь-объект P для Y, который очень хорош, и P.RightHomotopy f g непусто.
LaTeX
$$$(\\exists P : PathObject Y, P.IsVeryGood \\wedge Nonempty (P.RightHomotopy f g))$$$
Lean4
theorem exists_very_good_pathObject [ModelCategory C] {f g : X ⟶ Y} [IsCofibrant X] (h : RightHomotopyRel f g) :
∃ (P : PathObject Y), P.IsVeryGood ∧ Nonempty (P.RightHomotopy f g) :=
by
obtain ⟨P, _, ⟨h⟩⟩ := h.exists_good_pathObject
let fac := MorphismProperty.factorizationData (cofibrations C) (trivialFibrations C) P.ι
let P' : PathObject Y :=
{ P := fac.Z
p₀ := fac.p ≫ P.p₀
p₁ := fac.p ≫ P.p₁
ι := fac.i
weakEquivalence_ι := weakEquivalence_of_postcomp_of_fac fac.fac }
have : Fibration P'.p := by
rw [show P'.p = fac.p ≫ P.p by cat_disch]
infer_instance
have sq : CommSq (initial.to _) (initial.to _) fac.p h.h := { }
exact ⟨P', { }, ⟨{ h := sq.lift }⟩⟩
