A PDF of this post is available on github.
Motivation
In this post I’ll be looking at a subcategory of that consists of polynomial functors in which the fibration is done over one fixed set
:
The reason for this restriction is that morphisms between such functors, which are called polynomial lenses, can be understood in terms of monoidal actions. Optics that have this property automatically have profunctor representation. Profunctor representation has the advantage that it lets us compose optics using regular function composition.
Previously I’ve explored the representations of polynomial lenses as optics in terms on functors and profunctors on discrete categories. With just a few modifications, we can make these categories non-discrete. The trick is to replace sums with coends and products with ends; and, when appropriate, interpret ends as natural transformations.
Monoidal Action
Here’s the existential representation of a lens between polynomials in which all fibrations are over the same set :
This makes the matrices “square.” Such matrices can be multiplied using a version of matrix multiplication.
Interestingly, this idea generalizes naturally to a setting in which is replaced by a non-discrete category
. In this setting, we’ll write the residues
as profunctors:
They are objects in the monoidal category in which the tensor product is given by profunctor composition:
and the unit is the hom-functor . (Incidentally, a monoid in this category is called a promonad.)
In the case of a discrete category, these definitions decay to standard matrix multiplication:
and the Kronecker delta .
We define the monoidal action of the profunctor acting on a co-presheaf
as:
This is reminiscent of a vector being multiplied by a matrix. Such an action of a monoidal category equips the co-presheaf category with the structure of an actegory.
A product of hom-sets in the definition of the existential optic turns into a set of natural transformations in the functor category .
Or, using the end notation for natural transformations:
As before, we can eliminate the coend if we can isolate in the second hom-set using a series of isomorphisms:
I used the fact that a mapping out of a coend is an end. The result, after applying the Yoneda lemma to eliminate the end over , is:
or, with some abuse of notation:
When is discrete, this formula decays to the one for polynomial lens.
Profunctor Representation
Since this poly-lens is a special case of a general optic, it automatically has a profunctor representation. The trick is to define a generalized Tambara module, that is a category of profunctors of the type:
with additional structure given by the following family of transformations, in components:
The profunctor representation of the polynomial lens is then given by an end over all profunctors in this Tambara category:
Where is the obvious forgetful functor from
to the underlying profunctor category$.
Leave a Reply