Definition. let $A$ be a set and $R \subseteq A^n$ an n-ary relation on $A$. Then there exists an inclusion function $i_R : R \hookrightarrow A^n$ associated with $R$. A partial algebra on $R$ is then simply a function $f: R \to A$.
We can freely define any kind of function we want, but in order to get a valid category we also need to define morphisms. The first component to that will be the definition of composition relation homomorphisms.
Definition. let $(A,f: R \to A)$ and $(B,g : S \to B)$ be n-ary partial algebras. Then $m : A \to B$ is a composition relation homomorphism provided that $m : (A,R) \to (B,S)$ is a homomorphism of relations meanining that $(a_1,a_2,...) \in R$ implies that $(f(a_1),f(a_2),...) \in S$.
In the case of total algebras, we don't need a relation homomorphism. On the other hand, since partial algebras are defined over arbitrary n-ary relations we need the composition relation homomorphism to ensure the validity of the partial algebra homomorphism construction.
Definition. let $(A,f: R \to A)$ and $(B,g : S \to B)$ be n-ary partial algebras. Then $m : A \to B$ is a partial algebra homomorphism provided that (1) it is a composition relation homomorphism and (2) $f(a_1,a_2,...) = g(m(a_1),m(a_2),...)$ for any $(a_1,a_2,...) \in R$. The first condition ensures that $(m(a_1),m(a_2),...)$ actually exists and is in the domain of $g$. The second condition ensures that they are also equal.
A category is simply a special combination of objects and morphisms so now that we have the preliminary definitions out of the way we can define the category of partial nary algebras.
Definition. let $n \in \mathbb{N}$ then $PA_n$ is the category of $n-ary$ partial algebras with homomorphisms previously defined. The composition domain is a forgetful functor $D : PA_n \to Rel_n$ from this categroy to the category of nary relations.
In order to continue, we now need to prove a basic lemma about relation homomorphisms. This will allow us to construct the input function component of the morphism of functions in the topos $Sets^{\to}$ that emerges from partial algebra homomorphisms.
Lemma 1. let $f : (A,R) \to (B,S)$ be a homomorphism of n-ary relations then consider the product function $f^n : A^n \to B^n$ of the underlying function $f$. Then $(R,S)$ defines a subfunction of $f^n$ in the topos of functions.
Proof. in order for $(R,S)$ to be a subfunction of $f^n$ then it must be that for all $(a_1,a_2,...) \in R$ we have that $(f(a_1),f(a_2),...)$ but this is precisely the definition of a relation homomorphism. $\square$
Then we can restrict $f^n$ to $f^n_{R,S}$ to a get a monomorphism in the topos of functions as depicted in the commutative diagram below.
The point of this construction is to enable us to prove our main theorem which is that homomorphisms of partial nary functional algebras as we have defined them induce morphisms in the topos of functions $Sets^{\to}$.
Theorem 1. let $m : (A, \circ_A : R \to A) \to (B, \circ_B : S \to B)$ be a homomorphism of partial n-ary functional algebras. Then $(m^n_{(R,s) : R \to S},m: A \to B)$ is a morphism of functions from $\circ_A$ to $\circ_B$.
Proof. by lemma 1 we have that $f^n_{R,S}$ is a well defined function. By the definition of partial algebra homomorphisms we have that for each $(a_1,a_2,...) \in R$ that $f(\circ_A(a_1,a_2,..)) = \circ_B(f(a_1),f(a_2),...)$. It follows that $f \circ \circ_A = \circ_B \circ f^{n_{(R,S)}}$ as depited in the following commutative diagram.
It follows that $(m^n_{(R,s) : R \to S},m: A \to B)$ is a morphism in the topos of functions $Sets^{\to}$. It follows that $F : PA_n \to Sets^{\to}$ is a monomorphism from the category of partial algebras to the topos of functions. $\square$
This allows us to create a topos theoretic model for theory of partial algebras. We can now apply this to categories by definining the composition function of a category as a partial algebra.
Definition. let $(Ob(C),Arrows(C),source,target,id,\circ)$ be a category then $(Arrows(C), \circ : Arrows(C)^2_* \to Arrows(C))$ is a partial binary algebra defined over the morphism set of $C$.
Firstly, we can naturally relate functors to homomorphisms of composition relations. This produces a natural forgetful functor from the category of categories $Cat$ to the category of binary relations $Rel$ and relation homomorphisms.
Lemma 2. let $F: C \to D$ then $F$ induces a homomorphism of binary relations from $Arrows(C)^2_*$ to $Arrows(D)^2_*$.
Proof. let $m_1 : A \to B$ and $m_2 : C \to D$ be morphisms of $C$ then in order for them to be composable we humst have $B=C$. Then by the definition of functors, we have that $f(m_1) : f(A) \to f(B)$ and $f(m_2) : f(C) \to f(D)$ are the object signatures of $f(m_1)$ and $f(m_2)$. The fact that $B=C$ implies that $f(B) = f(C)$. It follows that $f(m_1)$ and $f(m_2)$ are composable, so that if $m_1$ and $m_2$ are composable then their outputs by $f$ are. It follows that the morphic component of $F$ is a homomorphism of composition relations. $\square$.
Lemma 3. let $F : C \to D$ be a functor then $F$ induces a homomorphism of partial algebras $PA_F : (Arrows(C)^2_*, \circ) \to (Arrows(D)^2_*, \circ)$.
Proof. in order for a function to be a partial algebra homomorphism it must satisfy two conditions. Condition (1) is satisfied by lemma 2. Condition (2) follows immediately from the definition of functors which ensures that $f(m_1 \circ m_2) = f(m_1) \circ f(m_2)$ whenever the two exist.
We started this discussion by relating the category $PA_n$ to the topos of functions $Sets^{\to}$. With this preliminary out of the way, we can now relate the category of categories $Cat$ itself to the topos of functions $Sets^{\to}$ by defining a forgetful functor from any category to its composition function.
Theorem 2. let $\circ : Cat \to Sets^{\to}$ be the function that maps any category to its underlying composition function, and any functor to its morphism of composition functions. Then $\circ$ is a forgetful functor from the category of categories to the topos of functions.
Proof. by lemma 3 we have a functor $Cat \to PA_2$ from $Cat$ to partial binary algebras. By theorem 1, we can then compose this with the functor from $PA_2$ to $Sets^{\to}$ to get a functor from $Cat$ to $Sets^{\to}$. $\square$
There are two main functors from $Cat$ to topoi the underlying quiver $q : Cat \to Quiv$ and the underlying composition functor $\circ : Cat \to Sets^{\to}$. The other topos valued functors from $Cat$ can be defined by composition with these functors, like the functor to $Sets^2$ or the different functors to $Sets$ defined by taking the object set or the morphism set of the category.
No comments:
Post a Comment