English
Assume Z is fibrant and f: X → Y is a cofibration and a weak equivalence. Then precomposition with f induces a bijection between right-homotopy classes from Y to Z and from X to Z.
Русский
Пусть Z фибривант, f: X → Y коферибация и слабая эквивалентность. Тогда пред-композиция с f порождает биекцию между правыми гомотопическими классами обзора Y → Z и X → Z.
LaTeX
$$$\operatorname{Bij}\Big( \lambda g\in \operatorname{RightHo}(Y,Z),\; g\circ f\Big)$$$
Lean4
theorem precomp_bijective_of_cofibration_of_weakEquivalence [IsFibrant Z] (f : X ⟶ Y) [Cofibration f]
[WeakEquivalence f] : Function.Bijective (fun (g : RightHomotopyClass Y Z) ↦ g.precomp f) :=
by
constructor
· intro f₀ f₁ h
obtain ⟨f₀, rfl⟩ := f₀.mk_surjective
obtain ⟨f₁, rfl⟩ := f₁.mk_surjective
simp only [precomp_mk, mk_eq_mk_iff] at h
obtain ⟨P, _, ⟨h⟩⟩ := h.exists_good_pathObject
have sq : CommSq h.h f P.p (prod.lift f₀ f₁) := { }
rw [mk_eq_mk_iff]
exact
⟨P, ⟨{
h := sq.lift
h₀ := by
have := sq.fac_right =≫ prod.fst
rwa [Category.assoc, P.p_fst, prod.lift_fst] at this
h₁ := by
have := sq.fac_right =≫ prod.snd
rwa [Category.assoc, P.p_snd, prod.lift_snd] at this }⟩⟩
· intro φ
obtain ⟨φ, rfl⟩ := φ.mk_surjective
have sq : CommSq φ f (terminal.from _) (terminal.from _) := { }
exact ⟨mk sq.lift, by simp⟩
