English
For a diagram F: J ⥤ FGModuleCat(k) with J finite and k Noetherian, the limit's carrier is finite over k.
Русский
Для диаграммы F: J ⥤ FGModuleCat(k) с конечным J и k Ноетеровской, носитель предела конечен над k.
LaTeX
$$$\operatorname{Module.Finite}_k(\operatorname{limit}(F \circ \forget_2(FGModuleCat(k), ModuleCat(k))).carrier)$$$
Lean4
/-- Finite limits of finite-dimensional vector spaces are finite dimensional,
because we can realise them as subobjects of a finite product. -/
instance (F : J ⥤ FGModuleCat k) :
Module.Finite k (limit (F ⋙ forget₂ (FGModuleCat k) (ModuleCat.{v} k)) : ModuleCat.{v} k) :=
haveI : ∀ j, Module.Finite k ((F ⋙ forget₂ (FGModuleCat k) (ModuleCat.{v} k)).obj j) := by intro j;
change Module.Finite k (F.obj j); infer_instance
Module.Finite.of_injective (limitSubobjectProduct (F ⋙ forget₂ (FGModuleCat k) (ModuleCat.{v} k))).hom
((ModuleCat.mono_iff_injective _).1 inferInstance)
