English
Let X be cofibrant and Y, Z be fibrant objects in a model category, and g: Y → Z a weak equivalence. Then the map sending a left-homotopy class [f] : X → Y to its postcomposition [f] ∘ g : X → Z is a bijection between left-homotopy classes.
Русский
Пусть X кофибрикабельный, Y и Z – асиды Фибривант в модельной категории, и g: Y → Z – слабая эквивалентность. Тогда отображение [f]: X → Y в [f] ∘ g: X → Z устанавливает биекцию между левыми гиперпроизвольными классами.
LaTeX
$$$\operatorname{Bij}\Big( \lambda f\in \operatorname{LeftHo}(X,Y),\; f\circ g \Big)$$$
Lean4
theorem postcomp_bijective_of_weakEquivalence [IsCofibrant X] (g : Y ⟶ Z) [IsFibrant Y] [IsFibrant Z]
[WeakEquivalence g] : Function.Bijective (fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g) :=
by
let h : FibrantBrownFactorization g := Classical.arbitrary _
have hi : Function.Bijective (fun (f : LeftHomotopyClass X Y) ↦ f.postcomp h.i) :=
by
rw [← Function.Bijective.of_comp_iff' (postcomp_bijective_of_fibration_of_weakEquivalence X h.r)]
convert Function.bijective_id
ext φ
obtain ⟨φ, rfl⟩ := φ.mk_surjective
simp
convert (postcomp_bijective_of_fibration_of_weakEquivalence X h.p).comp hi using 1
ext φ
obtain ⟨φ, rfl⟩ := φ.mk_surjective
simp
