English
If f and g are left-homotopic, then there exists a very good cylinder P on X joining them, provided the ambient category satisfies the fibrant condition on Y and related hypotheses.
Русский
Если f и g лево-гомотопичны, существует очень хороший цилиндр P над X, соединяющий их (при дополнительных предпосылках про фибривацию).
LaTeX
$$$\exists P: Cylinder(X), P.IsVeryGood \land Nonempty(P.LeftHomotopy f g)$$$
Lean4
theorem exists_very_good_cylinder [ModelCategory C] {f g : X ⟶ Y} [IsFibrant Y] (h : LeftHomotopyRel f g) :
∃ (P : Cylinder X), P.IsVeryGood ∧ Nonempty (P.LeftHomotopy f g) :=
by
obtain ⟨P, _, ⟨h⟩⟩ := h.exists_good_cylinder
let fac := MorphismProperty.factorizationData (trivialCofibrations C) (fibrations C) P.π
let P' : Cylinder X :=
{ I := fac.Z
i₀ := P.i₀ ≫ fac.i
i₁ := P.i₁ ≫ fac.i
π := fac.p
weakEquivalence_π := weakEquivalence_of_precomp_of_fac fac.fac }
have : Cofibration P'.i := by
rw [show P'.i = P.i ≫ fac.i by cat_disch]
infer_instance
have sq : CommSq h.h fac.i (terminal.from _) (terminal.from _) := { }
exact ⟨P', { }, ⟨{ h := sq.lift }⟩⟩
