exists_good_cylinder — Mathlib

English

For left-homotopic f and g between X and Y in a model category, there exists a cylinder object P on X that is good and carries a left-homotopy from f to g.

Русский

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

LaTeX

$$$\exists P: Cylinder(X), P.IsGood \land Nonempty(P.LeftHomotopy f g)$$$

Lean4

theorem exists_good_cylinder [ModelCategory C] {f g : X ⟶ Y} (h : LeftHomotopyRel f g) :
    ∃ (P : Cylinder X), P.IsGood ∧ Nonempty (P.LeftHomotopy f g) :=
  by
  obtain ⟨P, ⟨h⟩⟩ := h
  exact h.exists_good_cylinder

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