First note that every -module is an abelian group under addition by definition, and every -linear map is a group homomorphism. Thus there exists a “forgetful functor” (which turns out not to be forgetting anything)

Now every abelian group admits a -action, where for and we say

which is easily verified to satisfy all properties of a -module. Thus we have a functor

where and , hence the categories are isomorphic.