instPreservesFiniteColimitsForgetOfHasFiniteColimits

English

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

Русский

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

LaTeX

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

Lean4

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

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