Finite-dimensional module categories satisfy the intrinsic finiteness conditions

The full subcategory $A\text{-}\mathrm{m}\mathrm{o}\mathrm{d}$ of $A\text{-}\mathbf{M}\mathbf{o}\mathbf{d}$ contains the zero module, and it is closed in $A\text{-}\mathbf{M}\mathbf{o}\mathbf{d}$ under finite biproducts, kernels and cokernels: direct sums of finite-dimensional modules are finite-dimensional with dimensions adding, by [F2]; the kernel of an $A$-linear map $M\to N$ is a $k$-subspace of the finite-dimensional $M$, hence finite-dimensional; and the cokernel $N\mathrm{/}\mathrm{im}f$ is a quotient of the finite-dimensional $N$ by a subspace, hence finite-dimensional with ${\dim }_k(N\mathrm{/}\mathrm{im}f)={\dim }_{k}N-{\dim }_k(\mathrm{im}f)$ by [F2].

Every simple object $S$ of $A\text{-}\mathrm{m}\mathrm{o}\mathrm{d}$ has a projective cover in the sense of Superfluous subobjects and projective covers in an abelian category: by the cover theorem [F5] there is a finite-dimensional projective module $Q$ and an epimorphism $\pi :Q\twoheadrightarrow S$ whose kernel is superfluous in the module sense, and by [F6] this is exactly a superfluous subobject of $Q$ in the general sense, so $\pi$ is an essential epimorphism with projective source, that is, a projective cover of $S$.

Because $A\text{-}\mathbf{M}\mathbf{o}\mathbf{d}$ is abelian by [F1] and $A\text{-}\mathrm{m}\mathrm{o}\mathrm{d}$ is a full subcategory containing the zero object and closed under finite biproducts, kernels and cokernels computed there, step 1.1 makes $A\text{-}\mathrm{m}\mathrm{o}\mathrm{d}$ an abelian subcategory of $A\text{-}\mathbf{M}\mathbf{o}\mathbf{d}$; by [F8] it is therefore itself abelian.

For finite-dimensional modules $M,N$ the hom-set ${\mathrm{Hom}}_A(M,N)$ is a $k$-subspace of $\mathcal{L}(M,N)$ by [F3], and $\mathcal{L}(M,N)$ is finite-dimensional with ${\dim }_k\mathcal{L}(M,N)=({\dim }_{k}M)({\dim }_{k}N)$; a subspace of a finite-dimensional space is finite-dimensional by [F2], and composition is $k$-bilinear by [F3], so $A\text{-}\mathrm{m}\mathrm{o}\mathrm{d}$ is a locally small $k$-linear category with finite-dimensional hom-spaces.

Every object $M$ of $A\text{-}\mathrm{m}\mathrm{o}\mathrm{d}$ has finite length and $\mathrm{\ell }(M)\le {\dim }_{k}M$. Induct on $d={\dim }_{k}M$. If $d=0$ then $M=0$ and the empty composition series witnesses finite length with $\mathrm{\ell }(M)=0$. If $d>0$, the set of dimensions of nonzero submodules of $M$ is a nonempty set of natural numbers, so by [L1] it has a least element $d_0\ge 1$, and some nonzero submodule $N\le M$ has ${\dim }_{k}N=d_0$; such an $N$ is simple, because for any nonzero $N^{\mathrm{\prime }}\le N$ the submodule $N^{\mathrm{\prime }}$ is also a nonzero submodule of $M$ with ${\dim }_k{N}^{\mathrm{\prime }}\ge d_0$ and ${\dim }_k{N}^{\mathrm{\prime }}\le {\dim }_{k}N=d_0$ by [F2], so ${\dim }_k{N}^{\mathrm{\prime }}=d_0$ and $N^{\mathrm{\prime }}=N$ by the equality case of [F2]. By [F2] the quotient $M\mathrm{/}N$ has ${\dim }_k(M\mathrm{/}N)=d-d_0<d$, so by the induction hypothesis $M\mathrm{/}N$ has finite length with $\mathrm{\ell }(M\mathrm{/}N)\le {\dim }_k(M\mathrm{/}N)$; the simple module $N$ has finite length with $\mathrm{\ell }(N)=1$, so the additivity theorem [F4] gives that $M$ has finite length and $\mathrm{\ell }(M)=\mathrm{\ell }(N)+\mathrm{\ell }(M\mathrm{/}N)=1+\mathrm{\ell }(M\mathrm{/}N)\le 1+(d-d_0)\le d$.

Every simple left $A$-module is isomorphic to a composition factor of the regular module ${}_{A}A$, and there are finitely many isomorphism classes of simple modules. The algebra $A$ is a finite-dimensional left $A$-module, so by step 3.1 it has a composition series $0=A_0<A_1<\cdots <A_m=A$. Let $S$ be a simple left $A$-module and $0\mathrm{\ne }s\in S$; the map $\phi :A\to S$, $\phi (a)=as$, is $A$-linear with $\phi (1)=s\mathrm{\ne }0$, so its image is a nonzero submodule of the simple module $S$ and $\phi$ is surjective. Let $j\in \{1,\dots ,m\}$ be least with $\phi (A_j)\mathrm{\ne }0$, which exists because $\phi (A_m)=S\mathrm{\ne }0$ and the set is finite; then $\phi (A_{j-1})=0$, and $\phi (A_j)$ is a nonzero submodule of $S$, hence equals $S$, so the restriction of $\phi$ to $A_j$ is surjective with kernel containing $A_{j-1}$ and therefore factors through the quotient $A_j\mathrm{/}{A}_{j-1}$ by [F7], giving a nonzero surjection $A_j\mathrm{/}{A}_{j-1}\to S$; the source is simple, so this surjection is an isomorphism, whence $S\cong A_j\mathrm{/}{A}_{j-1}$. Thus every simple module is isomorphic to one of the $m$ composition factors of ${}_{A}A$, so there are at most $m$ isomorphism classes of simple modules.

Steps 2.1, 2.2 and 3.1 make $A\text{-}\mathrm{m}\mathrm{o}\mathrm{d}$ a locally small $k$-linear abelian category in which every object has finite length and every hom-space is finite-dimensional over $k$, that is, a locally finite $k$-linear abelian category; step 1.2 gives every simple object a projective cover, and step 4.1 shows that there are finitely many isomorphism classes of simple objects; hence $A\text{-}\mathrm{m}\mathrm{o}\mathrm{d}$ is a finite $k$-linear abelian category in the intrinsic sense of Finite k-linear abelian categories. The further claims are steps 4.1 and 3.1. All selections in the proof are made inside finite-dimensional objects (a nonzero submodule of least dimension and a composition series of the finite-dimensional algebra), so no choice principle is used.