English
If f is left-homotopic to g, then for any i: Z → X, i ≫ f is left-homotopic to i ≫ g.
Русский
Если f лево-гомотопичен к g, тогда для любого i: Z → X, i ∘ f лево-гомотопичен к i ∘ g.
LaTeX
$$$ f \sim_L g \Rightarrow (i \circ f) \sim_L (i \circ g)$ for any $i: Z \to X$$$
Lean4
theorem precomp [ModelCategory C] {f g : X ⟶ Y} [IsFibrant Y] (h : LeftHomotopyRel f g) {Z : C} (i : Z ⟶ X) :
LeftHomotopyRel (i ≫ f) (i ≫ g) :=
by
obtain ⟨P, _, ⟨h⟩⟩ := h.exists_very_good_cylinder
obtain ⟨Q, _⟩ := Cylinder.exists_very_good Z
have sq : CommSq (coprod.desc (i ≫ P.i₀) (i ≫ P.i₁)) Q.i P.π (Q.π ≫ i) := ⟨by aesop_cat⟩
exact
⟨Q, ⟨{
h := sq.lift ≫ h.h
h₀ := by
have := coprod.inl ≫= sq.fac_left
simp only [Q.inl_i_assoc, coprod.inl_desc] at this
simp [reassoc_of% this]
h₁ := by
have := coprod.inr ≫= sq.fac_left
simp only [Q.inr_i_assoc, coprod.inr_desc] at this
simp [reassoc_of% this] }⟩⟩
