I wish I can remember how it ends… until then, it’s yet another glitch in the matrix: is a given adjoint of a functor
discrete: S –> F
left or right adjoint? As if to compound my confusion, left adjoint coincides with right:
pieces = points
in the definition of quality type (see Axiomatic Cohesion), which I’m trying to understand.
Let’s start with the functor
discrete: S –> F
from the category S of sets to the category F of functions (simply because I have a vague feeling that this is how I went about telling left from right). The category S of sets has sets and functions as its objects and morphisms, respectively, while the category F of functions has functions and commutative squares as its objects and morphisms, respectively (Conceptual Mathematics, pp. 144-5). The functor
discrete: S –> F
assigns to each object (set)
A
(in S) its identity function
1A: A –> A
(an object in F) i.e.
discrete (A) = 1A: A –> A
and to each morphism (function)
f: A –> B
(in S) a morphism
discrete (f: A –> B) = discrete (A) –> discrete (B)
= <f, f>: 1A –> 1B
(in F) which is a commutative square
A –– f ––> B
^ ^
| |
1A 1B
| |
A –– f ––> B
(satisfying 1B · f = f · 1A, where ‘·’ denotes composition).
Now, we are told that the functors
points: F –> S
pieces: F –> S
are adjoint functors of the functor
discrete: S –> F
(see [or is it more like do] Exercise 6.14 on page 119 of Sets for Mathematics). And our job is to figure out which one is left adjoint and which one is right adjoint and, of course, why?
Let’s start with the functor
points: F –> S
which assigns to each object (function)
f: A –> B
(in F) its domain set
A
(in S) i.e.
points (f: A –> B) = A
and to each morphism from an object
f: A –> B
to an object
f’: A’ –> B’
i.e. to each commutative square
B –– w ––> B’
^ ^
| |
f f’
| |
A –– v ––> A’
(satisfying f’ · v = w · f) a function
v: A –> A’
(in S) i.e.
points (f’ v = w f) = points (f) –> points (f’)
= v: A –> A’
Looking at the definition of adjoint functor (Conceptual Mathematics, pp. 374-5), we realize that we could call
discrete: S –> F
left adjoint to
points: F –> S
if we can find a natural correspondence
d: discrete (X) –> f
————————————
p: X –> points (f)
for every object X in S and f in F.
In other words, every function
p: X –> points (f)
(in S; whose type is given as a value of the points functor) is determined by the function
nX: X –> points (discrete (X))
and the determination
points (d: discrete (X) –> f)
is unique i.e. for every
p: X –> points (f)
(in S) there is a unique
d: discrete (X) –> f
(in F) such that
p = points (d) · nX
In (yet) other words, there is a natural transformation
n: 1S –> points · discrete
from the identity functor
1S: S –> S
(on S) to the composite functor
points · discrete: S –> S
(an endofunctor on S), whose components are
nX: X –> points (discrete (X))
Summing up, so far, we say
discrete: S –> F
functor is left adjoint to
points: F –> S
functor if there is a natural transformation
n: 1S –> points · discrete
What if, instead, the functor
discrete: S –> F
is right adjoint to
points: F –> S
functor? Well, then we would expect to see a natural correspondence
p’: points (f) –> X
————————————
d’: f –> discrete (X)
for every object X in S and f in F.
In other words, every figure
p’: points (f) –> X
(in S; whose shape is given as a value of the points functor) is included in the figure
n’X: points (discrete (X)) –> X
and the inclusion
points (d’: f –> discrete (X))
is unique i.e. for every
p’: points (f) –> X
(in S) there is a unique
d’: f –> discrete (X)
(in F) such that
p’ = n’X · points (d’)
In (yet) other words, there is a natural transformation
n’: points · discrete –> 1S
from the composite functor
points · discrete: S –> S
(an endofunctor on S) to the identity functor
1S: S –> S
(on S), whose components are
n’X: points (discrete (X)) –> X
Summing up, so far, we say
discrete: S –> F
functor is right adjoint to
points: F –> S
functor if there is a natural transformation
n’: points · discrete –> 1S
Summing it all, if there’s a natural transformation
n: 1S –> points · discrete
we say
discrete is left adjoint to points
and if there is a natural transformation
n’: points · discrete –> 1S
we say
discrete is right adjoint to points
Let’s see: since
points · discrete (X) = X
and, of course,
1S (X) = X
and since we can take the identity function
1X: X –> X
as components of both the natural transformations i.e. with
nX: X –> points (discrete (X)) = 1X: X –> X
n’X: points (discrete (X)) –> X = 1X: X –> X
we have both the natural transformations
n: 1S –> points · discrete
n’: points · discrete –> 1S
which means
discrete is both left and right adjoint of pieces
But it’s clearly not the case:
discrete is left adjoint to pieces
(do Exercise 6.14 on page 119 of Sets for Mathematics). Are we doomed? No, it’s just intermission and everything that could possibly go wrong for the protagonist goes wrong half-way through Tollywood movies…