instReflectsLimitForget — Mathlib

English

The forgetful functor forget V G reflects limits: if a cone over F is a limit after forgetting, then F is a limit.

Русский

Забывающий функтор forget V G отражает пределы: если конический объект над F является пределом после забывания, то F образует предел.

LaTeX

$$$\operatorname{ReflectsLimit}(F, \mathrm{forget}(V,G)).$$$

Lean4

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

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