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

And hence FGModuleCat K has all finite limits.

Future work

After generalising FGModuleCat to allow the ring and the module to live in different universes, generalize this construction so we can take limits over smaller diagrams, as is done for the other algebraic categories.

Analogous constructions for Noetherian modules.

instance FGModuleCat.instFiniteDimensionalCarrierToRingToDivisionRingPiObjModuleCatModuleCategoryHasLimitOfHasLimitsOfShapeDiscreteDiscreteCategoryHasLimitsOfShape_discreteHasFiniteProducts_of_hasFiniteLimitsHasFiniteLimits_of_hasLimitsHasLimits'Of_fintypeFunctorIsAddCommGroupIsModule {k : Type v} [Field k] {J : Type} [Fintype J] (Z : J → ModuleCat k) [∀ (j : J), FiniteDimensional k ↑(Z j)] : FiniteDimensional k ↑(∏ fun j => Z j)

instance FGModuleCat.instFiniteDimensionalCarrierToRingToDivisionRingLimitModuleCatModuleCategoryCompFGModuleCatInstLargeCategoryFGModuleCatForget₂InstConcreteCategoryFGModuleCatInstLargeCategoryFGModuleCatModuleConcreteCategoryInstHasForget₂FGModuleCatModuleCatInstLargeCategoryFGModuleCatInstConcreteCategoryFGModuleCatInstLargeCategoryFGModuleCatModuleCategoryModuleConcreteCategoryHasLimitOfHasLimitsOfShapeHasLimitsOfShape_of_hasFiniteLimitsHasFiniteLimits_of_hasLimitsHasLimits'IsAddCommGroupIsModule {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] {k : Type v} [Field k] (F : CategoryTheory.Functor J (FGModuleCat k)) : FiniteDimensional k ↑(CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))))

Finite limits of finite dimensional vectors spaces are finite dimensional, because we can realise them as subobjects of a finite product.

def FGModuleCat.forget₂CreatesLimit {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] {k : Type v} [Field k] (F : CategoryTheory.Functor J (FGModuleCat k)) : CategoryTheory.CreatesLimit F (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))

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

instance FGModuleCat.instCreatesLimitsOfShapeFGModuleCatToRingToDivisionRingInstLargeCategoryFGModuleCatModuleCatModuleCategoryForget₂InstConcreteCategoryFGModuleCatInstLargeCategoryFGModuleCatModuleConcreteCategoryInstHasForget₂FGModuleCatModuleCatInstLargeCategoryFGModuleCatInstConcreteCategoryFGModuleCatInstLargeCategoryFGModuleCatModuleCategoryModuleConcreteCategory {J : Type} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] {k : Type v} [Field k] : CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))

instance FGModuleCat.instHasFiniteLimitsFGModuleCatToRingToDivisionRingInstLargeCategoryFGModuleCat {k : Type v} [Field k] : CategoryTheory.Limits.HasFiniteLimits (FGModuleCat k)

instance FGModuleCat.instPreservesFiniteLimitsFGModuleCatToRingToDivisionRingInstLargeCategoryFGModuleCatModuleCatModuleCategoryForget₂InstConcreteCategoryFGModuleCatInstLargeCategoryFGModuleCatModuleConcreteCategoryInstHasForget₂FGModuleCatModuleCatInstLargeCategoryFGModuleCatInstConcreteCategoryFGModuleCatInstLargeCategoryFGModuleCatModuleCategoryModuleConcreteCategory {k : Type v} [Field k] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget₂ (FGModuleCat k) (ModuleCat k))