hasColimitsOfShape — Mathlib

English

HasColimitsOfShape J (Action V G) when J is a shape and V has ColimitsOfShape J.

Русский

Колимиты формы J в Action V G существуют, если V имеет колимит формы J.

LaTeX

$$$\operatorname{HasColimitsOfShape}(J, \mathrm{Action}(V,G)).$$$

Lean4

/-- If `V` has colimits of shape `J`, so does `Action V G`. -/
instance hasColimitsOfShape {J : Type*} [Category J] [HasColimitsOfShape J V] : HasColimitsOfShape J (Action V G) :=
  Adjunction.hasColimitsOfShape_of_equivalence (Action.functorCategoryEquivalence _ _).functor

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