ONT Re: Higher Order Categorical Logic
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
Note 27
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
I return to Part 0 to pick up one or two bits
of indispensable material that I skipped over.
| 3. Adjoint Functors
|
| Perhaps the most important concept which category theory has helped
| to formulate is that of adjoint functors. Aspects of this idea were
| known even before the advent of category theory and we shall begin by
| looking at one such.
|
| We recall from Proposition 1.4 that a functor $A$ -> $B$ between two
| preordered sets $A$ = (A, =<) and $B$ = (B, =<) regarded as categories is
| an order preserving mapping F : A -> B, that is, such that, for all elements
| a, a' of A, if a =< a' then F(a) =< F(a'). A functor G : $B$ -> $A$ in the
| opposite direction is said to be 'right adjoint' to F provided, for all
| a in A and b in B,
|
| F(a) =< b if and only if a =< G(b).
|
| Classically, a pair of order preserving mappings (F, G) is called
| a covariant 'Galois correspondence' if it satisfies this condition.
|
| Once we have such a Galois correspondence, we see immediately that
| GF : $A$ -> $A$ is a 'closure operation', that is, for all a, a' in A,
|
| a =< GF(a),
|
| GFGF(a) =< GF(a),
|
| if a =< a' then GF(a) =< GF(a').
|
| Similarly, FG : $B$ -> $B$ may be called an 'interior operation':
| it satisfies the conditions dual to the above.
|
| In a preordered set an isomorphism a ~=~ a' just means that
| a =< a' and a' =< a. (In a 'poset', or 'partially ordered set',
| one has the antisymmetry law: if a ~=~ a' then a = a'.) We note
| that it follows from the above that GFGF(a) ~=~ GF(a) and, dually,
| FGFG(b) ~=~ FG(b), for all a in A and b in B.
|
| The most interesting consequence of a Galois correspondence is
| this: the functors F and G set up a one-to-one correspondence between
| isomorphism classes of "closed" elements a of A such that GF(a) ~=~ a
| and isomorphism classes of "open" elements b of B such that FG(b) ~=~ b.
| We also say that F and G determine an 'equivalence' between the preordered
| set $A$_0 of closed elements of $A$ and the preordered set $B$_0 of open
| elements of $B$. The following picture illustrates this principle of
| "unity of opposites", which will be generalized later in this section.
|
| F
| ------------------------>
| $A$ <------------------------ $B$
| ^ G ^
| | |
| | |
| | |
| inclusion | | inclusion
| | |
| | |
| | |
| | |
| $A$_0 <---------------------> $B$_0
| equivalence
|
| L&S, page 12.
|
| Lambek, J. & Scott, P.J.,
|'Introduction To Higher Order Categorical Logic',
| Cambridge University Press, Cambridge, UK, 1986.
|
| http://uk.cambridge.org/mathematics/catalogue/0521356539/
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤