English
If f: X → Y is a cofibration between cofibrant objects X, Y and a weak equivalence, and Z is fibrant, precomposition with f induces a bijection between RightHomotopyClass(Y,Z) and RightHomotopyClass(X,Z).
Русский
Если f: X → Y – кофибрикация между кофибризованными объектами X, Y и является слабой эквивалентностью, а Z – фибривант, пред-композиция с f порождает биекцию между RightHomotopyClass(Y,Z) и RightHomotopyClass(X,Z).
LaTeX
$$$\operatorname{Bij}\Big( \lambda g\in \operatorname{RightHo}(Y,Z),\; g\circ f\Big)$$$
Lean4
theorem precomp_bijective_of_weakEquivalence [IsFibrant Z] (f : X ⟶ Y) [IsCofibrant X] [IsCofibrant Y]
[WeakEquivalence f] : Function.Bijective (fun (g : RightHomotopyClass Y Z) ↦ g.precomp f) :=
by
let h : CofibrantBrownFactorization f := Classical.arbitrary _
have hj : Function.Bijective (fun (g : RightHomotopyClass Y Z) ↦ g.precomp h.p) :=
by
rw [← Function.Bijective.of_comp_iff' (precomp_bijective_of_cofibration_of_weakEquivalence Z h.s)]
convert Function.bijective_id
ext φ
obtain ⟨φ, rfl⟩ := φ.mk_surjective
simp
convert (precomp_bijective_of_cofibration_of_weakEquivalence Z h.i).comp hj using 1
ext φ
obtain ⟨φ, rfl⟩ := φ.mk_surjective
simp
