class CategoryTheory.FiniteModuleCategory (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [LeftModuleCategory C M] : Type (max u₁ v₁)

A finite module category over C: an abelian left C-module category with enough projectives, together with a representing algebra repAlg : Mon C so that M is equivalent to modules over repAlg.

• abelianM : Nonempty (Abelian M)
• enoughProjM : EnoughProjectives M
• repAlg : Mon C

theorem CategoryTheory.moduleFunctorCategoryAbelian {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : Type u₂} [Category.{v₂, u₂} M] [LeftModuleCategory C M] [FiniteModuleCategory C M] {N : Type u₃} [Category.{v₃, u₃} N] [LeftModuleCategory C N] [FiniteModuleCategory C N] : Nonempty (Abelian (ModuleFunctor C M N))

The category of module functors between two finite left C-module categories is itself abelian.