instPreservesFiniteLimitsForgetOfHasFiniteLimits

English

The forgetful functor forget V G preserves finite limits whenever V has finite limits.

Русский

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

LaTeX

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

Lean4

noncomputable instance [HasFiniteLimits V] : PreservesFiniteLimits (Action.forget V G) :=
  by
  change
    PreservesFiniteLimits
      ((Action.functorCategoryEquivalence V G).functor ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))
  have : PreservesFiniteLimits ((evaluation (SingleObj G) V).obj (SingleObj.star G)) :=
    by
    constructor
    intro _ _ _
    infer_instance
  apply comp_preservesFiniteLimits

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