English
Let F: J ⟶ C and G: C ⟶ D be functors with the relevant colimit structure. For every cocone t over F, the inverse of the canonical colimit comparison composed with G applied to the universal arrow desc_F(t) equals the universal arrow for the composed cocone G.mapCocone(t). In symbols, (preservesColimitIso G F)^{-1} ∘ G(colimit.desc_F t) = colimit.desc_{F∘G}( G(mapCocone)(t) ).
Русский
Пусть F: J ⟶ C и G: C ⟶ D --- функторы с необходимой структурой колимита. Для каждого коконa t над F, обратная сторона канонического сравнения колимита совместно с применением G к универсальному отображению desc_F(t) совпадает с универсальным отображением для композиции коконе G.mapCocone(t). В записи: (preservesColimitIso G F)^{-1} ∘ G(colimit.desc_F t) = colimit.desc_{F∘G}( G(mapCocone)(t) ).
LaTeX
$$$$(\\mathrm{preservesColimitIso}\\, G\\, F)^{-1} \\circ G\\big(\\operatorname{colimit.desc}_F t\\big) = \\operatorname{colimit.desc}_{F \\circ G}\\big( G(\\operatorname{mapCocone}(t))\\big)$$$$
Lean4
@[reassoc (attr := simp)]
theorem preservesColimitIso_inv_comp_desc (t : Cocone F) :
(preservesColimitIso G F).inv ≫ G.map (colimit.desc _ t) = colimit.desc _ (G.mapCocone t) :=
by
ext
simp [← G.map_comp]
