forget₂ (FGModuleCat K) (ModuleCat K) creates all finite colimits.

And hence FGModuleCat K has all finite colimits.

instance FGModuleCat.instFiniteCarrierSigmaObjModuleCatOfFinite {k : Type u} [Ring k] {J : Type} [Finite J] (Z : J → ModuleCat k) [∀ (j : J), Module.Finite k ↑(Z j)] : Module.Finite k ↑(∐ fun (j : J) => Z j)

instance FGModuleCat.instFiniteCarrierColimitModuleCatCompForget₂LinearMapIdObjIsFG {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] {k : Type u} [Ring k] (F : CategoryTheory.Functor J (FGModuleCat k)) : Module.Finite k ↑(CategoryTheory.Limits.colimit (F.comp (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))))

Finite colimits of finite modules are finite, because we can realise them as quotients of a finite coproduct.

def FGModuleCat.forget₂CreatesColimit {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] {k : Type u} [Ring k] (F : CategoryTheory.Functor J (FGModuleCat k)) : CategoryTheory.CreatesColimit F (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))

The forgetful functor from FGModuleCat k to ModuleCat k creates all finite colimits.

instance FGModuleCat.instCreatesColimitsOfShapeModuleCatForget₂LinearMapIdCarrierObjIsFG {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] {k : Type u} [Ring k] : CategoryTheory.CreatesColimitsOfShape J (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))

instance FGModuleCat.instHasColimitsOfShapeOfFinCategory {k : Type u} [Ring k] (J : Type) [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] : CategoryTheory.Limits.HasColimitsOfShape J (FGModuleCat k)

instance FGModuleCat.instHasFiniteColimits {k : Type u} [Ring k] : CategoryTheory.Limits.HasFiniteColimits (FGModuleCat k)

instance FGModuleCat.instPreservesFiniteColimitsModuleCatForget₂LinearMapIdCarrierObjIsFG {k : Type u} [Ring k] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))