English
For a diagram F: J ⥤ PresheafedSpace C and a cocone s over F, the natural descent morphism desc F s satisfies that composing the colimit cocone with desc recovers the cocone component: (colimitCocone F).ι.app j ≫ desc F s = s.ι.app j for every j.
Русский
Для диаграммы F: J ⥤ PresheafedSpace C и коконьe s над F, естественный морфизм спуска desc F s удовлетворяет равенству, что композиция инъекции коллимита с desc возвращает компоненту коконa: (colimitCocone F).ι.app j ≫ desc F s = s.ι.app j для каждого j.
LaTeX
$$$ (\\operatorname{colimitCocone} F).\\iota._{j} \\circ \\operatorname{desc} F s = s._{j}$$$
Lean4
theorem desc_fac (F : J ⥤ PresheafedSpace.{_, _, v} C) (s : Cocone F) (j : J) :
(colimitCocone F).ι.app j ≫ desc F s = s.ι.app j := by
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): the original proof is just
-- `ext <;> dsimp [desc, descCApp] <;> simpa`,
-- but this has to be expanded a bit
ext U
· simp [desc]
· simp only [op_obj, desc, descCApp, Presheaf.comp_app, comp_c_app, colimitCocone_ι_app_c, assoc]
rw [limitObjIsoLimitCompEvaluation_inv_π_app_assoc]
simp
