Just as a bimonoid is both a monoid and a comonoid in a compatible way, a ‘biring’ is both a commutative ring and a commutative coring in a compatible way.
A biring is a commutative ring equipped with ring homomorphisms called coaddition:
cozero:
co-additive inverse:
comultiplication:
and the multiplicative counit:
satisfying the usual axioms of a commutative ring, but ‘turned around’.
More tersely, and also more precisely, a biring is a commutative ring object in the opposite of the category of commutative rings (also known as the category of affine schemes).
Equivalently, a biring is a commutative ring equipped with a lift of the functor
to a functor
Birings form a monoidal category thanks to the fact that functors of this form are closed under composition. A monoid object in this monoidal category is called a plethory. A plethory is an example of a Tall–Wraith monoid.
The most important example of a biring is , the ring of symmetric polynomials. This is actually a plethory.
The biring is the Grothendieck group of the category of Schur functors, which is equivalent to the functor category
where is the permutation groupoid and is the category of finite-dimensional vector spaces over a field of characteristic zero. is also the Grothendieck group of
where we drop the finite-dimensionality restriction on our vector spaces and work with all of Vect.
This suggests that the biring structure of may emerge naturally from a ‘categorified biring’ structure on . In this section we sketch how such a categorified biring might be constructed, based on the assumption that there is a tensor product of cocomplete linear categories with good universal properties.
Namely, we assume that given cocomplete linear categories and , there is a cocomplete linear category such that:
There is a linear functor which is cocontinuous in each argument.
For any cocomplete linear category , the category of linear functors is equivalent to the category of linear functors that are cocontinuous in each argument, with the equivalence being given by precomposition with .
With any luck these two assumptions will let us show that for any categories and ,
where we use to denote the functor category.
Assuming all this, we obtain the following operations on the category :
Addition: form the composite functor
where the last arrow comes from postcomposition with
This composite is our addition:
It’s really just the coproduct in .
Multiplication: first form the composite functor
where the last arrow comes from postcomposition with
This composite is our multiplication:
Since this product preserves colimits in each argument, if we use the hoped-for universal property of the tensor product of cocomplete linear categories, we can reinterpret this as a cocontinuous functor
Coaddition: Form the composite functor
where the first arrow comes from precomposition with the addition operation on (a restriction of coproduct in FinSet), and the second comes from our hoped-for relation (1). This is our coaddition:
Comultiplication: Form the composite functor
where the first arrow comes from precomposition with the multiplication operation on (a restriction of product in FinSet), and the second comes from our hoped-for relation (1). This is our comultiplication:
The additive and multiplicative unit and counit may be similarly defined. Note that we are using rather little about and here. For example, the category of ordinary non-linear species, , should also become a categorified biring if there is a tensor product of cocomplete categories with properties analogous to those assumed for cocomplete -linear categories above. But we could also replace by any rig category. So, ‘biring categories’, or more precisely ‘birig categories’, should be fairly common.