Small projective modules are exactly finitely generated projective modules; the progenerator identification

(Finitely generated implies coproduct preservation.) Assume $P$ is finitely generated, with finite generating set $S=\{x_1,\dots ,x_n\}$, so every element of $P$ is a finite $B$-linear combination of the $x_j$ by [F3]. Let $Y={⨁}_i{Y}_i$ be a set-indexed direct sum in $B$-Mod and let $f:P\to Y$. Each $f(x_j)$ has finite support by [F4], so the union $F$ of the finitely many supports is finite and $f(x_j)\in {⨁}_{i\in F}{Y}_i$ for every $j$; since the $x_j$ generate $P$ and the submodule ${⨁}_{i\in F}{Y}_i$ contains all their images, $f$ factors through the inclusion ${\mathrm{ȷ}}_F:{⨁}_{i\in F}{Y}_i\to Y$. The canonical comparison $c:{⨁}_i{\mathrm{Hom}}_B(P,Y_i)\to {\mathrm{Hom}}_B(P,Y)$, $(u_i)\mapsto {\sum }_i{\mathrm{ȷ}}_i\circ u_i$, has components ${\pi }_i\circ c(u)=u_i$ by [F4] and [F10], so $c$ is injective; and for arbitrary $f$ the finite-support family $({\pi }_i\circ f{)}_i$ satisfies $c(({\pi }_i\circ f{)}_i)={\sum }_i{\mathrm{ȷ}}_i\circ {\pi }_i\circ f=f$ by [F4], so $c$ is surjective. Hence ${\mathrm{Hom}}_B(P,-)$ preserves this coproduct, and projectivity of $P$ was not used.

(Coproduct preservation and projectivity imply finite generation.) Assume $P$ is projective and ${\mathrm{Hom}}_B(P,-)$ preserves every set-indexed coproduct. Let $\epsilon :B^{(P)}\to P$ be the canonical surjection of [F6] from the free module on the underlying set of $P$, and let $s:P\to B^{(P)}$ be a section of $\epsilon$, which exists because $P$ is projective: lift the identity of $P$ through the epimorphism by [F2]. Smallness identifies ${\mathrm{Hom}}_B(P,B^{(P)})$ with ${⨁}_{p\in P}{\mathrm{Hom}}_B(P,B)$ under the comparison, so the family ${\phi }_p:={\pi }_p\circ s$ has finite support: there is a finite subset $F\subseteq P$ with ${\phi }_p=0$ for $p\mathrm{\notin }F$. For every $x\in P$ the element $s(x)$ has support contained in $F$ by [F4], so $x=\epsilon (s(x))={\sum }_{p\in F}{\phi }_p(x)p$ is a finite $B$-linear combination of the finitely many elements $p\in F$; by [F3] the module $P$ is generated by $F$, hence finitely generated. No infinite choice is used: the section $s$ is a single existential instance and the set $F$ is computed from it.

(Proof of (1).) Step 1.1 gives "finitely generated $\Rightarrow$ coproduct-preserving" and step 1.2 gives "projective and coproduct-preserving $\Rightarrow$ finitely generated"; combining them, a left $B$-module $P$ is projective with ${\mathrm{Hom}}_B(P,-)$ preserving every set-indexed coproduct if and only if $P$ is finitely generated and projective. Neither direction uses projectivity of an infinite free module or any choice principle.

(Proof of (3).) The regular module ${}_{B}B$ is the free module on the one-element set $\{1_B\}$ by [F7], so it is finitely generated, and it is projective by [F8] with a one-element basis, where finite choice suffices and no AC is needed. By step 1.1 the functor ${\mathrm{Hom}}_B(B,-)$ preserves every set-indexed coproduct. Evaluation at $1_B$ identifies ${\mathrm{Hom}}_B(B,Y)\cong Y$ naturally by [F7], so ${\mathrm{Hom}}_B(B,-):B\text{-Mod}\to \mathbf{A}\mathbf{b}$ is naturally isomorphic to the faithful underlying-additive-group functor: if $u\mathrm{\ne }v:X\to Y$, choose $x$ with $u(x)\mathrm{\ne }v(x)$ and the map $B\to X$, $b\mapsto bx$, distinguishes their postcompositions; hence ${}_{B}B$ is a generator by [F9] applied in the locally small abelian category $B$-Mod with AB3, which is cocomplete by [F5]. Therefore ${}_{B}B$ is a small projective generator.

(Proof of (2).) By [F1] both a small projective generator and a progenerator include the condition of being a generator, and $B$-Mod is a locally small cocomplete abelian category by [F5] whose coproducts are the direct sums of [F4]; the remaining conditions are "projective and coproduct-preserving" on the one side and "finitely generated and projective" on the other, which step 2.1 shows to be equivalent. Hence a left $B$-module $P$ is a small projective generator of $B$-Mod if and only if it is a progenerator.

Steps 2.1, 2.2 and 3.1 prove the three assertions: the smallness criterion for projective modules, the progenerator identification, and the regular module example. The only module projectivities used are those of $P$ itself, given in the hypothesis, and of the free module on one generator; no commutativity of $B$ is assumed and no choice principle is used.