ONT Re: Higher Order Categorical Logic
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 30
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| Proposition 3.3. Given two categories $A$ and $B$, there is a
| one-to-one correspondence between adjointnesses (F, U, !h!, !e!)
| and solutions (F, !h!, *) of the universal mapping problem for
| U : $B$ -> $A$.
|
| Proof. If (F, U, !h!, !e!) is given, put f* = !e!(B)F(f).
| Conversely, if U and (F, !h!, *) are given, for each f : A -> A',
| put F(f) = (!h!(A')f)* and check that this makes F a functor and
| !h! a natural transformation; moreover, define !e!(B) = (1_U(B))*.
|
| It follows from symmetry considerations that an adjointness is also
| equivalent to a "co-universal mapping problem", obtained by dualizing
| Definition 3.2. (A left adjoint to $B$ -> $A$ is a right adjoint to
| $B$^op -> $A$^op.)
|
| There is yet another way of looking at adjoint functors,
| at least when $A$ and $B$ are locally small.
|
| Proposition 3.4. An adjointness (F, U, !h!, !e!)
| between locally small categories $A$ and $B$ gives
| rise to and is determined by a natural isomorphism:
|
| Hom_$B$ (F(-), -) ~=~ Hom_$A$ (-, U(-))
|
| between functors $A$^op x $B$ -> Sets.
|
| We leave the proof of this to the reader.
|
| Even if $A$ is not locally small, there is a natural bijection between
| arrows FA -> B in $B$ and arrows A -> UB in $A$. Logicians may think
| of such a bijection as comprising two rules of inference; and this
| point of view has been quite influential in the development of
| categorical logic. An analogous situation in the propositional
| calculus would be the bijection between proofs of the entailments
| C & A |- B and A |- C => B (see Exercise 4 below). Inasmuch as
| implication is a more sophisticated notion than conjunction,
| the adjointness here explains the emergence of one concept
| from another. This point of view, due to Lawvere, may be
| summarized by yet another slogan, illustrations of which
| will be found throughout this book (see, for instance,
| Exercise 6 below).
|
| Slogan 4. Many important concepts in mathematics arise
| as adjoints, right or left, to previously known functors.
|
| We summarize two important properties of adjoint functors,
| which will be useful later.
|
| Proposition 3.5.
|
| 1. Adjoint functors determine each other uniquely
| up to natural isomorphisms.
|
| 2. If (U, F) and (U', F') are pairs of adjoint functors,
| as in the diagram:
|
| U' U
| --------> -------->
| $C$ $B$ $A$,
| <-------- <--------
| F' F
|
| then (UU', F'F) is also an adjoint pair.
|
| L&S, pages 14-15.
|
| Lambek, J. & Scott, P.J.,
|'Introduction To Higher Order Categorical Logic',
| Cambridge University Press, Cambridge, UK, 1986.
|
| http://uk.cambridge.org/mathematics/catalogue/0521356539/
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤