instReflectsColimitsForget — Mathlib

English

The forgetful functor forget V G : Action V G → V reflects colimits of all shapes; i.e., if a diagram in Action V G becomes a colimit after forgetting, then it was already a colimit in Action V G.

Русский

Функтор забывания forget V G : Action V G → V отражает колимиты произвольных форм; то есть если диаграмма в Action V G становится колимитом после забывания, то она была колимитом и в самой категории Action V G.

LaTeX

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

Lean4

noncomputable instance : ReflectsColimits (Action.forget V G) where

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