Restriction of finite-dimensional linear modules

Precomposition along a linear functor whose source has finitely many objects restricts finite-dimensional modules to finite-dimensional modules.

def MagnitudeConjecture.CoveringHom.finiteLinearModuleRestrictionFunctor {k : Type v} [Field k] {C : Type uC} {D : Type uD} [CategoryTheory.Category.{v, uC} C] [CategoryTheory.Category.{v, uD} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] [Fintype C] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] : CategoryTheory.Functor (FiniteDimensionalModuleCategory k) (FiniteDimensionalModuleCategory k)

Restriction of finite-dimensional linear modules along a linear functor with finite source.

instance MagnitudeConjecture.CoveringHom.finiteLinearModuleRestrictionFunctor_additive {k : Type v} [Field k] {C : Type uC} {D : Type uD} [CategoryTheory.Category.{v, uC} C] [CategoryTheory.Category.{v, uD} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] [Fintype C] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] : (finiteLinearModuleRestrictionFunctor F).Additive

instance MagnitudeConjecture.CoveringHom.finiteLinearModuleRestrictionFunctor_linear {k : Type v} [Field k] {C : Type uC} {D : Type uD} [CategoryTheory.Category.{v, uC} C] [CategoryTheory.Category.{v, uD} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] [Fintype C] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] : CategoryTheory.Functor.Linear k (finiteLinearModuleRestrictionFunctor F)

instance MagnitudeConjecture.CoveringHom.finiteLinearModuleRestrictionFunctor_preservesKernel {k : Type v} [Field k] {C : Type uC} {D : Type uD} [CategoryTheory.Category.{v, uC} C] [CategoryTheory.Category.{v, uD} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] [Fintype C] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Functor.Linear k F] {X Y : FiniteDimensionalModuleCategory k} (f : X ⟶ Y) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) (finiteLinearModuleRestrictionFunctor F)

Restriction of finite linear modules preserves kernels. After forgetting the two full-subcategory layers, this is the pointwise fact that precomposition preserves limits.