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

Locus 1.5

Locus 1.5 has been pushed to github. I would say the impetus for the recent series of changes was so that I could implement various categorical adjunctions that generalize images/inverse images. Towards that end, I have a multimethod for images and preimages which dispatches its arguments based upon the type of both of its values. So we have that images can be formed from various function-like objects applied to various mathematical objects.

• Set images are applicable to partial functions and multi-valued functions as well as ordinary functions. The image of a set under a multivalued function or set relation can be formed by the image multimethod.
• In most textbooks on category theory there is a mention of the topos $Quiv$ of binary quivers, which consists of two parallel functions from the edge set to the vertex set. I have generalized this to ternary quivers, and indeed all the way to nary quivers. The nary quivers implementation is new in this version.
• Given any nary quiver there are set images and inverse images: the set image of a set of edges in a nary quiver is the union of the sets of vertices in each edge, or in other words the union of all set images of the set under each component function. Inverses images are uniquely defined so that they form an adjunction.
• I implemented two new concepts for completions sake: partial quivers and hyperquivers. A hyperquiver is a functor from the parallel arrows category $T_{2,n}$ but to $Rel$ instead of $Sets$. Partial quivers are defined the same way but using te subcategory of partial functions. Set images under hyperquivers are formed by the union of all set images produced by all hte multivalued functions of the hyperquiver.
• Set images are defined for MSets and so instances of the MSet class implement the image multimethod now. The image of a set under an MSet is the set of all outputs of all actionts on the MSet applied to all elements of the set. Inverse images are defined dually so they form an adjunction.
• Images and inverse images are defined for set partitions. So that given a function you can apply it to a SetPartition rather then a set and you will get the appropriate set partition as an output using the image multimethod. This implements the adjunction between partition images and inverse images.
• Likewise, given any preorder you can apply it to a function instead of a set to get the preorder image or inverse image.
• The adjointness definition of continuous maps is defined by topological images/inverse images. So given a member of the TopologicalSpace class, it is interpreted properly by the image method to get an output topological space which is the maximal topological space which makes that map continuous. Topological inverse images are also defined so this forms an adjunction. So images/inverse images work in the most contexts possible now.
• A new class of copresheaves: Galois copresheaves is implemented now. These are just Galois connections without any reference to any underlying ordering.
• A new order theory framework integrating adjunctions is provided. New classes for residuated maps, coresiduated maps, and Galois connections are defined. The framework for supporting adjunctions has been greatly improved, motivated by this work on images and inverse images.
• Finally, new support for ordered algebraic structures is provided by new classes. These will be the first step towards algebraic structures like quantales which can always be formed from any algebraic structure using images and inverse images.

The implementation of the images/preimages framework is a good and necessary first step. A great many categories are defined by image/inverse image adjunctions, but the next steps will see us further improve the support for structure presheaves. Structure presheaves are our main focus.