Subobjects and quotients of thin quivers

Thin quivers are an important special case in presheaf topos theory. Suppose that we have a thin quiver $Q$ then we can form and consider its subobject and congruence lattices $Sub(Q)$ and $Con(Q)$ normally, but far more interesting is to consider subobjects and congruences of a thin quiver that remain thin.

Theorem 1. let $Q$ be a thin quiver, then every subobject of $Q$ is thin.

Proof. Thinness is a non-existence condition stating that there do not exist morphisms $m: A \to B$ and $n : A \to B$. Non-existence conditions are subset closed. $\square$

It is rather trivial that thin quivers are subobject closed, and that the subobjects of thin quivers are again thin. Of course, it also follows that any subcategory of a thin category is again thin. Far more interesting is the case of congruences of quivers that have thin quotients.

Lemma 1. let $Q$ be a thin quiver. Then $Q$ has no congruences that collapse two morphisms $m: A \to B$ and $n : C \to D$ without also equating two objects. $Q$ has a unique object-preserving partition.

Proof. $Q$ is a thin quiver it therefore follows that for the two morphisms $m$ and $n$ we must have either $A \not= C$ or $B \not= D$. Suppose that $A \not= C$ then we would have to equate $A$ and $C$ under the congruence so that would produce an equal pair of objects. Likewise, if $B \not= D$ then we would have to equate $B$ and $D$ also producing an equal pair of objects. So no two non-parallel morphisms can be equated under a thin quiver congruence. $\square$

This is the base case, which is that there is a unique congruence for the object partition that preserves all objects. Our goal is to show that there is a unique quiver congruence associated to every object partition.

Lemma 2. let $Q$ be a quiver, then the equivalence minimal congruence that turns $Q$ into a thin quiver $Thin(Q)$ is the congruence that equates all parallel pairs of morphisms in $Q$ and no objects. All other morphisms $f: Q \to T$ from $Q$ to a thin quiver factor through $Thin(Q)$.

Proof. let $Q$ be a quiver. Then in order for $Q$ to be thin there must not be any pairs of morphisms $m$ and $n$ with the property that $s(m) = s(n)$ and $t(m) = t(n)$. Thusly, to make $Q$ thin we can equate all such pairs of morphisms $m$ and $n$ to get the congruence $Thin(Q)$. This has as a quotient a thin quiver because it can not have any pairs $m$ and $n$ with $s(m) = s(n)$ and $t(m) = t(n)$ for if it did it would contradict the fact that we collapsed them. Then to see minimality, consider that any other congruence $C$ of $Q$ must also collapse all such pairs $m$ and $n$. It follows that $Thin(Q)$ is the minimal thin congruence. $\square$

With these two lemmas we now have have the means we need to prove our main theorem, which is that the thin congruences of a quiver are fully determined by object partitions.

Theorem 2. Let $Q$ be a quiver and $B$ a partition of its objects. Then there is a unique quiver congruence of $Q$ with $B$ its object partition that has a thin quotient.

Proof. there is always a unique quiver congruence associated to any object partition $B$ of a quiver $Q$: the congruence that collapses all objects in $B$ but no morphisms. We can always form this congruence by the pair $(id,B)$. Then the quotient of this congruence need not be thin. So by lemma 2 we can form a partition $A$ of the morphism set $E$ by equating all parallel edges which turns $\frac{Q}{(id,B)}$ into a thin quiver. This forms the following commutative diagram: Then also by lemma one, we see that every morphism from $Q$ to a thin quiver $T$ that goes through $B$ must filter through $\frac{Q}{(A,B)}$. However, by lemma one we know that no such further congruence can exist without further equating the objects of $B$. So $\frac{Q}{(A,B)}$ is the only thin quiver produced by a congruence with object partition $B$. It follows that thin congruences are fully determined by their object partitions. $\square$

If by theorem 2, we have that each object partition is uniquely associated to a thin congruence, then there is a one to one mapping $U : Con(Ob(Q)) \to Con(Q)$ that maps any object partition into a thin congruence.

Corollary. let $Q$ be a quiver then the suborder of $Con(Q)$ consisting of all thin congruences is isomorphic to the partition lattice $Con(Ob(Q))$ of partitions of the object set $Ob(Q)$.

It follows from this that the lattice of thin congruences of $Q$ is simply a partition lattice. We can further consider the thin mapping we defined in lemma 2 to be a closure operation on $Con(Q)$.

Corollary. $Thin: Con(Q) \to Con(Q)$ is a closure operation on the lattice of congruences of a quiver $Con(Q)$ that maps any congruence to its thin component.

The relevance of this result is that we can understand the epi-mono factorisations in the full subcategory of the topos $Quiv$ of thin quivers. We see from this that every morphism of directed graphs is determined by a vertex partition on the one hand a subset of vertices and edges on the other. The interesting thing about this is that it produces a dichotomy between congruences and subobjects, where only the later requires both object and morphism components.

Of particular interest is the application of this theory to considering subobjects and congruences of binary operations, which can simply be considered to be quivers with an algebraic function operation adjoined to them in the topos $Sets^{T_{2,3}}$ of ternary quivers. This leads into a more advanced topos theoretic theory of algebraic operations and their subobjects and congruences, which will be helpful in defining the topos theoretic foundations of algebra.

We see that topos theory provides the best foundation for combinatorics because topoi like $Quiv$ let you reason logically about graphs, digraphs, etc. $Sets^{[1,2]}$ lets you reason about hypergraphs. In order to make it the best foundation for abstract algebra we need to consider other topoi like $Sets^{T_{2,3}}$. In order to use topoi in geometry, as was originally intended, we can consider topoi of sheaves $Sh(X)$ of topological spaces. Every branch has its own topoi available for further study, which makes topos theory such an exciting field for further research and analysis.

References:
Quiver in nlab
Topoi: The Categorial Analysis of Logic

Congruence lattices of quivers

Let $Q$ be a multi-directed graph, then $Q$ is associated to a lattice of congruences $Con(Q)$ which can be constructed using new and original algorithms of mine. A quiver can be seen as a presheaf over the following category: This category I call the double arrow category, because it has a repeated pair of arrows going from the first object to the second one. As a category, it has an underlying quiver $Q$. Its congruence lattice $Con(Q)$ looks like this: This defines the congruence lattice of a multi-directed graph, but the same could be applied to any directed graph without repeated edges. Consider the directed cycle graph $C_3$ on three elements: Then the congruence lattice of the directed cycle graph $Con(C_3)$ has this interesting structure: This different sort of congruence lattice for $Con(C_3)$ might look unexpected at first, but actually it makes perfect sense. It is formed by adjoining two different five elements congruence lattices of a three element set to one another. Recall that the congruence lattice $Con(S)$ of a set with three elements has the structure [1,3,1] and that it has five elements. The reason for this appearance is that the cycle $(0,1),(1,2),(2,0)$ has this unique property is that every vertex is in any two of its edges. Therefore, in order to form any congruence of $C_3$ you must first collapse all of its vertices.

We have shown that every directed multigraph is associated with a congruence lattice $Con(Q)$, but let us not forget that every object of a congruence lattice is associated with a quotient. In the case of $C_3$ all of the different congruences of the same size and height have the same quotient, and so all the different quotients of $C_3$ can be formed one after another. They are formed in five steps: starting with $C_3$, collapsing a pair of objects, then collapsing another pair of objects, then collapsing a pair of morphisms, then collpasing the last pair of morphisms.

We have now seen the congruence lattice $Con(C_3)$ of a directed cycle graph on three elements as well as all of its quotients. It had the unique structure of a weak order. It would be interesting to see if $C_4$ has the same structure of congruences: Then the congruence lattice of $Con(C_4)$ looks as displayed below. It does not have the property that it is two partition lattices adjoined to one another, because it doesn't have the property that any vertex is contained in any pair of edges. Nonetheless, you still have to collapse at least three objects before you can collapse one edge, so you can still visibly see the fifteen element partition lattice on four elements on the bottom connected to another one above it but now with some mixed congruences between them:

Another directed graph with an interesting congruence lattice is the strict total order $T_3$. It has a congruence lattice $Con(T_3)$ as displayed below. The reason for this interesting structure is that when you collapse two lower objects you then get repeated edges from the lower class to the upper one. These repeated edges can then be collapsed without equating more objects, and the same works in the other direction from above. So you get this interesting self dual structure in the form of a lattice. We have considered some interesting cases of directed graphs, but what if you have a repeated edges. In that case, we can see that repeated edges actually do have an effect on the appearance of the congruence lattice. A directed multigraph with repeated edges has as an atomic congruence a partition that equates two parallel edges rather then two vertices. So the atoms of such a congruence lattice don't necessarily generate a partition lattice, so they appear different. This is a non-thin quiver, so it has an atomic congruence that is not part of any partition lattice. It is the unique atom that is not a part of an element that covers three atoms. Consider two disconnected edges: Then their congruence lattice is displayed below. Initially, it just looks like a partition lattice on four elements, but there is a little bit more that meets the eye. There is one special congruence on the disconnected pair of edges: the one that equates both the minimal edges and that equates both the maximal edges. Then the two arrows can also be equated to get a parallel pair between two objects as a quotient. The disjoint arrows map is a function, but it is perhaps not a transformation because it is not closed. But we can make it one like this: Simply adding these two edges creates a much larger congruence lattice, which demonstrates how these congruence lattices tend to grow quite large for even small directed graphs: Topos theory generates congruence lattices for far more objects then classical lattice theory, which would only generated them for lattices or semilattices. We can now generate them for any poset. Consider the following poset: This poset is known as $[1,2]$ and its congruence lattice $Con([1,2])$ is of the following form: These congruence lattices are already getting quite larger. We can certainly go deeper, and create congruence lattices for even larger directed graphs and we can even run computations on them, but they will get too big for Graphviz to display nicely I think so we'll have to leave it at this. The congruence lattices generted so far should give you an inkling of the subject.

All these congruence lattices were generated by using the topos $Quiv$. This is just a small sampling of what can be done with topos theory, within only part of one subject. Topos theory is a logical theory of everything, and its techniques are the most widely applicable.

Globular sets as models of (n,r)-categories

One of the concerns of mine is the presheaf theory of categories and higher categories, and the use of presheaf topoi to create models for higher categories. The basic presheaf topoi I would like to focus in on are the (n,r)-globular sets.

Definition. Let a 0-globular set be a set. Then an (n+1)-globular set is a quiver with an n-globular set as its hom classes.

So for example, a quiver is a 1-globular set and all of its hom classes are simply sets. A 2-globular set is simply a quiver such that each hom class is itself its own quiver. Equivalently, that means that a 2-globular set is like a 2-quiver with the condition that $s \circ t = s \circ s$ and $t \circ s = t \circ t$ so that all 2-morphisms are between parallel pairs of 1-morphisms. The relationship to topos theory is that these are presheaves over the globe category $G_n$.

Definition. let $G_n$ denote the nth globe category. This has source and target morphisms from (n+1)-morphisms to n-morphisms with the condition that $s \circ t = s \circ s$ and $t \circ s = t \circ t$ for each source and target morphism.

It follows that an n-globular set is actually an object of the presheaf topos $Sets^G_n$. It follows that we can use presheaf topos theory to reason about n-globular sets.

Proposition. the section preorder of an n-globular set is a height (e.g max chain length) n+1 partial order.

Proof. the n-globe category is an endotrivial partially ordered category, so it follows that the section preorder is a partial order. Its chains are determined by chains of n-morphisms followed by (n-1)-morphisms all the way to 0-morphisms. It follows that the chain can have length no more then $(n+1)$. $\square$

The subobject lattice $Sub(G)$ of a globular set $G$ in the topos $Sets^{G_n}$ is simply a distributive lattice of the max chain length n+1 partial order. The congruence lattice $Con(G)$ is formed in the standard way it is formed for any presheaf object in a topos. The first thing we see is that $Sets^{G_n}$ lacks identity morphisms so it is not a good model for n-categories. Instead it is a model for n-semicategories. To resolve this we define and implement unital n-globular sets.

Definition. we construct the unital n-globe category $U_n$ in the following manner:

• we have n-morphisms for all 0,...,n
• we have nth source and nth target morphisms for each m-morphism going to an (m-n) morphism. These are denoted $s^n$ and $t^n$
• we have nth identity morphisms $id^n$ that take an m-morphism to an (m+n) identity morphism
• every morphism in $U_n$ can canonically be represented as a pair of $id^n s^m$ or as a pair $id_n t^m$ representing the n-th identity morphism on an mth-source or an mth-target morphism.
• the composition of two morphisms $id^w s^x$ and $id^y t^z$ proceeds by canceling out as many identities as possible by removing pairs of $s$ and $id$. Then if identities are remaining they get $id^{y-x+w}$ by combining identity morphisms as the identity part in front of $t_z$. If $x > y$ then we cancel out $id^y$ and we get $id^w s^{x-z}$ because when we get $s^n$ composed with $t^n$ we combine the two with the source/target type the last to be called. So this can canonically define composition in the unital n-globe category.

It follows that a unital n-globular set is simply a copresheaf in the fundamental topos $Sets^{U_n}$. This presheaf definition may not be the exact one you always want so another approach is as follows:

Definition. a unital n-globular set can be defined from the data of a n-globular set as well as identity morphisms for each m-morphism with $m \lt n$. The identity morphisms for a morphism $m$ have the property that their source and target morphisms are both $m$.

We now have an underlying presheaf model for n-categories. The distinction between the two is readily apparent:

• A 2-semicategory can be defined as a compositionally enriched 2-globular set. An ordered semigroup, for example, is a 2-semicategory. As a not necessarily globular set, it doesn't require the definition of identities.
• A 2-category is a compositionally enriched unital 2-globular set. It has identity morphisms for each object, and two identity morphisms for each 1-morphism defined by its underlying globular structure.

We now have two different topoi, with the later one, $Sets^{U_n}$, providing a better presheaf topos theoretic model for n-categories, and yet our discussion still cannot end here. There is one more detail, which leads to the formation of $(n,r)$-categories. As we shall see each of these different $(n,r)$-categories actually has its own special type of underlying globular structure.

We can start with groupoids which are $(1,0)$-categories. In the most basic case we might treat a groupoid as simply a special case of a 1-category. But in actually, a groupoid is a structured dependency quiver, which is to say a unital quiver with an extra inverse function $inv: Arrows(Q) \to Arrows(Q)$ that takes any edge and maps it to its inverse. These dependency quivers are actually used in the topos theory of undirected graphs, whilst ordinary quivers are used in the topos theory of directed graphs.

We now actually have a better terminology for dependency quivers. They can now be considered to simply be the unital (1,0)-globular sets. So the $(n,r)$ category theory terminology matches the underlying globular set terminology, and this same approach in fact generalizes onwards to infinity.

The next case is that of 2-categories. Here we distinguish between three cases: (2,0) categories which are simply the 2-groupoids, (2,1) categories which have all 2-morphisms invertible, and ordinary 2-categories. Each of these different types of (n,r) categories has their own corresponding class of globular set, in the same way that groupoids are distinguished by unital (1,0)-globular sets.

A (2,1)-globular set has an inverse for 2-morphisms, and a (2,0)-globular set has an inverse for both 2-morphisms and 1-morphisms. A (2,2)-globular set is just an ordinary unital 2-globular set. Each of these different types of globular sets correspond to special classes of presheaves, in the same way as we constructed presheaves for dependency quivers. This generalises to the theory of (n,r) globular sets.

• a (0,0)-globular set is just a set
• a (1,0) globular set is a dependency quiver
• a (1,1) globular set is a unital quiver
• a (2,0) globular set is a unital 2-globular set with an inverse function for 1-morphisms and 2-morphisms
• a (2,1) globular set is a unital 2-globular set with an inverse function for 2-morphisms
• a (2,2) globular set is a unital 2-globular set

So these different types of (n,r)-globular set determine the different types of (n,r)-category that can be formed over them. The type of an (n,r) category is determined by the underlying presheaf that it enriches.

Definition. the category $G_{(n,m)}$ is the unital globe category $U_n$ with an inverse adjoined for all morphisms with index greater then $m$.

Definition. an (n,r) globular set is a presheaf in the topos $Sets^{G_{(n,m)}}$.

Every $(n,r)$ type encodes its own type of globular set and it has its own topos. At the same time, the type of for semicategories, and n-semicategories is determined by having an n-globular set without identities, so much like how $(n,r)$ categories are distinguished from one another by their underlying globular set, the same is true for how semicategories are distinguished from their corresponding categories.

In fact, rather or not an object is a category, semicategory, groupoid, 2-semicategory, 2-category, 2-groupoid, (2,1)-category, etc can always be determined by the topos of its underlying globular set. So the highest level classification of categories comes from their globular topos. Categories and their generalisations can always be identified by two different aspects:

• Combinatorial structure: the underlying globular set of the category, rather or not it is an (n,r)-globular set, has identities, etc.
• Algebraic structure: the compositional aspect of the category, which allows you to extend a quiver or other globular set with the composition of morphisms.

The combinatorial structure of a category can always be understood with topos theory and selected topoi like $Sets^{G_n}$ and $Sets^{G_{(n,m)}}$. One of the things that I have strongly emphasized is the topos theoretic foundations of algebra, and that presheaves are the best models we have for algebraic stuctures, but the full realisation of this programme is a subject for further development.

We have noticed by this formalisation that the different types of $(n,r)$ categories are distinguished presheaf theoretically by the type of their underlying globular sets. A slightly different situation occurs when considering $\infty$-categories. $\infty$-categories are defined by other base topoi like $\infty$-globular sets and simplicial sets. An $\infty$-category is then just a different type of presheaf. Higher categories then fit nicely into our foundations in presheaf topos theory.

The development of higher category theory does not challenge our foundation in presheaf topos theory. If anything, it actually reinforces it because all the different types of higher category construction are determined by the different types of presheaves. We will model higher categories using presheaf topos theory.

References:
(n,r)-Categories
Globular sets
Geometric shapes for higher structures

The subobject classifier in the topos Sets^(->)

In order to demonstrate operations in on objects of the elementary copresheaf topos $Sets^{\to}$ we should first create a function object. This can be done as of Locus 1.2 using the mapfn function, which converts a clojure.lang.IPersistentMap into a SetFunction. You can also perform the same conversion using the standard to-function method.

(def f
  (mapfn 
    {:a :x, 
     :b :x, 
     :d :y, 
     :e :y, 
     :f :z}))

Once you have defined a function, you can display it using the visualize routine which will give you a diagram like this, demonstrating a surjective function. When we define a subobject classifier in a topos, we also need an object of truth values. The object of truth values in the topos of functions $Sets^{\to}$ is a function that looks like this. The subobject classifier in the topos $Sets^{\to}$ is then a morphism in $Sets^{\to}$, but that means it is also an object in the topos $Sets^{T_2 \times T_2}$ and a presheaf object of a topos in its own right. We get a subfunction from the pair (#{:a :d}, #{:x :y}). The resulting subobject classifier in the topos $Sets^{T_2 \times T_2}$ looks like this: I recently mentioned that $Sets^{\to}$ is a concrete category. This is a new development that I only implemented in Locus 1.2, when I decided that everything should be made into a concrete category in order to implement structure copresheaves and to expose as many morphisms as possible to reasoning in the topos $Sets^{\to}$. This means that the subobject classifier in $Sets^{\to}$ itself has an underlying function that looks like this: This demonstrates that the subobject classifier in $Sets^{\to}$ is like a function on the elements of functions. The elements of functions are inputs labeled by zero and outputs labeled by one, and the maps between them map inputs to inputs and outputs to outputs. We map inputs to $0$, $\frac{1}{2}$ and $1$ depending upon rather they are in the set, their image is in the set, or if their image isn't even in the set at all. So this gives a different notion of truth then we are used to in $Sets$.

When we think of a function $f: A \to B$ we don't typically think of it as a structured set, in fact I am not familiar with any text that describes them as such nor anything that describes $Sets^{\to}$ as a concrete category. This requires a fundamental rethinking of one of the most basic objects of mathematics: functions. We must now consider functions to be like structured sets again.

The beauty of this construction is that when can then take morphisms in $Sets^{\to}$ and consider them to be objects in $Sets^{\to}$ again so we can use the categorical logic of $Sets^{\to}$ on them. In particular, we see that the underlying function of the diamond copresheaf demonstrated above has a function congruence which maps the first part of the input to the first part of the output, demonstrating that morphisms of functions preserve input/output types.

The justification of representing everything as a structured set and every category as a concrete category, is actually primarily so that every morphism can be structured function. This way we can always reason about any morphism in a concrete category using the fundamental topos $Sets^{\to}$ which is our most deepest goal. This requires that we rethink our understanding of presheaves, so that we can consider the different layers of presheaf representations that mathematical objects can be exposed to.

References:
Topoi: The Categorial Analysis of Logic by Robert Goldblatt

Locus 1.2.0

A new release of Locus has been pushed to github. This version is the most different from any of its predecessors.

• Everything is a set again: the new concrete categories support in this system makes everything as much as possible into structured sets. This allows us to reason about more functions using topos theory and the fundamental topos $Sets^{\to}$.
  • $Sets^{\to}$ itself is a concrete category. Functions $f: A \to B$ have elements which are either input elements of $A$ or output elements of $B$ which can be represented as ordered pairs $(0,a)$ and $(1,b)$ to distinguish rather or not an element is in the input set or the output set. A morphism of functions in $Sets^{\to}$ is then a function on these input and output elements.
  • $Quiv$ is a concrete category whose elements are objects and morphisms. In particular, as categories are enriched quivers, they are again structured sets whose elements are objects and morphisms. Functors are functions of categorical elements.
  • Let $F$ be an arbitrary copresheaf in $Sets^P$. Then its elements are simply section elements $(o,x)$ with $o \in Ob(P)$ and $x \in F(o)$. It follows that structured presheaves are simply structured sets of sections. Section elements are now supported by special classes.
• The new concrete category framework also supports the theory of structure presheaves. Any functor to a concrete category has an udnerlying copresheaf. So it follows for example that a quiver valued functor $F: C \to Quiv$ has an underlying presheaf defined by the mechanism that turns $Quiv$ into a concrete category.
• By the same token we have mechanisms for converting $Rel$ and the category of partial functions into concrete categories, so that functors $f : C \to Rel$ are represented as structure presheaves.
• In order to better support the topos theoretic foundations, our emphasis on $Sets^{\to}$ and set valued functors, the fundamental parts of the system related to $Sets^{\to}$ and the foundational logic of functions are moved into the base folder instead of the elementary folder.
• A whole new and fundamental mechanism for displaying copresheaves is now supported in this version of Locus. It focuses on copresheaves over partial orders, and it displays them in Graphviz like a clustered Hasse diagram. Corresponding to this, a wide variety of new types of copresheaves over partial orders is supported in this version. New mechanisms for handling functional dependencies are provided, and a new class for handling copresheaves over preorders is defined.
• New mechanisms are provided to make morphisms of dependency functors back into dependency functors, and morphisms of copresheaves back into copresheaves. With these new mechanisms we can get a handle on the sufficiency of presheaf topos theory.
• Subobject classifiers are finally provided for all the different topoi in the system, including subobject classifiers of chains which generalize subobject classifiers of functions.
• We have new support for two quivers: which are simply ordered pairs of quivers sharing a common set of edges and objects. In other words, they are quivers which have 2-morphisms between morphisms without any conditions that the morphisms they are between need to be parallel.
• By the same token, we provide a 2-globular set class that provides us with quivers with 2-morphisms that are only between parallel pairs of morphisms. These 2-globular sets can then be used to provide a model of 2-categories.
• We now have support for n-globular sets, n quivers, etc. These are the first in the series of presheaf topos theoretic structures for higher categories. Globular and simplicial sets can be used as models of higher categories, thereby giving them a basis in presheaves.
• The readme was drastically changed and whole sections were removed, dealing with topos theoretic knowledge representation as I have rethought the entire issue. Instead, I leave a new section on geometric philosophy. In this section, I describe how computer science is like geometry and topos theory is the key to understanding computation. I leave the details of that open to further examination, rather then going in to too many specifics as the theory is constantly changing.

Subobject lattices of presheaves

Functions standout as among the most ubiquitous of mathematical structures. Ever since I first encountered functions, I have sought to reason about them logically. At first I met with failure. There was no overall framework available to me to fit everything together. The solution then occurred to me in topos theory.

We start by reasoning logically about presheaves, and then we can consider functions to be presheaves using $Sets^{\to}$. Within presheaf theory itself, we tend to focus first on subobject lattices of presheaves, but equally fundamental is to consider their dual categorical logic of quotients. The later is responsible for some of the most exciting developments in topos theory. Today we focus on the former.

Every step that we make in topos theory brings us closer to understanding the big picture view provided by topoi. With topos theory, we can build an overall unified theory of mathematical structures. This should be a topic of further research, so without further ado lets get started.

Sections
A copresheaf (set-valued functor) $F : C \to Sets$ is a special type of structured set whose members are sections. Sections are defined as certain ordered pairs.

Definition. Let $F : C \to Sets$ be a presheaf. Then a section $(o,m)$ is an ordered pair with $o \in Ob(C)$ and $m \in F(o)$.

A morphism of copresheaves is then a structured function on sections. Let $F : C \to Sets$ and $G : C \to Sets$ be copresheaves and let $\tau : F \to G$ be a natural transformation between them. Then $\tau(o,m) = (o, \tau_o(m))$ where $\tau_o$ is the component function of the natural transformation associated with the object $o \in Ob(C)$.

The action preorder of a copresheaf:
We associated to the set of sections of a presheaf a preorder on sections, that generalises the familiar action preorder of an MSet used to define Green's relations.

Definition. let $F : C \to Sets$ then we can define a binary relation $\subseteq$ on sections. \[ (o_1, m_1) \subseteq (o_2, m_2) \] \[ \exists g : o_1 \to o_2 \in Arrows(C) \text{ and } F(g)(m_1) = m_2 \] Proposition 1. The binary relation $\subseteq$ is a preorder.

Proof. let $(o,m) \in F$ then $\exists 1_o : o \to o \in Arrows(C)$ with $1_o(m) = m$ so that implies that $(o,m) \subseteq (o,m)$ with means that $\subseteq$ is reflexive. On the other hand, suppose that $(a,l), (b,m), (c,n)$ are sections of $F$ with $(a,l) \subseteq (b,m)$ and $(b,m) \subseteq (c,n)$. Then since $(a,l) \subseteq (b,m)$ there exists a morphism $f : a \to b$ with $f(l) = m$. Then because $(b,m) \subseteq (c,n)$ there exists a morphism $g: b \to c$ with $g(m) = n$.

As $f(l) = m$ and $g(m) = n$ by substitution we have that $g(f(l)) = n$. By the same token $(g \circ f)(l) = n$. So there exists a morphism $g \circ f : a \to c$ with the property that $g(f(l)) = n$ which implies that $(a,l) \subseteq (c,n)$. It follows that $\subseteq$ is transitive. Since it is both transitive and reflexive it is a preorder. $\square$

The process by which the transitivity of $\subseteq$ is ensured is the same process by which the underlying binary relation of a category is ensured to be a preorder. Each category is defined to be an algebraic extension of a preorder. The fact that $\subseteq$ is a preorder saves us from having to do a transitive closure, which aids us in computation of the action preorder.

The relationship to the object preorder:
Categories are deeply intertwined with preorders. This fact starts on the most basic level with the object preorder, which preorders the set $Ob(C)$ of objects of a category.

Definition. let $C$ be a category and $a,b \in Ob(C)$ then $a \subseteq b$ provided that $\exists f :a \to b \in Arrows(C)$.

This suggests a basic relationship between the preorder on sections of a copresheaf and the preorder on objects of its index category.

Definition. let $F: C \to Sets$ be a copresheaf then the mapping $t: Sections(F) \to Ob(C)$ that takes any section $(o,m)$ to its object part is a forgetful functor from the section preorder to the object preorder.

It follows that $t$ is a monotone map. As a consequence, we can always look to the object preorder of the index category as a first step to understanding the section preorder, so when we implement an algorithm for checking for membership in the action preorder relation, the first step will be to check inclusion in the object preorder.

Implementing the action preorder:
The definition of the section preorder of a copresheaf suggests a general mechanism for computing the preorder for a given copresheaf over an index category $C$. In particular, for any pair $(o_1,m_1)$ and $(o_2,m_2)$ we can compute their membership in the section preorder using the following algorithm:

• check that $o_1 \subseteq o_2$ in the object preorder of $C$
• compute the hom class $Hom(o_1, o_2)$ then loop through its members and check if a member $f$ in the hom class if $f(m_1) = m_2$. If such a member does satisfy this condition exit the loop and return true, otherwise return false.

This suggests the main requisite mechanism for computing the section preorder is the prior definition of a computable hom classes function $Hom(a,b)$ for objects of the index category $C$. The object preordering can easily be defined them from the emptyness of the hom class $Hom(a,b)$ or it can be defined separately if a quicker mechanism is available.

In the special case where in the index category $C$ is itself a preorder, then we can cut out the loop entirely as every hom class has a unique element. Then $(o_1,m_1) \subseteq (o_2,m_2)$ provided that $o_1 \subseteq o_2$ and $f(m_1) = m_2$ for the unique $f \in Hom(o_1,o_2)$. It follows naturally that preorders are a special case where in the action preorders on their sections are made amenable to easy computation.

Recovering the action preorder of a monoid:
Let $M$ be a monoid and $F: M \to Sets$ be a copresheaf on $M$ with underlying set $S$. Then we have that $a \subseteq b$ in $S$ provided that $\exists m \in M : ma = b$. Then this action preorder is isomorphic to the action preorder of sections of $F$ as a copresheaf. This demonstrates that this familiar concept is monoid theory is actually just a special case of something from presheaf theory.

The action preorder on $S$ is taken by defining that $a \subseteq b$ provided that $\exists m \in M : ma = b$. It is customary that a monoid has a single object which we call $0$ for the non-negative unsigned integer. So now all sections of the MSet are of the form $(0,x)$ for any $x \in S$. Then we have that $(0,a) \subseteq (0,b)$ provided that there exists $m : 0 \to 0$ in the monoid $M$ such that $m(a) = b$ which recovers the definition of the action preorder of the MSet. From now on we will simply refer to the action preorder of a copresheaf.

Partially ordered endotrivial categories:
A category $C$ is called endotrivial provided that $\forall x \in Ob(C)$ we have that $|End(C)| = 1$, so that the only morphism in any endomorphism monoid is the identity.

Theorem 1. let $C$ be an endotrivial category with an antisymmetric object preorder. Then the section preorder on a copresheaf $F : C \to Sets$ over $C$ is antisymmetric, and therefore it is a partial order as well.

Proof. suppose that $(o_1,m_1) \subseteq (o_2,m_2)$ and $(o_2,m_2) \subseteq (o_1,m_1)$. Then by the relationship to the object preorder, we have $o_1 \subseteq o_2$ and $o_2 \subseteq o_1$ but since this is an endotrivial preorder we have $o_1 = o_2$. So this means the sections are of the form $(o,m_1)$ and $(o,m_2)$ now in order for $(o,m_1) \subseteq (o,m_2)$ we must have that there exists $f \in Hom(o,o)$ such that $f(m_1) = m_2$.

However, $C$ is endotrivial so the hom class $Hom(o,o)$ contains only the identity $1_o$. Therefore $f = 1_o$ which implies that $f(m_1) = m_1$ and since $f(m_1) = m_2$ as well this implies that $m_1 = m_2$. Then substituting this back into our definition of the sections we get $(o_1,m_1)$ equals $(o_2,m_2)$. By the fact that the only symmetrically related pairs in $F$ are equal ones, we see that the section preorder $\subseteq$ is antisymmetric. $\subseteq$

Corollary 1. let $F: C \to Sets$ be a copresheaf over a partial order $C$. Then the section preorder of $F$ forms a partial order.

Example 1. let $Quiv$ be the topos of quivers. Then $Quiv$ is isomorphic to $Sets^{T_2^*}$ which is the copresheaf topos over the partially ordered endotrivial index category $T_2^*$. It follows that given any quiver $Q$ we have that its sections are partially ordered, with the condition that any morphism is dependent upon its source and target objects.

Example 2. let $(\mathbb{N},+)$ be the commutative monoid of addition over the non-negative integers. Then consider the self induced action $\mathbb{N}$-set of $\mathbb{N}$ acting on itself. Then since $(\mathbb{N},+)$ is a commutative J-trivial monoid, its self induced action preorder is also a partial order. However, $(\mathbb{N},+)$ is clearly not endotrivial. This demonstrates that the converse condition isn't true, as there are other types of copresheaves with antisymmetric section preorders.

The subobject lattice of a copresheaf
The nice thing about the section preorder of a copresheaf, a concept which introduced here, is that it completely determines the distributive subobject lattice of a copresheaf.

Proposition 2. Let $F : C \to Sets$ be a copresheaf. Then the subobject lattice of $F$ is isomorphic to the lattice of upper sets of its section preorder.

Proof. suppose that $F: C \to Sets$ is a presheaf with each $x \in Ob(C)$ associated to a set $F(x)$. Define another mapping, $\tau$ that takes each $x$ to some set $\tau(x) \subseteq F(x)$. Then in order for the subsets represented by $\tau$ to be a subobject of $F$ it must be the case that for each $a \in \tau(x)$ then for each morphism $m: x \to y$ starting at $x$ we have that $m(x) \in \tau_y$ so that $\tau$ is an upper set of the section preorder. In other direction, we can take each $\tau$ to form an inclusion function $\tau(x) \hookrightarrow F(x)$ and these components of a natural transformation determine a subobject of $F$. $\square$

Theorem 2. Let $F : C \to Sets$ be a copresheaf. Then the subobject lattice $Sub(F)$ is distributive.

Proof. By order theory we know that the upper sets of a preorder always form a distributive lattice. By proposition 2, we know that $Sub(F)$ is the lattice of upper sets of the section preorder. Therefore, $Sub(F)$ is distributive. $\square$

Distributive lattices tend to emerge from the lattice of upper sets of a preorder, for example recall that the lattice $Con(L)$ of congruences of a finite lattice is simply the upper sets of the induced preorder on atomic intervals. This new theorem defines the distributive lattice on subobjects of copresheaf in terms of the preorder on its section elements.

Copresheaves over groupoids
Lemma 1. Let $G$ be a groupoid and let $F: G \to Sets$ be a copresheaf. Then the section preorder on $F$ is symmetric.

Proof. suppose that $(o_1,m_1) \subseteq (o_2,m_2)$ then we have that there exists $f : o_1 \to o_2$ such that $f(m_1) = m_2$. By the fact that $G$ is a groupoid there also exists $f^{-1} : o_2 \to o_1$ and that $f^{-1}(f(m_1)) = f^{-1}(m_2) = m_1$. It follows that $f^{-1}(m_2) = m_1$. This implies that $(o_2,m_2) \subseteq (o_1,m_1)$. It follows that $\subseteq$ is symmetric. $\square$

Theorem 3. Let $G$ be a groupoid. Then the topos $Sets^G$ is boolean.

Proof. let $F \in Sets^G$ be a coresheaf $F : G \to Sets$ then by lemma 1 the section preorder on $F$ is symmetric. The upper sets of a symmetric preorder always form a boolean algebra, and so now by proposition 2 it follows that $Sub(F)$ is a boolean algebra. This means that $Sets^G$ is a boolean topos. $\square$

The restriction partial order on a sheaf:
Let $X$ be a topological space, then a sheaf on $X$ is a special type of presheaf $F : X \to Sets$ on the partially ordered set formed by $X$. By corollary 1, it follows that the section preorder on $F$ is antisymmetric and therefore it forms a partial order. We can simply call this the restriction partial order on the sheaf.

Definition. let $F: X \to Sets$ be a topological sheaf. Then the section preorder on $F$ is a partial order called the restriction order on $F$.

Theorem. let $F: X \to Sets$ be a topological sheaf and suppose that $s_i \in F(U_i)$ is a gluable family of sections (so that the $U_i$ form an open cover and the sections meet on intersections) then the glue $s$ is a least upper bound of the $s_i$ in the restriction partial order.

Proof. the glue $s$ has the property that $s_{U_i} = s_i$ for each $i \in I$ so it follows that $s_i \subseteq s$ for each $i \in I$ with respect to the restriction ordering of the sheaf. The gluing condition requires that the $U_i$ form a covering family, but then $U$ forms a least upper bound of the $U_i$. So by the relationship to the object preorder any other section must have an object at least as big as $U$ so no upper bound can be smaller then $s$. Therefore, $s$ is a least upper bound of the $s_i$ and furthermore by the locality condition it is a unique least upper bound of the $s_i$. $\square$

A sheaf is a partially ordered set of sections with a semilattice-like operation of gluing that produces the join of sections under certain conditions. A sheaf can almost always be considered to be like a set of functions, in which case the restriction ordering is simply the partial ordering on functions, that says that one function is a part of another if it is a restriction of it.

Furthermore, in that case the gluing operation is simply the special case of the union of two functions which can only exist when the two functions meet on their common intersections. As the union operation is a least upper bound, it immediately follows that the gluing is a special case of a least upper bound operation on a poset. As we see here, this follows directly from the abstract definition of a sheaf.

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.