- 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.
Friday, September 30, 2022
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.
Wednesday, September 21, 2022
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:
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.
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.
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.
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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
Subscribe to:
Posts (Atom)