instReflectsColimitForget — Mathlib

English

Let J be a small category and F : J ⥤ Action V G. The forgetful functor forget V G reflects colimits along F; equivalently, if the underlying cocone in V is a colimit, then F is a colimit in Action V G.

Русский

Пусть J — малая категория и F : J ⥤ Action V G. Функтор-переходник forget V G отражает колимиты вдоль F: если образующийся в V ко-конус является колимитом, то F образует колимит в Action V G.

LaTeX

$$$\\operatorname{ReflectsColimit}(F, \\mathrm{forget}_{V,G})$$$

Lean4

instance {J : Type*} [Category J] (F : J ⥤ Action V G) : ReflectsColimit F (Action.forget V G) where
  reflects
    h :=
    ⟨by
      apply isColimitOfReflects ((Action.functorCategoryEquivalence V G).functor)
      exact evaluationJointlyReflectsColimits _ (fun _ => h)⟩

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