Let
Endo be the
category where:
objects are pairs
(X,f) of a
set X and
function f:X→X
morphisms φ:(X,f)→(Y,g) are maps
φ:X→Y so that the square
commutes.
(We may be interested in studying such
objects to
model, for instance, iterative computation, such as simulation. An
object (X,f) consists of a
set of possible simulation states and a stepping
function f:X→X which updates a simulation by one time
unit. A
morphism φ:(X,f)→(Y,g) gives a way to use
(X,f) to
model (Y,g): you can compute
fk(x0) in
X; then passing through
φ produces
φ(fk(x0)), which, by the commutative square, is guaranteed to be the same as
gk(φ(x0)). This is useful if, for instance, we want to compute
gk(y0) but computation in
Y is expensive: then we find some
X admitting cheaper computation, some
x0 for which
φ(x0)=y0, and we compute
φ(fk(x0)) instead.)
Note that we may stack the commutative square multiple times:
To conclude, for any
k, that
fk ; φ=φ ; gk
Unmotivated, let’s bring attention to the particular
object (N,s), where
s(x)=x+1 is the successor
function. The above tells us that for any
morphism φ:(N,s)→(Y,g) we have
sk ; φ=φ ; gk
that is,
φ(n+k)=gk(φ(n))
Hence knowing
φ(n) decides the values of
φ(n+k); ie, decides the values of
φ(m≥n). For the special case of
n=0, then, we should decide
all values, and indeed we do: specializing the above
formula to
n=0 produces
φ(k)=gk(φ(0))
What we have learned is that a
homomorphism φ:(N,s)→(Y,g) is decided entirely by its value on
0!
Also note that its value on
0 has no restrictions; for any choice
y0∈Y we may construct the mapping
ψy0:(N,s)0(n>0)→(Y,g)↦y0↦gn(y0)
which takes
0 to
y0 and still succeeds in being a
homomorphism.
In other words, a
homomorphism φ:(N,s)→(Y,g) contains exactly as much information as the single mapping
φ(0)=y0. Thus we may reasonably correspond
homomorphisms φ with their values
φ(0); one could say we are, ahem, representing
φ with
φ(0).
We reify this thought process with the following collection of
bijections, which implement this correspondence:
β(Y,g):((N,s)→(Y,g))φ(n↦gn(y0))→Y↦φ(0)←∣y0
(Note that the construction
β−1(y0) is the same as the construction
ψy0 from before)
It is left to the reader to verify that this definition does indeed produce
bijections.
Note that—hey!—this looks a lot like a
natural isomorphism. Define a “
forgetful functor” out of our
category
U:Endo(X,f)(φ:(X,f)→(Y,g))→Set↦X↦(φ:X→Y)
and then our
bijections β(Y,g) form
components that seem to compose a
natural isomorphism
β:Mor((N,s),−)≅U
In fact, this
is a
natural isomorphism; we can see that its naturality square
commutes since for any
φ:(N,s)→(Y,g) we get
((f∘−) ; α(Z,h))(φ)=(f∘φ)(0)=f(φ(0))=(α(Y,g) ; f)(φ)
Hence, the
forgetful functor U is represented by
(Z,s).
To conclude, for any , that
Unmotivated, let’s bring attention to the particular object , where is the successor function. The above tells us that for any morphism we have
that is,
Hence knowing decides the values of ; ie, decides the values of . For the special case of , then, we should decide all values, and indeed we do: specializing the above formula to produces
What we have learned is that a homomorphism is decided entirely by its value on !
Also note that its value on has no restrictions; for any choice we may construct the mapping
which takes to and still succeeds in being a homomorphism.
In other words, a homomorphism contains exactly as much information as the single mapping . Thus we may reasonably correspond homomorphisms with their values ; one could say we are, ahem, representing with .
We reify this thought process with the following collection of bijections, which implement this correspondence:
(Note that the construction is the same as the construction from before)
It is left to the reader to verify that this definition does indeed produce bijections.
Note that—hey!—this looks a lot like a natural isomorphism. Define a “forgetful functor” out of our category
and then our bijections form components that seem to compose a natural isomorphism
In fact, this is a natural isomorphism; we can see that its naturality square
commutes since for any we get
Hence, the forgetful functor is represented by .
commutes. Because is initial, then each mor-set has size one, so each component
has only one possible value. (There is only one way to biject singleton sets!)
So let be composed of such bijections. This choice of bijection commutes, because
Hence is a natural isomorphism; done.