Tuesday, December 6, 2022

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.

No comments:

Post a Comment