The identity functor

The most basic and fundamental topoi are $Sets$ and $Sets^{\to}$. These describe the fundamentals of sets and functions respectively. As these are the most important objects of topos theoretic mathematics, it would be nice if the two could be related to one another in a way.

Definition. let $Sets$ be the topos of sets and $Sets^{\to}$ the topos of functions. Then let $id : Sets \to Sets^{\to}$ be the function of categories that maps each set $X$ to its identity function $id_X: X \to X$ with $f(x) = x$ and that maps each morphism of sets $f : A \to B$ to the morphism of functions $id_f : id_A \to id_B$ defined by the ordered pair of functions $(f,f) : A^2 \to B^2$.

Theorem. $id : Sets \to Sets^{\to}$ is a monofunctor, which makes $Sets$ into a full subcategory of $Sets^{\to}$.

Proof. (1) let $f: A \to B$ and $g : B \to C$ be morphisms of $Sets$ then their composition is $f \circ g : A \to C$. The corresponding morphisms of $Sets^{\to}$ are $(id_f,id_f)$ and $(id_g,id_g)$ defined as ordered pairs of functions. Then their composition is defined componentwise to be $(id_f \circ id_g, id_f \circ id_g)$ which can be be refactored as $(id_{f \circ g}, id_{f \circ g})$. So that $id_{f} \circ id_{g} = id_{f \circ g}$ which makes $id$ a functor.

(2) let $id_A : A \to A$ and $id_B : B \to B$ be the identities of $A$ and $B$ respectively. Suppose that $(f,g)$ is a morphism of functions from $id_A$ to $id_B$ then it must satisfy the commutative diagram which says that $id_B \circ f = g \circ id_A$ which is logically equivalent to $f = g$. By the fact that $f=g$, it follows that any morphism of identity functions is of the form $(f,f) : id_A \to id_B$ which can be defined by identity functor $id_f$ which makes $Sets$ a full subcategory of $Sets^{\to}$. $\square$

This embeds the topos $Sets$ into the topos $Sets^{\to}$ as the full subcategory $Id$. It would be interesting, if we could further determine the properties of this embedding and the extent to which it preserves the topos theoretic properties of $Sets$.

Theorem. $Id$ is closed under taking products and coproducts, but not under subobjects and quotients.

Proof. (1) suppose that $id_A: A \to A$ is an identity function, then it has as a subobject all non-surjections that are taken by reducing the domain and not the codomain. Likewise, given $id_A : A \to A$ we can define a congruence of functions by $(=_A, true)$ which has a constant quotient, rather then an identity quotient. So $Id$ is not closed under subobjects or quotients.

(2) on the other hand suppose that $id_A : A \to A$ and $id_B : B \to B$ are two identity functions. Then $id_A \times id_B : A \times B \to A \times B$ takes $f(a,b)$ to $(id_A(a),id_B(b))$ which is equal to $(a,b)$ so it is still an identity function. Similarily, the coproduct $id_A + id_B : A + B \to A + B$ takes any $a \in A$ to $a$ and $b \in B$ to $b$ so that it is still an identity function. $\square$

This completes the process of relating $Sets$ to $Sets^{\to}$. In the other direction, there are a couple of ways to relate $Sets^{\to}$ back to $Sets$. Firstly, given any category $C$ with subcategory $S$ then we can define a morphism of topoi $Sets^{C} \to Sets^{S}$ that reduces each set-valued functor to its $S$ components. Using this, we can define input set and output set functors on $Sets^{\to}$.

A limitation of this approach is that it doesn't make $Sets^{\to}$ into a concrete category, so in order to do that we simply need to use the coproduct construction. This takes any function $f : A \to B$ to its coproduct set $A + B$ constructed from its input and output sets. Together with the input and output set functors, these functors relate $Sets{\to}$ and $Sets$.