The enriched presheaves framework

The Locus computer algebra system is going to be centered around the idea of presheaf theory. It is our claim that presheaves make for the best models of computation, and presheaves can be a unifying fabric for logical and functional programming. Logic programming is modeled using the topos $Sets$ and functional programming is modeled using $Sets^{\to}$.

With this initial effort, we saw that a number of presheaf topos $Sets^{C}$ had interesting properties. MSets and their topoi $Sets^M$ could be used to model the fundamental properties of monoids and their Green's relations through their subobject lattices. Categories can be described by the topos of compositional quivers or by simplicial sets using the nerve construction.

However, there is only so far you can go with this construction without considering other types of functors, like structure presheaves. This leads to the enriched presheaves framework in particular. I have in mind as part of this framework that modules, left modules, right modules, and bimodules should be considered to be types of Ab-enriched presheaves. This will allow more of our fundamental constructions to be integrated into the presheaf theoretic and sheaf theoretic world view.

First examples of enriched categories:
Let $Cat$ be the category of categories and functors. Then $Ord$, $CMon$, and $Ab$ are closed subcategories of $Cat$, and it follows naturally from this that they are self-enriched. So these form the most fundamental examples of enriched categories:

• Locally ordered categories: categories enriched in $Ord$
• Ringoids: categories enriched in $Ab$
• Semiringoids: categories enriched in $CMon$

Each of the categories $Ord$,$CMon$, and $Ab$ are also concrete: so abelian presheaves, preordered presheaves, and presheaves of commutative monoids are all examples of structure presheaves. Now using their enriched category structure we can form modules as special types of structure presheaves.

The general framework
The general framework is for defining an enriched category over a monoidal category, also called a $V$-enriched category. In particular, every cartesian monoidal category is a monoidal category $V$ which can be used to form enriched categories. Then a $V$-enriched structure presheaf is a functor from a $V$ enriched category to a $V$ enriched concrete category. If $V$ is a concrete closed category, then $V$ enriched functors to $V$ are used to form modules.

Modules as structure presheaves:
Rings in general are partially commutative, with totally commutative rings being a special case (*). In order to deal with this most general context, we need to deal with differences between left and right composition. This leads to notions of left and right modules, which fortunately can be handled nicely be the structure copresheaves framework.

• Left modules: $Ab$-enriched copresheaves of abelian groups
• Right modules: $Ab$-enriched presheaves of abelian groups
• Bimodules: $Ab$-enriched profunctors of abelian groups
• Modules: the same as left modules except that the source category $R$ is a commutative ring

How fortuitous that we already have presheaf-theoretic counterparts for each of the different types of modules. Left modules are just copresheaves, right modules are presheaves, and bimodules are profunctors.

Sets	Ab
Left modules	Copresheaves
Right modules	Presheaves
Bimodules	profunctors

This means in effect that whilst left modules, right modules, and bimodules are to be treated the same as in any other computer algebra system, in a presheaf based computer algebra system, we can in addition implement for them the methods get-object, get-morphism, get-set, and get-function so that they can optionally be treated as structure copresheaves as well. This will be a strictly advantageous result.

Semimodules as structure presheaves:
The same approach as for modules works for semimodules, if we replace all the enriched categorical machinery of $Ab$ with $CMon$. In fact, this will work for any similarly closed category.

• Left semimodules: $CMon$-enriched copresheaves of commutative monoids
• Right semimodules: $CMon$-enriched presheaves of commutative monoids
• Bisemimodules: $CMon$-enriched profunctors of commutative monoids
• Semimodules: the same as left semimodules except the source category is a commutative semiring

The generalisation of modules to semimodules is necessary because a great number of constructions in modern mathematics are based upon semirings. For instance, the ideals of a commutative ring form an idempotent semiring.

Presheaves of preorders:
In our presheaf theoretic foundations, we have already made presheaf versions of most categorical constructions. In particular, we can generalize the lattice of preorders on a set to the lattice of preorders on a presheaf.

Definition. let $F$ be a presheaf then $Ord(F)$ is its lattice of preorders. Its objects are presheaves of preorders with underlying presheaf $F$ with the join and meet defined componentwise.

Another construction is that for any given preorder $P$ we can form its condensation which is a partial order. This generalizes to preorderd presheaves, so that for any presheaf we can form its condensed presheaf of partial orders by composition with the condensation functor.

Definition. let $F$ be a presheaf of preorders then $C(F)$ is its underlying presheaf of partial orders.

We previously considered the idea of a locally ordered category. A special case is a locally ordered monoid. We can form modules over locally ordered monoids, in a similar manner to rings using this structured presheaf framework, and the same technique is even applicable to locally ordered categories.

Definition. let $C$ be a locally ordered category. Then a left module over $C$ is simply a $Ord$ copresheaf of partial orders well a right module is an $Ord$ enriched presheaf of partial orders.

In particular, let $M$ be a locally ordered monoid. Then as a monoid it has left and right MSets define over it. In the case that $M$ is locally ordered, these further form $Ord$ enriched presheaves of partial orders, which are order modules. These are analogous to the left and right induced modules over rings. Most modules over ordered monoids can be formed this way, or by their restrictions by change of index functors defined by monotone monoid homomorphisms.

References:
[1] Enriched categories

[2] Enriched functor

[3] Categorical algebra

[4] Presheaves

[5] Copresheaves

[6] Profunctors