instPreservesFiniteColimitsModuleCatForget₂

English

The forgetful functor forget₂ from FGModuleCat(k) to ModuleCat(k) preserves finite colimits.

Русский

Забывающая функция forget₂: FGModuleCat(k) → ModuleCat(k) сохраняет конечные колимиты.

LaTeX

$$$\operatorname{PreservesFiniteColimits}(\text{forget}_2( FGModuleCat(k), ModuleCat(k) ))$$$

Lean4

instance : PreservesFiniteColimits (forget₂ (FGModuleCat k) (ModuleCat.{v} k)) where
  preservesFiniteColimits _ _ _ := inferInstance

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