English
The eq_desc statement asserts an equivalence describing that every morphism from the homotopy fiber is determined by a choice of α and a homotopy from φ ≫ α to 0.
Русский
Утверждение eq_desc формулирует эквивалентность: любой морфизм из гомотопического волокна определяется выбором α и гомотопии φ ≫ α → 0.
LaTeX
$$$ f = desc φ (inr φ ≫ f) (Homotopy.trans (Homotopy.ofEq ...) ((inrCompHomotopy φ hc).compRight f).trans (Homotopy.ofEq ...)) $$$
Lean4
theorem eq_desc (f : homotopyCofiber φ ⟶ K) (hc : ∀ j, ∃ i, c.Rel i j) :
f =
desc φ (inr φ ≫ f)
(Homotopy.trans (Homotopy.ofEq (by simp))
(((inrCompHomotopy φ hc).compRight f).trans (Homotopy.ofEq (by simp)))) :=
by
ext j
by_cases hj : c.Rel j (c.next j)
· apply ext_from_X φ _ _ hj
· simp [inrCompHomotopy_hom _ _ _ _ hj]
· simp
· apply ext_from_X' φ _ hj
simp
