English
Let X be cofibrant. For any fibration g: Y → Z which is a weak equivalence, the postcomposition map on left homotopy classes, f ↦ f.postcomp g, is a bijection between LeftHomotopyClass X Y and LeftHomotopyClass X Z.
Русский
Пусть X ко-фибриентен. Для любого фибрационального г: Y → Z, являющегося слабой эквивалентностью, отображение f ↦ f.postcomp g является биекцией между классами левогомотопий X→Y и X→Z.
LaTeX
$$$\text{postcomp Bijective}$; $\forall X, g: Y\to Z$ с [IsCofibrant X], [Fibration g], [WeakEquivalence g],\; \mathrm{postcomp}: \text{LeftHomotopyClass}(X,Y) \to \text{LeftHomotopyClass}(X,Z)$ is bijective.$$
Lean4
theorem postcomp_bijective_of_fibration_of_weakEquivalence [IsCofibrant X] (g : Y ⟶ Z) [Fibration g]
[WeakEquivalence g] : Function.Bijective (fun (f : LeftHomotopyClass X Y) ↦ f.postcomp g) :=
by
constructor
· intro f₀ f₁ h
obtain ⟨f₀, rfl⟩ := f₀.mk_surjective
obtain ⟨f₁, rfl⟩ := f₁.mk_surjective
simp only [postcomp_mk, mk_eq_mk_iff] at h
obtain ⟨P, _, ⟨h⟩⟩ := h.exists_good_cylinder
have sq : CommSq (coprod.desc f₀ f₁) P.i g h.h := { }
rw [mk_eq_mk_iff]
exact
⟨P, ⟨{
h := sq.lift
h₀ := by
have := coprod.inl ≫= sq.fac_left
rwa [P.inl_i_assoc, coprod.inl_desc] at this
h₁ := by
have := coprod.inr ≫= sq.fac_left
rwa [P.inr_i_assoc, coprod.inr_desc] at this }⟩⟩
· intro φ
obtain ⟨φ, rfl⟩ := φ.mk_surjective
have sq : CommSq (initial.to Y) (initial.to X) g φ := { }
exact ⟨mk sq.lift, by simp⟩
