Friday, September 2, 2022

Locus 1.1.0

A new release of Locus has been pushed to github, which includes several features involving elementary topos theory.
  1. The readme was changed to focus on topos theory and commutative algebra. In particular, order theory, semigroup theory, and monoid theory are de-emphasized and categories are emphasized more.
  2. The topos theory of hypergraphs was greatly developed in this version as well as the idea of subobjects and quotients of the span copresheaf topos. The special case of incidence structures, which are flag distinguishing spans were studied. The flag distinguishing spans are a subcategory of the span topos that is subobject closed, however, it is not quotient closed. To get around this, we defined the together injective quotient of a span copresheaf which always produces a flag distinguishing quotient. This function is a suborder producing map on the congruence lattice of a span copresheaf.
  3. A corresponding topos theory of cospans was devised based upon the dual category of the index category of the span copresheaf topos. This is nice for adding a degree of completion to the basic copresheaf theory.
  4. The use of diamond copresheafs was further developed, which is extended from the copresheaf theory of morphisms of functions. When I first studied topos theory of $Sets^{\to}$, much like in the standard textbooks I treated morphisms of functions as morphisms rather then as another class of copresheaf. The decision to apply categorical logic to them was an original innovation of mine. Now I have extended the theory of the diamond topos with functors to the span and cospan topos, as well as dual functors to the topos of triangles. In other other direction, methods were implemented for creating diamond copresheafs from spans and cospans using cartesian and cocartesian squares, which were interpreted from the stacks project. Another method of creating diamonds is defined by combining parallel triangle copresheaves.
  5. I place very special emphasis now on the fact that $Rel$ is a concrete category. This wasn't something that I was considering before, when I first started considering relations. I knew that $Rel$ would be of central importance, for example because of its use of dataflow analysis, but I didn't see how it would fit into the big picture. In this new implementation in Locus 1.1 the category $Rel$ is part of the concrete category framework. The new ImageFunction class handles the conversion of relations to functions. Relational functors are handled as part of the larger structure presheaves framework I am developing, which I think will work nicely as the whole point of Locus is that everything revolves around presheaves.
  6. The opposite category $Sets^{op}$ is also implemented as a concrete category embedded in $Rel$ so that the dual of a concrete category can again be considered to be concrete.
  7. I implemented a ComposablePath class which is designed to handle pairs of compatible morphisms in a category. The point of this class is that it handles the third kind of section of a compositional quiver copresheaf, which emerges in the copresheaf theory of categories. The copresheaf theory of categories is an original development of mine, which is a consequence of the copresheaf topos theory of everything that I am developing, so this is another original idea of mine.
  8. The impetus of the entire 1.0 series of Locus versions is going to be the structured presheaf framework. This means that rather it is a structured sets, structured function, structured pair of sets, structured pair of functions, a structure presheaf, a structure sheaf, sheaf of rings, or a scheme every single mathematical object is going to be treated as a structure placed over some presheaf. This provides us a much more flexible framework then focusing on structured sets alone and it fits well with the structure sheaves familiar from algebraic geometry. The first stages of the structured presheaf framework were implemented in this version of Locus by using the class hierarchy.
Topos theory is the key to solving the issues of logic-based artificial intelligence, and I am more certain of this then ever. Right now the focus is on improving this program.

No comments:

Post a Comment