In a topos, is the category of internal $R$-modules abelian for $R$ commutative and unitary?

Question

Let $\mathcal E$ be a topos and $R$ be a commutative unitary ring object in it. Let $R$-$\mathsf{Mod}$ be the category of (internal) $R$-modules. Is this category abelian? Does it at least have biproducts? Is it maybe even Grothendieck abelian?

I ask because using the internal language we have an easy morphism $R^m\to R^{m+n}\cong R^m\times R^n$ which seem like a coproduct injection, but I'm not sure how to prove the universal property.

Answer 1

The answer was hiding in Johnstone's Topos Theory, chapter 8, theorem 8.11. The statement there is for the category of internal abelian groups, but the same argument seems to work for $R$-modules.

Theorem.

• For any topos $\mathcal E$, with commutative unitary ring object $R$, the category $R$-$\mathsf{Mod}$ of internal $R$-modules is abelian;
• If $\mathcal E$ has a natural number object, $R$-$\mathsf{Mod}$ is monadic over $\mathcal E$;
• If $\mathcal E$ is a Grothendieck topos, $R$-$\mathsf{Mod}$ is a Grothendieck abelian category with a generator.