Reprints in Theory and Applications of Categories, No. 16, 2006, pp. 1–16.

ADJOINTNESS IN FOUNDATIONS

F. WILLIAM LAWVERE

Author’s commentary

In this article we see how already in 1967 category theory had made explicit a number of conceptual advances that were entering into the everyday practice of mathematics. For example, local Galois connections (in algebraic geometry, model theory, linear algebra, etc.) are globalized into functors, such as Spec, carrying much more information. Also, “theories” (even when presented symbolically) are viewed explicitly as categories; so are the background universes of sets that serve as the recipients for models. (Models themselves are functors, hence preserve the fundamental operation of substitution/composition in terms of which the other logical operations can be characterized as local adjoints.)

My 1963 observation (referred to by Eilenberg and Kelly in La Jolla, 1965), that cartesian closed categories serve as a common abstraction of type theory and propositional logic, permits an invariant algebraic treatment of the essential problem of proof theory, though most of the later work by proof theorists still relies on presentation-dependent formulations. This article sums up a stage of the development of the relationship between category theory and proof theory. (For more details see Proceedings of the AMS Symposium on Pure Mathematics XVII (1970), pp. 1–14, and Marcel Dekker, Lecture Notes in Pure and Applied Mathematics, no. 180 (1996), pp. 181–189.)

The main problem addressed by proof theory arises from the existential quantifier in “there exists a proof… ”. The strategy to interpret proofs themselves as structures had been discussed by Kreisel; however, the influential “realizers” of Kleene are not yet the usual mathematical sort of structures. Inspired by Läuchli’s 1967 success in finding a completeness theorem for Heyting predicate calculus lurking in the category of ordinary permutations, I presented, at the 1967 AMS Los Angeles Symposium on Set Theory, a common functorization of several geometrical structures, including such proof-theoretic structures. As Hyperdoctrines, those structures are described in the Proceedings of the AMS New York Symposium XVII, cited above.

Author’s commentary copyright F. William Lawvere

Originally published: Dialectica, 23 (1969), used by permission.

My heartfelt thanks go to Christoph Schubert who expertly rendered the original article into TEX

and to the editors of TAC for their work and dedication.

Received by the editors of TAC February 22, 2006 and by Dialectica December 15, 1967.

Transmitted by R. Paré, R. Rosebrugh and R.J. Wood. Republished on 2006-05-21.

2000 Mathematics Subject Classification: 00A30, 14F20, 18B25, 18B30, 18B40, 55U40, 81P05.

Key words and phrases: Formal-conceptual duality, cartesian-closed categories, algebraic logic,

globalized Galois connections.

Proof theory may be regarded as the study of the presentations of certain algebraic structures, for example, locally cartesian closed categories C with finite coproducts. The map category C/X models “proof bundles” with its morphisms playing the role of deductions. Then PX, defined as the poset reflection of C/X, is a Heyting algebra; any map X → Y in C contravariantly induces a Heyting homomorphism of substitution and covariantly induces existential and universal quantifier operations that not only satisfy the correct rules of inference but, moreover, satisfy the usual proof-theoretic slogans that

(a) a proof of an existential statement includes the specification of an element of the kind required by the statement;

(b) a proof of a universal statement is a functional giving a uniform proof of all the instances.

The poset reflection expresses the idea of “there exists a deduction A → B” in C/X, and PX serves as a system of “proof-theoretic propositions” about elements of X. In case C is actually a topos, there is a natural map

PX → P_{C}(X)

to the usual subobject lattice, defined by taking the image of any A → X. This map will be an isomorphism for all X only if C satisfies the axiom of choice, but we might hope that at least P is “small” like P_{C} and that the idempotent of P whose splitting is P_{C} could be described in a useful way. There are two results about that.

(1) The Heyting algebras PX are small iff C itself is Boolean, as in Läuchli’s original construction.

(2) If we localize the definition of P in the sense that we do not ask for the existence of maps A → B in C/X, but only for maps A′ → B where A′ has an epimorphism to A, then this coarsened version of P is actually isomorphic to P_{C} for all toposes C.

The second result divides the existential quantifier in the proof problem into two steps; the preliminary search for an appropriate A′ which covers A illustrates that a hypothesis must sometimes be analyzed before it can be used to launch a deduction. The collapse from a type system to the corresponding system of proof-theoretic propositions is of course not an “isomorphism” (contrary to a fashionable colloquialism), even though both involve cartesian closed categories. To arrive at mathematical truth, we require the further collapse resulting from the unbounded preliminary step.

Buffalo, 22 February 2006

1. The Formal–Conceptual Duality in Mathematics and in its Foundations^{1}

That pursuit of exact knowledge which we call mathematics seems to involve in an essential way two dual aspects, which we may call the Formal and the Conceptual. For example, we manipulate algebraically a polynomial equation and visualize geometrically the corresponding curve. Or we concentrate in one moment on the deduction of theorems from the axioms of group theory, and in the next consider the classes of actual groups to which the theorems refer. Thus the Conceptual is in a certain sense the subject matter of the Formal.

Foundations will mean here the study of what is universal in mathematics. Thus Foundations in this sense cannot be identified with any “starting-point” or “justification” for mathematics, though partial results in these directions may be among its fruits. But among the other fruits of Foundations so defined would presumably be guide-lines for passing from one branch of mathematics to another and for gauging to some extent which directions of research are likely to be relevant.

Being itself part of Mathematics, Foundations also partakes of the Formal-Conceptual duality. In its formal aspect, Foundations has often concentrated on the formal side of mathematics, giving rise to Logic. More recently, the search for universals has also taken a conceptual turn in the form of Category Theory, which began by viewing as a new mathematical object the totality of all morphisms of the mathematical objects of a given species A, and then recognizing that these new mathematical objects all belong to a common non-trivial species C which is independent of A. Naturally, the formal tendency in Foundations can also deal with the conceptual aspect of mathematics, as when the semantics of a formalized theory T is viewed itself as another formalized theory T′, or in a somewhat different way, as in attempts to formalize the study of the category of categories. On the other hand, Foundations may conceptualize the formal aspect of mathematics, leading to Boolean algebras, cylindric and polyadic algebras, and to certain of the structures discussed below.

One of the aims of this paper is to give evidence for the universality of the concept of adjointness, which was first isolated and named in the conceptual sphere of category theory, but which also seems to pervade logic. Specifically, we describe in section III the notion of cartesian closed category, which appears to be the appropriate abstract structure for making explicit the known analogy (sometimes exploited in proof theory) between the theory of functionality and propositional logic. The structure of a cartesian closed category is entirely given by adjointness, as is the structure of a “hyperdoctrine”, which includes quantification as well. Precisely analogous “quantifiers” occur in realms of mathematics normally considered far removed from the province of logic or proof theory.

1I inserted the following subtitles into the text for this reprinting:

1. The formal-conceptual duality in mathematics and in its foundations

2. Adjointness in the meta-category of categories

3. Cartesian-closed categories and hyperdoctrines

4. Globalized Galois connections in algebraic geometry and in foundations

As we point out, recursion (at least on the natural numbers) is also characterized entirely by an appropriate adjoint; thus it is possible to give a theory, roughly proof theory of intuitionistic higher-order number theory, in which all important axioms (logical or mathematical) express instances of the notion of adjointness.

The above-discussed notions of Conceptual, Formal, and Foundations play no mathematical role in this paper; they were included in this introductory section only to provide one possible perspective from which to view the relationship of category theory in general and of this paper in particular to other work of universal tendency. However, if one wished to take these notions seriously, it would seem to follow that an essential feature of any attempt to formalize Foundations would be a description of this claimed “duality” between the Formal and the Conceptual; indeed, both category theory and set theory succeed to some extent in providing such a description in certain cases. Concerning the latter point there is a remark at the end of section IV, which is otherwise devoted to a discussion of a class of adjoint situations differing from those of section III but likewise seeming to be of universal significance — these may be described briefly as a sort of globalized Galois connection.

2. Adjointness in the Meta-Category of Categories

The formalism of category theory is itself often presented in “geometric” terms. In fact, to give a category is to give a meaning to the word morphism and to the commutativity of diagrams like

A ⟶^{f} B  \xymatrix{A \ar[r]^{f} \ar[dr]_{h} & B \ar[d]^{g} \\  & C}  \xymatrix{A \ar[r]^{f} \ar[d]_{a} & B \ar[d]^{b} \\ A′ \ar[r]_{f′} & B′} etc.

which involve morphisms, in such a way that the obvious associativity and identity conditions hold, as well as the condition that whenever

A ⟶^{f} B and B ⟶^{g} C

are commutative then there is just one h such that

\xymatrix{A \ar[r]^{f} \ar[dr]_{h} & B \ar[d]^{g} \\  & C}

is commutative.

To save printing space, one also says that A is the domain, and B the codomain of f when

A ⟶^{f} B

is commutative, and in particular that h is the composition f.g if

\xymatrix{A \ar[r]^{f} \ar[dr]_{h} & B \ar[d]^{g} \\  & C}

is commutative. We regard objects as co-extensive with identity morphisms, or equivalently with those morphisms which appear as domains or codomains. As usual we call a morphism which has a two-sided inverse an isomorphism.

With any category A is associated another A^{op} obtained by maintaining the interpretation of “morphism” but reversing the direction of all arrows when re-interpreting diagrams and their commutativity. Thus A ⟶^{f} B in A^{op} means B ⟶^{f} A in A, and h = f.g in A^{op} means h = g.f in A; clearly the interpretations of “domain”, “codomain” and “composition” determine the interpretation of general “commutativity of diagrams”. The category-theorist owes an apology to the philosophical reader for this unfortunately well-established use of the word “commutativity” in a context more general than any which could reasonably have a description in terms of “interchangeability”.

A functor F involves a domain category A, a codomain category B, and a mapping assigning to every morphism x in A a morphism xF in B in a fashion which preserves the commutativity of diagrams. (Thus in particular a functor preserves objects, domains, codomains, compositions, and isomorphisms.) Utilizing the usual composition of mappings to define commutative diagrams of functors, one sees that functors are the morphisms of a super-category, usually called the (meta-) category of categories.

A category with exactly one morphism will be denoted by 1. It is determined uniquely up to isomorphism by the fact that for any category A, there is exactly one functor A ⟶ 1; the functors 1 ⟶^{A} A correspond bijectively to the objects in A.

A natural transformation φ involves a domain category A, a codomain category B, domain and codomain functors

\xymatrix{A \ar[r]^{F_{0}} \ar[r]_{F_{1}} & B}

and a mapping assigning to each object A of A a morphism

AF_{0} ⟶^{Aφ} AF_{1}

in B, in such a way that for every morphism

A ⟶^{a} A′

in A, the diagram

\xymatrix{AF_{0} \ar[r]^{Aφ} \ar[d]_{aF_{0}} & AF_{1} \ar[d]^{aF_{1}} \\ A′F_{0} \ar[r]_{A′φ} & A′F_{1}}

is commutative in B. For fixed A and B, the natural transformations are the morphisms of a functor category B^{A}, where we write

F_{0} ⟶^{φ} F_{1} in B^{A}

for the above described situation, and define commutativity of triangles

\xymatrix{F_{0} \ar[r]^{φ} \ar[dr]_{φ·\overline{φ}} & F_{1} \ar[d]^{\overline{φ}} \\  & F_{2}}  in B^{A}

by the condition

A(φ.\overline{φ}) = (Aφ).(A\overline{φ})

for all objects A in A.

A second Godement multiplication is also defined for natural transformations, in a way which extends in a sense the composition of functors. Namely, if

F_{0} ⟶^{φ} F_{1} in B^{A} and G_{0} ⟶^{ψ} G_{1} in C^{B}

then F_{0}G_{0} ⟶^{φψ} F_{1}G_{1} in C^{A} is the natural transformation which assigns to each A of A the morphism of C which may be indifferently described as either composition in the commutative square

\xymatrix{AF_{0}G_{0} \ar[r]^{(Aφ)G_{0}} \ar[d]_{(AF_{0})ψ} & AF_{1}G_{0} \ar[d]^{(AF_{1})ψ} \\ AF_{0}G_{1} \ar[r]_{(Aφ)G_{1}} & AF_{1}G_{1}}

The Godement multiplication is functorial

B^{A} × C^{B} ⟶ C^{A}

which means in particular that

(φ.\overline{φ})(ψ.\overline{ψ}) = (φψ).(\overline{φ}\overline{ψ}),

and associative, meaning that if also H_{0} ⟶^{ϑ} H_{1} in D^{C}, then

(φψ)ϑ = φ(ψϑ) in D^{A}.

Other rules follow from the facts that in any product category L × M (obvious definition) a sort a commutativity relation

⟨l, M⟩.⟨L′, m⟩ = ⟨L, m⟩.⟨l, M′⟩

holds for

L ⟶^{l} L′ in L and M ⟶^{m} M′ in M,

and that if Godement multiplication is applied to identity natural transformations, it reduces to composition of the corresponding functors. Two intermediate cases will be important in the sequel: if

F_{0} = φ = F_{1} = F,

then

A(F ψ) = (AF)ψ

while if G_{0} = ψ = G_{1} = G, then A(φG) = (Aφ)G. Thus each functor A ⟶^{F} B induces via Godement multiplication by F a functor C^{B} ⟶^{C^{F}} C^{A} for any category C, and similarly each B ⟶^{G} C induces B^{A} ⟶^{G^{A}} C^{A} for any category A.

Now we come to the central concept, of which we will presently see many examples. An adjoint situation involves two categories A and B, two functors

\xymatrix{A \ar[r]^{F} & B \ar[l]^{U}}

and two natural transformations

A ⟶^{η} F U  in A^{A}
UF ⟶^{ε} B  in B^{B}

satisfying the two equations (commutative triangles)

ηF.F ε = F  in B^{A}
Uη.εU = U  in A^{B}.

We state immediately an equivalent form of the definition. Let (F, B) denote the category whose morphisms are those quadruples of morphisms A ⟶^{a} A′ in A, B ⟶^{b} B′,

AF ⟶^{h} B, A′F ⟶^{h′} B′ in B for which

\xymatrix{AF \ar[r]^{aF} \ar[d]_{h} & A′F \ar[d]^{h′} \\ B \ar[r]_{b} & B′}

is commutative in B; commutative diagrams in (F, B) are defined so that forgetting h, h′ in the above defines a functor

(F, B) ⟶ A × B.

The objects of (F, B) thus correspond to pairs each consisting of a morphism AF ⟶^{h} B in B with a given A in A. Similarly a category (A, U) is defined whose objects correspond to pairs each consisting of a morphism A ⟶^{f} BU in A with a given B in B, and which also has a forgetful functor

(A, U) ⟶ A × B.

Now it can be shown that giving η, ε satisfying the two conditions above in order to complete an adjoint situation is equivalent with giving a functor

(F, B) ⟶^{Q} (A, U)

which commutes with the forgetful functors to A × B and which has a two-sided inverse

(A, U) ⟶^{Q^{−1}} (F, B).

In particular, Q assigns to the object AF ⟶^{h} B of (F, B) the object

A ⟶^{(Aη).(hU)} BU

of (A, U), while Q^{−1} assigns

AF ⟶^{(fF).(Bε)} B

to A ⟶^{f} BU. Sometimes Q is called an adjointness, η an adjunction, and ε a coadjunction for F and U; if such exists, F is said to be left adjoint to U and U is said to be right adjoint to F, and we write F ⊣ U. Briefly, F and U may be placed in an adjoint situation iff bijections

(AF, B) ≅ (A, BU)

can be given in a way which is “natural” or “functorial” when A and B vary; here the left-hand side denotes the set of all AF ⟶^{h} B in B and the right-hand side denotes the set of all A ⟶^{f} BU in A.

Several important properties hold for adjoint situations in general. One is that adjoints are unique (if they exist). That is, any two adjoint situations with a given A ⟶^{F} B are uniquely isomorphic, and similarly for a given B ⟶^{U} A. More generally, given two adjoint situations with fixed A and B (with and without primes), then any natural transformation F′ ⟶ F induces a unique U ⟶ U′, and conversely. If A ⟶^{F} B with F ⊣ U, and B ⟶^{F̃} C, with F̃ ⊣ Ũ, then F F̃ ⊣ ŨU, and also F^{D} ⊣ U^{D} for any category D. Thus a necessary condition for a functor U to have a left adjoint is that U commutes (up to isomorphism of functors) with all generalized limits which exist in B and A, and dually a functor F can have a right adjoint only if F commutes up to isomorphism with all generalized colimits which exist in A and B. Here, for any functor D′ ⟶^{L} D, generalized limits in A along L and generalized colimits in A along L are, when they exist, respectively right and left adjoint to the induced functor A^{L}. These generalized colimits include direct limits in the usual sense as well as free products and pushouts and evaluation adjoints; for many A of importance, they exist for all L with D′ and D smaller than some fixed regular cardinal, but they will exist for all L iff A is a category in which the morphisms reduce to nothing more than a preordering on the objects, with respect to which the latter form a complete lattice.

The general adjoint functor theorem asserts that if a functor B ⟶^{U} A satisfies the necessary continuity condition mentioned above, then it will have a left adjoint provided that B is suitably complete and U is suitably bounded. Freyd’s Special Adjoint Functor Theorem shows that certain categories B (such as the category of sets or of abelian groups, but not the category of groups) are “compact” in the sense that every continuous U to a standard A (say the category of sets) is bounded. A schema formalizing these adjoint functor theorems for the case where A and B are replaced by metacategories comparable to the conceptual universe would, on the one hand, justify by itself a large portion of the existential richness of that universe, as follows at least to the extent of the higher types and of infinite objects from the following section, and on the other hand, provide a common rationale for the inevitability and basic properties of a large number of mathematical constructions, as the following examples indicate.

If Top denotes the category of continuous mappings of topological spaces, the diagonal functor

Top ⟶ Top × Top

has a right adjoint, which forces the definition of product topology. If A denotes, say, the unit interval, then

Top ⟶^{A×( )} Top

also has a right adjoint, yielding the construction of the compact-open topology on path spaces. The inclusion functor Comp ⟶ Top from the category of continuous mappings between compact spaces has a left adjoint, giving the Stone-Čech compactification construction.

Turning to algebra, the forgetful functor Gps ⟶ Sets, which views every grouphomomorphism as a mapping of the carrier sets, has a left adjoint, yielding the notion of free groups. The “commutator bracket” functor Assoc ⟶ Lie, which interprets every homomorphism of associative linear algebras as a homomorphism of the same underlying vector spaces viewed only as Lie algebras, has also a left adjoint, yielding universal enveloping algebras. These two adjoint situations belong to a special large class, which also includes abelianization of groups, monoid rings, symmetric algebras, etc.

There are also adjoint situations in analysis, leading for example to l^{1} spaces and almost-periodic functions. Needless to say, viewing all these constructions explicitly as adjoint situations seems to have certain formal and conceptual utility apart from any philosophical attempt to unify their necessity.

3. Cartesian-closed Categories and Hyperdoctrines

A cartesian closed category is a category C equipped with adjoint situations of the following three sorts:

(1) A terminal object 1 ⟶^{1} C, meaning a right adjoint to the unique C ⟶ 1; if η denotes the adjunction, then C ⟶^{Cη} 1 is the unique morphism in C with domain C and codomain 1, for each object C.

(2) A product C × C ⟶^{×} C, meaning a right adjoint to the diagonal functor C ⟶ C×C. Denoting the adjunction and co-adjunction by δ and π respectively, we have Xδ as a diagonal morphism X ⟶ X ×X and (Y_{0}, Y_{1})π as a projection pair usually denoted for short by

Y_{0} × Y_{1} ⟶^{π_{0}} Y_{0}, Y_{0} × Y_{1} ⟶^{π_{1}} Y_{1}.

Given morphisms X ⟶^{f_{0}} Y_{0}, X ⟶^{f_{1}} Y_{1}, then ⟨f_{0}, f_{1}⟩ = Xδ · (f_{0} × f_{1}) is the unique X ⟶ Y_{0} × Y_{1} whose compositions with the π_{i} are the f_{i}. The projection A × 1 ⟶ A is an isomorphism for any object A.

(3) For each object A, exponentiation by A, C ⟶^{( )^{A}} C, meaning a right adjoint to the functor C ⟶^{A×( )} C. Denote by λ_{A} and ε_{A} the adjunction and co-adjunction respectively. Then

X ⟶^{Xλ_{A}} (A × X)^{A} and A × Y^{A} ⟶^{Y ε_{A}} Y,

and for any A × X ⟶^{h} Y, one has that

X ⟶^{Xλ_{A}.h^{A}} Y^{A}

is the unique morphism g for which (A × g).Y ε_{A} = h. For any morphism A ⟶^{f} Y, one may consider in the above process the case X = 1, h = (⟨A, 1⟩π_{1})^{−1}.f, obtaining a morphism 1 ⟶ Y^{A} denoted for short by ⌜f⌝; every morphism 1 ⟶ Y^{A} is of form ⌜f⌝ for a unique A ⟶^{f} Y. Now for any 1 ⟶^{a} A, A ⟶^{f} Y, one has that

⟨a⌜f⌝⟩.Y ε_{A} = a.f,

which justifies calling Y ε_{A} the evaluation morphism, though in most cartesian closed C, a paucity of morphisms with domain 1 prevents the last equation from determining ε.

From the uniqueness of adjoints it is clear that any two cartesian closed categories with a given category C are uniquely isomorphic. Most categories C cannot be made into cartesian closed categories at all. The category of all mappings between finite sets can be made cartesian closed, as can many larger categories of mappings between sets. Also, order-preserving mappings between partially ordered sets can be made cartesian closed, Y^{A} then being necessarily isomorphic to the set of order-preserving mappings A ⟶ Y equipped with the usual pointwise partial ordering. Another kind of example is provided by a Brouwerian semi-lattice, these being essentially co-extensive with the “trivial” cartesian closed categories (those in which there is at most one morphism X ⟶ Y for any given objects X and Y, or equivalently those in which all diagonal morphisms Xδ are isomorphisms X ⟶ X × X). More examples will appear presently.

A hyperdoctrine shall consist of at least the following four data

1. A cartesian closed category T. We will refer sometimes to the objects of T as types, to the morphisms in T as terms, and to the morphisms 1 ⟶ X in particular as constant terms of type X.

2. For each type X, a corresponding cartesian closed category P (X) called the category of attributes of type X. Morphisms of attributes will be called deductions over X, entailments, or inclusions as is appropriate. The basic functors giving P (X) its closed structure will be denoted by

1_{X}, ∧_{X}, α_{X} ⇒ ( )

to distinguish them from the analogous

1, ×, ( )^{A}

in T (the subscripts X may be omitted when no confusion is likely). Thus the evaluation morphisms in P (X) for each pair of objects α, ψ in P (X)

α ∧_{X} (α ⇒ ψ) ⟶ ψ

may be sometimes more appropriately referred to as the modus ponens deductions.

3. For each term X ⟶^{f} Y (morphism in T) a corresponding functor

P (Y) ⟶^{f·( )} P (X).

Then for any attribute ψ of type Y, f · ψ will be called the attribute of type X resulting from substituting f in ψ. We assume that for Y ⟶^{g} Z, (f.g)·ζ = f ·(g·ζ) for all attributes ζ of type Z (at least up to coherent isomorphism) and similarly for deductions over Z.

4. For each X ⟶^{f} Y in T two further functors

P (X) ⟶^{( )Σf} P (Y) and P (X) ⟶^{( )Πf} P (Y)

equipped with adjunctions that make them respectively left and right adjoint to substitution f. For any object φ in P (X) we call φΣf (respectively φΠf) the existential (respectively universal) quantification of φ along f. For ψ in P (Y), the adjointnesses reduce to two (natural) bijections, one between deductions φΣf ⟶ ψ over Y and deductions φ ⟶ f · ψ over X, and the other between deductions ψ ⟶ φΠf over Y and deductions f · ψ ⟶ φ over X. From the assumed functorality of substitution we have for a further term Y ⟶^{g} Z that φΣ(f.g) = (φΣf)Σg and φΠ(f.g) = (φΠf)Πg, at least up to an invertible deduction in P (Z).

Now among general features of hyperdoctrines we note for example that the existence of existential quantification implies that substitution commutes with conjunction; usually substitution does not commute with implication, as one of our examples below shows. There is at least one interesting realm that has roughly all the features of a hyperdoctrine except existential quantification, namely sheaf theory, wherein T is the category of continuous mappings between Kelley spaces^{2} and P (X) is the category of (morphisms between) set-valued sheaves on X.

Also, in a general hyperdoctrine we can construct for each term X ⟶^{f} Y the attribute 1_{X}Σ⟨X, f⟩ of type X ×Y which plays the role of the graph of f; in particular the graph of the identity morphism on X is an object in P (X × X) having the rudimentary properties of equality. With help of equality, graphs, and the behavior of quantification under composition of terms, one can in certain hyperdoctrines reduce the general quantification to quantification along very special terms, namely projections Y × Z ⟶ Y.

Any (single-sorted) theory formalized in higher-order logic yields a hyperdoctrine in which types are just all expressions 1, V, V^{V}, V × V, (V × V)^{(V ×V ×V)^{V}}, etc. and in which terms are identified if they are in the theory provably equal (we assume that “higherorder logic” does involve at least terms corresponding to the δ, π, λ, ε necessary to yield a cartesian closed category by this procedure). In this hyperdoctrine, we let the objects of P (X) be those formulas of the theory whose free variables are of type X (for example if X = V × V^{V}, P (X) consists of the formulas with two free variables, one an “element” variable and the other a “function” variable, but with bound variables of arbitrary type) and we let the morphisms of P (X) be simply entailments deducible in the theory. Thus the diagonal φ ⟶ φ ∧_{X} φ is an isomorphism in this example. Also each P (X) has a coterminal object 0_{X} (falsity) with a deduction φ ⟶ (φ ⇒_{X} 0_{X}) ⇒_{X} 0_{X} which is an isomorphism if the logic is classical. If the theory is number theory, then T participates in another adjoint situation (setting ω = V)

[figure: T; T; ω×( )]

2Intended here are the k-spaces of Hurewicz, which are well-described in the book General Topology by J. L. Kelley.

where the unlabeled right adjoint functor is the forgetful functor from the category whose objects correspond to endomorphisms X ⟶^{t} X in T and whose morphisms are diagrams

[figure: X; t; h; Y; s]

in T with t.h = h.s. Conversely, any cartesian closed category in which this forgetful functor has a left adjoint will contain a definite morphism corresponding to each highertype primitive recursive function, and if the category contains somewhere at least one non-identity endomorphism, then there will be an infinite number of morphisms 1 ⟶ ω in the category.

We also obtain a hyperdoctrine if we consider as types arbitrary sets, as terms arbitrary mappings, and as attributes arbitrary subsets, (i.e. P (X) = 2^{X}) and take substitution as the inverse image operator, which forces existential quantification to be the direct image operator. With the appropriate definition of morphism between hyperdoctrines, such a morphism into this one from a higher order theory (as in the previous paragraph) involves nothing more nor less than a model of the theory in question.

A different hyperdoctrine with the same category of types and terms (namely arbitrary sets and mappings) is obtained by defining P (X) = (T, X) = the category of “sets over X” whose morphisms are arbitrary commutative triangles

\xymatrix{A \ar[rr]^{d} \ar[dr]_{φ} &  & A′ \ar[dl]^{φ′} \\  & X}

of mappings of sets, and taking for f · ψ (when X ⟶^{f} Y and B ⟶^{ψ} Y) the projection to X of the set of pairs ⟨x, b⟩ with xf = bψ. Then existential quantification is simply composition φΣf = φ.f . Since P (1) = T, for any element 1 ⟶^{x} X and “property” φ in P (X), x · φ is simply a set, the “fiber” of φ over x. Calling a deduction 1_{X} ⟶ φ over X a “proof” of φ, and noting that in the present example 1_{X} is just the identity mapping, we see that a proof of φ is a mapping that assigns to each x a proof of x · φ. Then a proof of φΣf is a mapping that assigns to each y a specific x such that xf = y, together with a proof of x · φ. Since the fiber over y of a universal quantification y.(φΠf) = Πx · φ, a proof of φΠf involves a mapping that assigns to each y a mapping that assigns to each x with xf = y a proof that x · φ, and more generally deductions with premises other than 1_{X} have similar descriptions. The validity of the axiom of choice in T then implies that

(T, X) ⟶^{direct image} 2^{X}

commutes with all the “propositional” and quantificational operations and hence defines the strictest sort of morphism from the present hyperdoctrine to the previous one. Since in this case every ψ in P (Y) is of the form 1_{X}Σf = ψ for a unique X and f, it is possible to view conjunction and implication as particular cases of substitution and universal quantification. In particular a deduction over X of a conjunction φ_{1} ∧_{X} φ_{2} involves an ordered pair of mappings, each of which may be an arbitrary deduction of φ_{1}, or φ_{2} respectively; this language makes clear the reasonableness of the non-idempotence of conjunction.

As a final example of a hyperdoctrine, we mention the one in which types are finite categories and terms arbitrary functors between them, while P (A) = S^{A}, where S is the category of finite sets and mappings, with substitution as the special Godement multiplication. Quantification must then consist of generalized limits and colimits, while implication works like this: α ⇒ ψ is a functor whose value at an object A in A is the set of natural transformations h_{A} × α ⟶ ψ, where h_{A} : A ⟶ S is the “representable” functor assigning to A′ the set of morphisms A(A, A′). By focusing on those A having one object and all morphisms invertible, one sees that this hyperdoctrine includes the theory of permutation groups; in fact, such A are groups and a “property” of A is nothing but a representation of A by permutations. Quantification yields “induced representations” and implication gives a kind of “intertwining representation”. Deductions are of course equivariant maps.

4. Globalized Galois Connections in Algebraic Geometry and in Foundations

If O_{1} and O_{2} are partially ordered sets the traditional notion of a Galois connection between them is easily seen to be equivalent to an adjoint situation

\xymatrix{O_{1}^{op} \ar[r] & O_{2} \ar[l]}

between the corresponding trivial categories (one of them turned opposite). Recently it has begun to appear that the basic examples of Galois connections are really just fragments of more global adjoints which involve non-trivial categories and which carry more information.

For example, Galois theory itself has profitably been treated as the study of adjoint situations

[figure: Alg; {op \atop k}; Sets; Gal(\overline{k},k)]

where the left-hand category has as objects all commutative and associative linear algebras over a field k and the right-hand all continuous permutation representations of the compact Galois group of the separable closure \overline{k} of k, while the left-to-right right adjoint functor assigns to every k-algebra A the representation by permutations of the set Alg_{k}(A, \overline{k}) of all algebra homomorphisms A ⟶ \overline{k}. Restricting to subalgebras of \overline{k} on the one hand and to quotients of the regular representation on the other retrieves in effect the usual Galois connection. Similarly, in algebraic geometry the Galois connection between ideals in a polynomial ring k[x_{1}, …, x_{n}] and subsets of k^{n} has been globalized to an adjoint situation

Alg_{k}^{op} [figure: spec; Γ]Schema_{k}

where Γ assigns the algebra of global functions to each scheme.

Finally, in Foundations there is the familiar Galois connection between sets of axioms and classes of models, for a fixed set of relation variable R_{i}. Globalizing to an adjoint pair allows making precise the semantical effects, not only of increasing the axioms, but also of omitting some relation symbols or reinterpreting them in a unified way. The categories of models then reciprocally determine their own full sets of natural relation variables, thus giving definability theory a new significance outside the realm of axiomatic classes. To do this for a given species — equational, elementary, higher-order, etc. — of, say, I-sorted theories, one defines an adjoint situation

\xymatrix{Theories^{op} \ar[r]^{semantics} & (Cat, [Sets^{I}]) \ar[l]^{structure}}

in which the right hand side denotes a category whose morphisms are commutative triangles

\xymatrix{C \ar[rr] \ar[dr] &  & C′ \ar[dl] \\  & _{Sets_{I}}}

of functors with C and C′ more or less arbitrary categories. The invariant notion of theory here appropriate has, in all cases considered by the author, been expressed most naturally by identifying a theory T itself with a category of a certain sort, in which case the semantics (categories of models) of T is a certain subcategory of the category of functors T ⟶ Sets^{I}. There is then a further adjoint situation

\xymatrix{Formal \ar[r] & Theories \ar[l]}

describing the presentation of the invariant theories by means of the formalized languages appropriate to the species. Composing these two adjoint situations, and tentatively identifying the Conceptual with categories of the general sort (Cat, [Sets^{I}]), we arrive at a family of adjoint situations

\xymatrix{Formal^{op} \ar[r] & Conceptual \ar[l]}

(one for each species of theory) which one may reasonably hope constitute the fragments of a precise description of the duality with which we began our discussion.

16  F. WILLIAM LAWVERE

Bibliography

Eilenberg, S., and Kelly, G.M., Closed Categories, Proceedings of the Conference on Categorical Algebra (La Jolla 1965), Springer Verlag 1966.

Eilenberg, S., and Mac Lane, S., General Theory of Natural Equivalences, Trans. Amer. Math. Soc. 58, 231–294 (1945).

Kan, D. M., Adjoint Functors, Trans. Amer. Math. Soc. 87, 294–329 (1958).

Lawvere, F. W., Functorial Semantics of Algebraic Theories, Proc. Nat. Acad. Sc. U.S.A. 50, 869–872 (1963).

Lawvere, F. W., The Category of Categories as a Foundation for Mathematics, Proceedings of the Conference on Categorical Algebra (La Jolla 1965), Springer Verlag 1966 [See also Review 7332 by J. Isbell, Dec. 1967, Math. Reviews].

Mac Lane, S., Categorical Algebra, Bull. Amer. Math. Soc. 71, 40–106 (1965).

This article may be accessed via WWW at http://www.tac.mta.ca/tac/reprints or

by anonymous ftp at

ftp://ftp.tac.mta.ca/pub/tac/html/reprints/articles/16/tr16.{dvi,ps,pdf}