Abelian categories of finite-dimensional linear modules

Kernels and cokernels of additive linear module functors are again additive and linear. Pointwise, a kernel embeds into its source and a cokernel is a quotient of its target. Finite-dimensionality and finite object support therefore pass to both constructions. Together with the previously constructed finite biproducts, this makes the linear-module category and its finite-dimensional, finite-support full subcategory abelian.

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

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

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

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

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

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