Introduction
Mathematical objects can often be described in several ways, each description usually offering a different perspective and serving a different purpose.
For example, group rings - the subject of this post - can be described in two very different ways. Given a group G and a ring R, one way to think of the group ring R[G] is as the space of functions from G to R having finite support, with addition being pointwise and multiplication given by convolution. Another description of elements of R[G] is as finite formal linear combinations of group elements with coefficients in the ring R.
This kind of flexibility in the choice of a definition can however be a constraint in formalisation, as one might end up proving the same result multiple times - each time with a different representation of the underlying object. It is therefore desirable to have a "meta-theorem" that states that theorems proved for one representation are valid for a different representation of the object (theorems can be "transported" across isomorphisms this way in the framework of Homotopy Type Theory, from what I understand), or even better, to have an abstract and conceptual description of the underlying object that does not depend on how it is represented. In the second case, one can prove all results using the abstract description of the object and then simply show that a particular concrete representation satisfies the abstract property.
The rest of this post is about one such abstract description of group rings in the language of category theory.
Some Category theory
This post assumes some familiarity with categories, functors, natural transformations and other fundamental notions in category theory. Some of the other concepts that will be used are described below.
Group actions
A category comes equipped with an identity morphism for each object, together with a composition operation on compatible morphisms. The situation is even better in the case of a category with a single object, where any pair of morphisms can be composed. This leads to the natural definition of a group as a single-object category where every morphism is an isomorphism (i.e., every morphism is invertible). The elements of the group are the morphisms of the single-object category, and the group operation is composition of morphisms.
Thinking of a group as an entire category may be strange, but it has its advantages. For instance, a group action on a set is just a functor from the single-object category associated with the group to the category of sets. Similarly, a group representation is a functor from the category to the category of vector spaces over a chosen field.
Functor categories
Functors are maps between categories, and natural transformations are maps between functors with the same source and target. In some sense, a natural transformation is a "morphism" between functors. This intuition is made precise through the definition of the functor category.
If C and D are categories, the functor category D^C has objects as functors from C to D and morphisms as natural transformations. Continuing the earlier examples, the category of all representations of a group G over is simply the functor category where the source category is the group G (thought of as a single-object category) and the target is the category of vector spaces over the complex numbers.
Initial objects
An initial object of a category is one that has a unique morphism to every object of the category. In the category of groups, for example, the initial object is the trivial group.
It follows from this description that any two initial objects of a category must be unique up to a unique isomorphism.
A category-theoretic description of a group ring
Given a ring R and a group G, the objective is to give an abstract description of the group ring R[G].
The category of R-algebras, where the objects are R-algebras and the morphisms are R-algebra homomorphisms, will serve as the starting point. To bring the group G into the picture, consider G-actions on R-algebras.
As mentioned earlier, an action of the group G on an R-algebra can be considered as a functor from the group (treated as a single-object category) to the category of R-algebras. Studying all such actions on R-algebras at once amounts to constructing the functor category with the source of the functors being the group and the target being the category of R-algebras.
The claim now is that the group ring R[G] is nothing but the initial object in this functor category.
To see this, we must first show that the group ring R[G] actually lies in this category. This however follows from the natural multiplicative structure of R[G]. Next, consider any element of the above category, which is essentially an R-algebra together with a group action.
To show that there is a unique map from R[G] to this R-algebra, we first deduce the properties that such a homomorphism must satisfy and then observe that it forces there to be unique map. An arbitrary word $\sum_{i} r_{i}g_{i}$ of R[G] is mapped by a homomorphism $\phi$ to $\phi(\sum_{i} r_{i}g_{i}) = \sum_{i} \phi(r_{i}g_{i})$. However, the map $\phi$ is $G$-equivariant as it is a morphism in the functor category, and hence a natural transformation between the corresponding functors. Therefore, the expression $\sum_{i} \phi(r_{i}g_{i})$ is equal to $\sum_{i} \phi(r_{i}) g_{i}$. Since all the $r_{i}$ are scalars coming from the ring R, they must be fixed by the $R$-algebra homomorphism $\phi$. Therefore, any homomorphism from R[G] to an object is essentially uniquely determined, and is a valid homomorphism.
TODO The thought process
The process of ariving at the above result was far messier than presented. This section will present some of the ideas that eventually led to the above formulation (it has been a few days since I first came up with this, so some details will be missing).