instHasColimitOfModuleCatCompForget₂

English

If a diagram F: J ⥤ TopModuleCat R has a colimit after forgetting to ModuleCat R (via forget₂), then F has a colimit in TopModuleCat R.

Русский

Если диаграмма F: J ⥤ TopModuleCat R имеет колимит после забывания до ModuleCat R, то F имеет колимит в TopModuleCat R.

LaTeX

$$$\\text{HasColimit}(F) \\;\\Longrightarrow\\; \\text{HasColimit}(F).$$$

Lean4

instance {J : Type*} [Category J] {F : J ⥤ TopModuleCat R} [HasColimit (F ⋙ forget₂ _ (ModuleCat R))] : HasColimit F :=
  ⟨_, isColimit (colimit.isColimit _)⟩

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