English
Dually, the inv component of the equivalence iso composed with the colimit desc equals the desc along G with the precomposition by w.inv.
Русский
Аналогично, компонент обратной стороны изоморфизма эквивалентности, составленный с декомпозицией колимита, равен декомпозиции через G с предсоставлением через w.inv.
LaTeX
$$$ (\\operatorname{HasColimit.isoOfEquivalence} e w).inv \\; \\circ \\operatorname{colimit.desc} F t = \\operatorname{colimit.desc} G ( (\\operatorname{Cocones.precompose} w.inv).obj t ) $$$
Lean4
@[simp]
theorem pre_pre [h : HasColimit (D ⋙ E ⋙ F)] :
haveI : HasColimit ((D ⋙ E) ⋙ F) := h
colimit.pre (E ⋙ F) D ≫ colimit.pre F E = colimit.pre F (D ⋙ E) :=
by
ext j
rw [← assoc, colimit.ι_pre, colimit.ι_pre]
haveI : HasColimit ((D ⋙ E) ⋙ F) := h
exact (colimit.ι_pre F (D ⋙ E) j).symm
