English
Let X and Y be cofibrant and fibrant respectively, and f: X → Y a weak equivalence. Then there exists g: Y → X such that f ∘ g ≃ id_X and g ∘ f ≃ id_Y up to right-homotopy.
Русский
Пусть X кофибривиден, Y фибривант, и f: X → Y – слабая эквивалентность. Тогда существует g: Y → X such that f ∘ g и g ∘ f гомотопически равны соответствующим единичным маппингам.Y
LaTeX
$$$\exists g:\; Y\to X\;\text{such that } (f\circ g)\sim_{\mathrm{R}} id_X \text{ and } (g\circ f)\sim_{\mathrm{R}} id_Y$$$
Lean4
theorem whitehead [IsCofibrant X] [IsCofibrant Y] [IsFibrant X] [IsFibrant Y] (f : X ⟶ Y) [WeakEquivalence f] :
∃ (g : Y ⟶ X), RightHomotopyRel (f ≫ g) (𝟙 X) ∧ RightHomotopyRel (g ≫ f) (𝟙 Y) :=
by
obtain ⟨g, hg⟩ := (precomp_bijective_of_weakEquivalence X f).2 (.mk (𝟙 X))
obtain ⟨g, rfl⟩ := g.mk_surjective
dsimp at hg
refine ⟨g, by rwa [← mk_eq_mk_iff], ?_⟩
rw [← mk_eq_mk_iff]
apply (precomp_bijective_of_weakEquivalence Y f).1
simp only [precomp_mk, Category.comp_id]
rw [mk_eq_mk_iff, ← leftHomotopyRel_iff_rightHomotopyRel] at hg ⊢
simpa using hg.postcomp f
