exists_nonempty_homotopy — Mathlib

English

Up to homotopy, the category of (pre-)1-hypercovers is cofiltered: for any f,g there exists W with a morphism to E and a nonempty homotopy between their composites with f and g.

Русский

Пусть f и g — морфизмы, тогда существует W и h: W.Hom E с гомотопией между h∘f и h∘g; то есть категория 1-гиперковеров является кофильтированной по отношению к гомотопии.

LaTeX

$$$\\exists W\\;\\exists h\\;\\mathrm{Nonempty}(\\mathrm{Homotopy}(h\\circ f, h\\circ g))$$$

Lean4

/-- Up to homotopy, the category of (pre-)`1`-hypercovers is cofiltered. -/
theorem exists_nonempty_homotopy (f g : E.Hom F) :
    ∃ (W : PreOneHypercover.{max w w'} S) (h : W.Hom E), Nonempty (Homotopy (h.comp f) (h.comp g)) :=
  ⟨cylinder f g, PreOneHypercover.cylinderHom f g, ⟨cylinderHomotopy f g⟩⟩

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