English
The transitivity of right homotopy relations on maps between fixed objects in a model category.
Русский
Транзитивность правой гомотопии между отображениями между фиксированными объектами в модельной категории.
LaTeX
$$$\text{RightHomotopyRel } f_0 f_1 \rightarrow \text{RightHomotopyRel } f_1 f_2 \rightarrow \text{RightHomotopyRel } f_0 f_2$$$
Lean4
theorem postcomp [ModelCategory C] {f g : X ⟶ Y} [IsCofibrant X] (h : RightHomotopyRel f g) {Z : C} (p : Y ⟶ Z) :
RightHomotopyRel (f ≫ p) (g ≫ p) :=
by
obtain ⟨P, _, ⟨h⟩⟩ := h.exists_very_good_pathObject
obtain ⟨Q, _⟩ := PathObject.exists_very_good Z
have sq : CommSq (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p)) := { }
exact
⟨Q, ⟨{
h := h.h ≫ sq.lift
h₀ := by
have := sq.fac_right =≫ prod.fst
simp only [Category.assoc, prod.lift_fst, Q.p_fst] at this
simp [this]
h₁ := by
have := sq.fac_right =≫ prod.snd
simp only [Category.assoc, prod.lift_snd, Q.p_snd] at this
simp [this] }⟩⟩
