Finite biproducts of finite-dimensional modules

Finite products of additive linear functors are again additive and linear. For a finite family of finite-dimensional modules, the pointwise product is finite-dimensional and its object support is contained in the finite union of the supports of the factors. Consequently both the linear-module category and its finite-dimensional full subcategory have finite biproducts.

theorem MagnitudeConjecture.CoveringHom.isLinearModule_limit {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {J : Type} [Finite J] (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Functor C (ModuleCat k))) [CategoryTheory.Limits.HasLimit F] (hF : ∀ (j : CategoryTheory.Discrete J), IsLinearModule k (F.obj j)) : IsLinearModule k (CategoryTheory.Limits.limit F)

A finite product of additive linear module-valued functors is additive and linear.

instance MagnitudeConjecture.CoveringHom.isLinearModule_closedUnderFiniteProducts {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : (IsLinearModule k).IsClosedUnderFiniteProducts

instance MagnitudeConjecture.CoveringHom.linearModuleCategory_hasFiniteBiproducts {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : CategoryTheory.Limits.HasFiniteBiproducts (LinearModuleCategory k)

instance MagnitudeConjecture.CoveringHom.linearModuleCategory_hasBinaryBiproducts {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : CategoryTheory.Limits.HasBinaryBiproducts (LinearModuleCategory k)

instance MagnitudeConjecture.CoveringHom.isFiniteDimensionalModule_closedUnderFiniteProducts {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : (IsFiniteDimensionalModule k).IsClosedUnderFiniteProducts

instance MagnitudeConjecture.CoveringHom.finiteDimensionalModuleCategory_hasFiniteBiproducts {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : CategoryTheory.Limits.HasFiniteBiproducts (FiniteDimensionalModuleCategory k)

instance MagnitudeConjecture.CoveringHom.finiteDimensionalModuleCategory_hasBinaryBiproducts {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : CategoryTheory.Limits.HasBinaryBiproducts (FiniteDimensionalModuleCategory k)