comp_reflectsColimit — Mathlib

English

Let K: J ⥤ C, F: C ⥤ D, G: D ⥤ E. If K F reflects a colimit and K ⋙ F reflects a colimit with G, then K reflects the colimit of F ⋙ G.

Русский

Пусть K: J ⥤ C, F: C ⥤ D, G: D ⥤ E. Если K F отражает колимит, и K ⋙ F отражает колимит для G, тогда K отражает колимит F ⋙ G.

LaTeX

$$$\\mathrm{ReflectsColimit}\,K\,F \\land \\mathrm{ReflectsColimit}\\,(K \\;⋙\\; F)\\,G \\Rightarrow \\mathrm{ReflectsColimit}\\,K\\,(F \\;⋙\\; G)$$$

Lean4

instance comp_reflectsColimit [ReflectsColimit K F] [ReflectsColimit (K ⋙ F) G] : ReflectsColimit K (F ⋙ G) :=
  ⟨fun h => ReflectsColimit.reflects (isColimitOfReflects G h)⟩

Похожие утверждения