exists_good_cylinder — Mathlib

English

Given a left homotopy, there exists a good cylinder P' on X such that a left homotopy from f to g exists in P' and P.i1 and P'.i0 have a pushout, etc.

Русский

Для данного правила левой гомотопии существует хороший цилиндр P' на X, такой что существует левая гомотопия между f и g в P' и выполняются свойства связки через pushout.

LaTeX

$$$\exists P'\,\bigl(P'.IsGood \land \text{Nonempty}(P'.LeftHomotopy f g)\bigr)$$$

Lean4

theorem exists_good_cylinder {f g : X ⟶ Y} (h : P.LeftHomotopy f g) :
    ∃ (P' : Cylinder X), P'.IsGood ∧ Nonempty (P'.LeftHomotopy f g) :=
  by
  let d := MorphismProperty.factorizationData (cofibrations C) (trivialFibrations C) P.i
  exact
    ⟨{  I := d.Z
        i₀ := coprod.inl ≫ d.i
        i₁ := coprod.inr ≫ d.i
        π := d.p ≫ P.π },
      ⟨by
        rw [cofibration_iff]
        convert d.hi
        aesop⟩,
      ⟨{ h := d.p ≫ h.h }⟩⟩

Похожие утверждения