trans — Mathlib

English

If f0 is left-homotopic to f1 and f1 is left-homotopic to f2, then f0 is left-homotopic to f2 (under suitable cofibrancy assumptions).

Русский

Если f0 левая гомотопия к f1 и f1 к f2, тогда f0 левая гомотопия к f2 (при разумных допущениях о кофтрибированных).

LaTeX

$$$ f_0 \sim_L f_1 \land f_1 \sim_L f_2 \Rightarrow f_0 \sim_L f_2$$$

Lean4

theorem trans [ModelCategory C] {f₀ f₁ f₂ : X ⟶ Y} [IsCofibrant X] (h : LeftHomotopyRel f₀ f₁)
    (h' : LeftHomotopyRel f₁ f₂) : LeftHomotopyRel f₀ f₂ :=
  by
  obtain ⟨P, ⟨h⟩⟩ := h
  obtain ⟨P', _, ⟨h'⟩⟩ := h'.exists_good_cylinder
  exact (h.trans h').leftHomotopyRel

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