[rm]bfb
Cartesian closed
varieties I:
The classification theorem
Abstract.
In 1990, Johnstone gave a syntactic characterisation of the equational theories whose associated varieties are cartesian closed. Among such theories are all unary theories—whose models are sets equipped with an action by a monoid —and all hyperaffine theories—whose models are sets with an action by a Boolean algebra . We improve on Johnstone’s result by showing that an equational theory is cartesian closed just when its operations have a unique hyperaffine–unary decomposition. It follows that any non-degenerate cartesian closed variety is a variety of sets equipped with compatible actions by a monoid and a Boolean algebra ; this is the classification theorem of the title.
1. Introduction
In [10], Johnstone considered the following very natural question: when is a variety—by which we mean the category of models of a single-sorted equational algebraic theory—a cartesian closed category? This was, in fact, a follow-up to an earlier question—“when is a variety a topos?”—asked by Johnstone in [9], with the answers in the two cases turning out to be surprisingly similar. The solutions Johnstone provides are syntactic recognition theorems, giving necessary and sufficient conditions on the operations of an equational theory for the variety it presents to be cartesian closed or a topos. We recall the cartesian closed result as Theorem 5.2 below, and the reader will readily observe that, while a little delicate, the conditions involved are straightforward enough to be practically useful; and indeed, a very similar set of conditions finds computational application in [13].
Be this as it may, Johnstone’s conditions do little to help us delineate the scope of the cartesian closed varieties. Much as we can say that every Grothendieck topos is the topos of sheaves on a site, we would like to say that every cartesian closed variety is … and filling this gap would amount to providing a semantic classification theorem for cartesian closed varieties. This is one of the main objectives of this paper: we will show that every cartesian closed variety is the variety of sets endowed with two actions, one by a monoid and one by a Boolean algebra , which interact in a suitable way. Thus, our classification shows that any cartesian closed variety is a kind of “bicrossed product” of the variety of -sets, which as a presheaf category, is well known to be cartesian closed; and the variety of -sets, as introduced in [1] and recalled in Section 3, which was shown to be cartesian closed in [10, Example 8.8].
Our semantic classification theorem will be obtained by way of a syntactic classification theorem derived from Johnstone’s recognition theorem. To motivate this result, observe first that the cartesian closed varieties of -sets are precisely those which can be presented by unary algebraic theories, that is, theories whose operations and equations are all of arity . On the other hand, as shown in [10] and recalled in Section 4, the cartesian closed varieties of -sets are precisely those which are presented by hyperaffine algebraic theories, that is ones whose every operation is hyperaffine (Definition 4.1); here, for (say) a ternary operation , hyperaffineness asserts that , i.e., is affine, and moreover that:
Our syntactic classification theorem (Theorem 5.5) now states that:
Theorem.
An equational theory presents a cartesian closed variety if, and only if, every operation has a unique decomposition as a hyperaffine operation applied to a unary one , i.e., .
The proof of this result is simply Johnstone’s recognition theorem together with a little calculation, but we should note that our result does not supplant Johnstone’s, but rather complements it: for while our condition may be simpler to state, it is harder to check if one wants to determine if a given variety is cartesian closed.
Where our formulation comes into its own is in deriving our semantic classification theorem. If presents a cartesian closed variety, then the syntactic classification theorem tell us that its operations are completely determined by the monoid of unary operations together with the subtheory of hyperaffine operations. However, just knowing these is not enough to recover the substitution of our equational theory, and so we must also record the manner in which and act on each other by substitution. This leads to what we term a matched pair of theories (Definition 6.3), and our second main result (Theorem 6.9):
Theorem.
The category of non-degenerate cartesian closed varieties is equivalent to the category of non-degenerate matched pairs of theories.
Applying the correspondence between hyperaffine algebraic theories and theories of -sets over Boolean algebras now transforms each matched pair of theories into what we term a matched pair of algebras (Definition 7.1). This involves a Boolean algebra and a monoid such that is a -set, is an -set, and various further equational axioms hold. In fact, this structure has been studied in the literature: in the nomenclature of [6], we would say that is a -monoid. Concomitantly, we have a notion of -set (Definition 7.3), which is a set equipped with -action and -action in a manner which is compatible with the -action on and the -action on . In terms of this, we finally obtain our semantic classification result (Theorem 7.10):
Theorem.
The category of non-degenerate cartesian closed varieties is equivalent to the category of non-degenerate matched pairs of algebras via an equivalence which identifies the matched pair with the cartesian closed variety of -sets.
There is one point we should clarify about the preceding result. As stated, it is only valid for varieties and equational theories which are finitary, i.e., generated by operations of finite arity. However, in the paper proper, it will also be valid in the infinitary case; and the adjustments needed to account for this are entirely confined to the Boolean algebra side of things. Indeed, whereas finitary hyperaffine theories correspond to Boolean algebras , arbitary hyperaffine theories correspond to strongly zero-dimensional locales; these are locales (= complete Heyting algebras) in which every cover can be refined to a partition. Two different proofs of this correspondence can be found in [10, Example 8.8] and in [7, §2]; we in fact provide a third proof (Theorem 4.9), but with respect to a slightly different presentation of strongly zero-dimensional locales, inspired by [14]: we consider Boolean algebras equipped with a collection of well-behaved partitions of , under axioms which make them correspond to strongly zero-dimensional topologies on . We refer to such a pair as a Grothendieck Boolean algebra ; and we now have notions of Grothendieck matched pair of algebras and of -set which, when deployed in the theorem above, make it valid for infinitary cartesian closed varieties.
This concludes our overview of the paper, and the reader will notice that we give scarcely any examples. The justification for this is the companion paper [5], which begins a programme to develop the theory of -sets and link them to structures from operator algebra; in particular, we will see that any matched pair has an associated topological category, and that for suitable, and natural, choices of , we can recover the étale topological groupoids which give rise to structures such as Cuntz -algebras, Leavitt path algebras, and -algebras associated to self-similar groups, and so on.
2. Background
2.1. Conventions
Given sets and we write for the set of functions from to . If , we write for the value of the function at ; on the other hand, given a family of elements , we write for the corresponding element of . Given , and , we may write for the function which agrees with except that its value at is given by . We may identify a natural number with the set .
A category is concrete if it comes equipped with a faithful functor to the category of sets. This is often an obvious “forgetful” functor, in which case we suppress it from our notation. A concrete functor is a functor with . Such an associates to each -structure on a set a corresponding -structure, in such a way that each -homomorphism is also a homomorphism of the associated -structures. A concrete isomorphism is an invertible concrete functor; this amounts to a bijection between -structures and -structures on each set for which the homomorphisms match up.
If is a concrete category and a set, then a free -object on is a -object endowed with a function , the unit, such that, for any -object , each function has a unique factorisation through via a -homomorphism . We say that free -structures exist if they exist for every set ; this is equivalent to the faithful functor having a left adjoint.
2.2. Varieties and algebraic theories
By a variety , we mean the concrete category of (possibly empty) models of a (possibly infinitary) single-sorted equational theory. For theories with a mere set of function symbols, free -structures always exist; we will relax this by allowing a proper class of function symbols, but still assuming that free -structures exist. So the category of complete join-lattices is a variety in our sense, but not the category of complete Boolean algebras. We write for the category of varieties and concrete functors between them.
A variety is non-degenerate if it contains a structure with at least two elements. To within concrete isomorphism, there are two degenerate varieties: is the full subcategory of on the one-element sets, while is the full subcategory on the zero- and one-element sets. The former is the category of models of the equational theory with no operation symbols and the axiom ; while the latter is the category of models of the theory with a single constant and the axiom .
A given variety may be axiomatised by operations and equations in many ways; however, there is always a maximal choice, which is captured by the following notion of algebraic theory. This is what a universal algebraist would call an (infinitary) abstract clone, and what a category theorist would call a monad relative to the identity functor .
Definition 2.1 (Algebraic theories).
An algebraic theory comprises:
-
•
For each set , a set of -operations of arity ;
-
•
For each set and , an element (the th projection);
-
•
For all sets a substitution function , written as , or when as ;
all subject to the axioms:
-
•
for all ;
-
•
for all and ;
-
•
for all , and .
If and are algebraic theories, then a homomorphism of algebraic theories comprises functions for each set , such that:
-
•
for all ;
-
•
for all and .
We write for the category of algebraic theories and homomomorphisms.
An algebraic theory is said to be non-degenerate if , or equivalently, if implies . To within isomorphism, there are exactly two degenerate algebraic theories: , in which for all ; and , in which and otherwise.
When working with an algebraic theory we will deploy variable notation. For example, in the algebraic theory of semigroups, the defining axiom is expressed by the equality left below in ; however, we would prefer to write it as to the right.
We may do so if we view this right-hand equality as universally quantified over all sets and all elements . It then implies the left-hand equality on taking , and conversely, is implied by the left equality via substitution. Our convention throughout will be that any -, - or -symbol (possibly subscripted) appearing in an equality is to be interpreted in this way.
2.3. Semantics and realisation
We now draw the link between algebraic theories and varieties via the semantics of an algebraic theory.
Definition 2.2 (Category of models of a theory).
A model for an algebraic theory is a set together with for each set an interpretation function , written as satisfying the following axioms:
-
•
for all and ;
-
•
for all , and .
A -model homomorphism is a function with for all and . We write for the concrete category of -models and homomorphisms.
The category can be presented as the models of an equational first-order theory, whose proper class of function-symbols is given by the disjoint union of the ’s. Moreover, free -models exist; for indeed, given a set , the set becomes a -model on defining , and now the map sending to exhibits as free on . Thus, the concrete category is a variety for any theory . In fact, this process is functorial:
Definition 2.3 (Semantics of algebraic theories).
For any homomorphism of algebraic theories, we write for the concrete functor which to each -model associates the -model structure on with . We write for the functor sending each algebraic theory to its concrete category of models, and each homomorphism to .
A basic result in the functorial semantics of algebraic theories is that is an equivalence of categories. In particular, it is essentially surjective, which is to say that every variety is realised by some algebraic theory; here, we say that an algebraic theory realises a variety if and are concretely isomorphic. For example, the degenerate varieties , are realised by the degenerate algebraic theories , . In general, we can find a which realises a variety using free objects in . Writing for the free -object on , with unit , the desired theory has sets of operations ; projection elements ; and substitution given by .
2.4. Cartesian closed varieties
Any variety has finite products, with the product of being with the componentwise -structure. We say is cartesian closed if for every , the functor has a right adjoint. More elementarily, this means that for every in , there is a “function-space” and a homomorphism (“evaluation”), such that for all , there is a unique with . Note that, in particular, the degenerate varieties and are cartesian closed, since they are equivalent to the one- and two-element Heyting algebras respectively.
The simplest possible class of non-degenerate cartesian closed varieties are the varieties of -sets for a monoid : sets equipped with an associative, unital left -action. It is well known that the variety of -sets, being a presheaf category, is cartesian closed; we record the structure here for future reference.
Proposition 2.4.
The variety of -sets is cartesian closed.
Proof.
For -sets and , the function-space is the set of -set maps (where acts on itself by multiplication) under the action
(2.1) |
Evaluation is given by ; and given a homomorphism , its transpose is given by . ∎
3. Boolean algebras and -sets
3.1. Varieties of -sets
In this section, we discuss another important class of non-degenerate cartesian closed varieties, namely the varieties of -sets for a Boolean algebra , as introduced by Bergman in [1]. In what follows, we write for the distributive lattice structure of a Boolean algebra , and for its negation; we say that is non-degenerate if .
Definition 3.1 (Variety of -sets).
Let be a non-degenerate Boolean algebra. A -set is a set endowed with an action , written , satisfying the axioms
(3.1) | ||||
We write for the variety of -sets.
As explained in [1], the first three axioms make each into a decomposition operation [12, Definition 4.32], meaning that it induces a direct product decomposition where and are quotients of by suitable equivalence relations. The first equivalence relation is defined by
(3.2) |
the second dually relates and just when but, in light of the fifth -set axiom, can equally be described as . In fact, as in [12, Theorem 4.33], we can recover from and , since is the unique element of with
(3.3) |
Thus, we can recast the notion of -set in terms of a set equipped with a suitable family of equivalence relations:
Proposition 3.2.
Let be a non-degenerate Boolean algebra. Each -set structure on a set induces equivalence relations as in (3.2) which satisfy:
-
(i)
If and then ;
-
(ii)
if and only if , and always;
-
(iii)
If and then ;
-
(iv)
For any and , there is such that and .
Any family of equivalence relations satisfying (i)–(iv) arises in this way from a unique -set structure on whose operations are characterised by (3.3). Furthermore, under this correspondence, a function between -sets is a homomorphism if and only it preserves each equivalence relation .
Proof.
Given -set structure on , each as in (3.2) is an equivalence relation by [12, Lemma on p.162]. To verify (i), if and , then , so . Next, (ii) follows immediately from and . For (iii), if and , then . Finally, for (iv), we take ; then and as desired. We argued above that we can reconstruct the -set operations from the ’s, so this gives an injective map from -set structures on to families of equivalence relations satifying (i)–(iv).
To show surjectivity, consider a family satisfying (i)–(iv). For any and , the element whose existence is asserted by (iv) is, by (ii) and (iii), unique. If we write it as as in (3.3), then we claim this assignment endows with -set structure. Indeed:
-
•
Since and , we have ;
-
•
Since and , we have , and likewise we have ;
-
•
Since is the only with , we have ;
-
•
Since and we have ;
-
•
By (i) we have . Similarly , and also , whence by (iii), . Thus .
Moreover, this -set structure induces the given equivalence relations ; indeed, since and we have by (i)–(iii) that if and only if . Finally, any -set homomorphism clearly preserves each ; conversely, if preserves each , then from (3.3) in we have and , and so by (3.3) in . ∎
Remark 3.3.
Conditions (i)–(iii) above say that, for any elements of a -set , the set is an ideal of the Boolean algebra ; and since each is an equivalence relation, the function is an -valued equivalence relation, in the sense that , and . So becomes an -valued set in the sense of [4]—but one of a rather special kind, since in a general -valued set the equality need only be a partial equivalence relation. As explained in [4], -valued sets are a way of presenting sheaves on , and so the preceding observations draw the link between -sets and sheaves that was central to [1]. In this context, the totality of our reflects the fact that the elements of a -set correspond to total elements of the corresponding sheaf.
By exploiting Proposition 3.2 we can now prove easily that:
Proposition 3.4.
The variety of -sets is cartesian closed.
Proof.
Given -sets and , we consider the set of -set homomorphisms . We claim this is a -set under the pointwise equivalence relations . Only axiom (iv) is non-trivial. So suppose and . For each , we have such that and , and so will satisfy and so long as it is in fact a homomorphism. So suppose that in ; we must show . Since and (as is a homomorphism) we have by (i) that ; and similarly . Thus by (iii) and so is a homomorphism as desired. So is a -set under the pointwise structure; whereupon it is clear that the usual evaluation map is a homomorphism, and that for any homomorphism , the usual transpose is a homomorphism: so is a function-space as desired. ∎
3.2. Varieties of -sets
If is a finite set, then as in [10, Proposition 4.3], a -set structure on a set determines and is determined by equivalence relations on , for which the quotient maps exhibit as the product of the sets . Thus the category of -sets is equivalent to the category of -fold cartesian products of sets. However, this does not carry over to infinite sets , for which a -set is more general than an -fold cartesian product of sets. The reason is that the notion of -set does not pay regard to the infinite joins needed to construct each from atoms . This can be rectified by equipping with a suitable collection of “well-behaved” joins.
Definition 3.5 (Partition).
Let be a Boolean algebra and . A partition of is a subset such that , and whenever . An extended partition of is a subset (possibly containing ) satisfying the same conditions. If is an extended partition of , then we write for the corresponding partition. We say merely “partition” to mean “partition of ”.
Definition 3.6 (Zero-dimensional topology, Grothendieck Boolean algebra).
A zero-dimensional topology on a Boolean algebra is a collection of partitions of which contains every finite partition, and satisfies:
-
(i)
If , and for each , then ;
-
(ii)
If and is a surjective map, then each join exists and .
A Grothendieck Boolean algebra is a Boolean algebra with a zero-dimensional topology . A homomorphism of Grothendieck Boolean algebras is a Boolean homomorphism such that implies .
A zero-dimensional topology on is a special kind of Grothendieck topology on in the sense of [8, §II.2.11], wherein the covers of are the elements of , and the covers of an arbitrary are given by:
Definition 3.7 (Local partitions).
Let be a Grothendieck Boolean algebra and . We write for the set of partitions of characterised by:
However, our presentation follows not [8] but rather [14]—according to which, our Grothendieck Boolean algebras are the “subcomplete, locally refinable Boolean partition algebras”. Via the general theory of [8, §II.2.11], any Grothendieck Boolean algebra generates a locale (= complete Heyting algebra) given by the set of ideals which are -closed, meaning that as soon as for some . The locales so arising are the strongly zero-dimensional locales considered in [7], and in fact, our category of Grothendieck Boolean algebras is dually equivalent to the category of strongly zero-dimensional locales [15, Theorem 24].
Definition 3.8 (Variety of -sets).
Let be a non-degenerate Grothendieck Boolean algebra. A -set is a -set endowed with a function for each infinite , satisfying:
(3.4) |
We write for the variety of -sets.
Note that any non-degenerate Boolean algebra has a least zero-dimensional topology given by the collection of all finite partitions of . In this case, -sets are just -sets, so that Definition 3.8 includes Definition 3.1 as a special case.
While the existence of functions like above looks like extra structure on a -set, it is in fact a property, rather like the existence of inverses in a monoid:
Proposition 3.9.
Let be a non-degenerate Boolean algebra and a partition of .
-
(i)
An operation on a -set satisfying the axioms (3.4) is unique if it exists.
-
(ii)
If and are -sets admitting the operation , then any homomorphism of -sets will preserve it.
Proof.
For (i), suppose and both satisfy the axioms of (3.4). For any we have and so . For (ii), let again; since and preserves , we have , and so
It follows that is a full subcategory of . We can also characterise this subcategory in terms of the induced equivalence relations of Proposition 3.2.
Proposition 3.10.
Let be a non-degenerate Grothendieck Boolean algebra. A -set is a -set if, and only if, for each infinite and , there is a unique element with for all .
Proof.
First, suppose is a -set. Given infinite and , we define ; we now have by the right-hand axiom in (3.4), and if for each , then by the other two axioms, so that is unique with the desired property.
Suppose conversely that the stated condition holds; we endow with -set structure. Given infinite and , we define as the unique element such that for all . Since just when we have for all ; we also have as for each . Finally, for the second axiom in (3.4), given we have and so by unicity. ∎
There is some awkwardness above in the distinction between infinite and non-infinite partitions; but in fact, this can be avoided.
Proposition 3.11.
Let be a non-degenerate Grothendieck Boolean algebra. A family of equivalence relations on a set determines -set structure on if, and only if, it satisfies axiom (i) of Proposition 3.2 together with
-
(ii)′
For any and , there is a unique with for all .
Proof.
Suppose first that (i) and (ii)′ hold. It suffices to show that axioms (ii)–(iv) of Proposition 3.2 also hold. (ii) and (iv) follow easily on applying (ii)′ to the partitions and respectively. As for (iii), given its hypotheses, let be unique by (ii)′ such that and . Then using (i) and the hypotheses, we have and . So agrees with on each part of and so ; whence as desired.
For the converse, we must show that (i)–(iv) of Proposition 3.2 imply (ii)′ for any finite partition . The unicity in (ii)′ holds by repeatedly applying axiom (iii) then axiom (i). For existence, the base case is trivial; so let us assume the result for , and prove it for . By induction, we find such that and for ; now by (iv) we can find such that and . Since for also for all , as desired. ∎
Again, using the equalities makes it easy to show that -sets are a cartesian closed variety. First we need a preparatory lemma.
Lemma 3.12.
Let be a -set and let .
-
(i)
For any and , if for all , then .
-
(ii)
For any , if for all , then .
Proof.
For (i), first note by applying condition (i) for a zero-dimensional topology with , and . Now let be unique such that and . For each we have , and so agrees with on each part of the partition in . Thus and so as desired. For (ii), apply (i) with . ∎
Remark 3.13.
Note that part (ii) of this Lemma asserts that, for all elements in a -set , the ideal of Remark 3.3 is a -closed ideal.
Proposition 3.14.
The variety of -sets is cartesian closed.
Proof.
It suffices to show that for -sets and , the -set exponential of Proposition 3.14 is itself a -set. So suppose given a partition and a family of homomorphisms for each , and define by the property that for each ; this will be unique such that for each , so long as it is a -set map. So suppose that ; we must show that , for which by the preceding lemma it suffices to show that for all : and this follows exactly as in Proposition 3.4. ∎
3.3. Theories of -sets and -sets
To conclude this section, we describe algebraic theories which realise the varieties of -sets and -sets.
Definition 3.15.
Let be a non-degenerate Grothendieck Boolean algebra. A -valued distribution on a set is a function whose restriction to is an injection onto a partition in . The theory of -sets has given by the set of -valued distributions on ; the projection element given by if and otherwise; and the composition of and given by , where this join exists using axioms (ii) and (iii) for a zero-dimensional topology.
When is the topology of finite partitions, we will write in place of and call it the theory of -sets. In this case, a -valued distribution is simply an whose support injects onto a finite partition of .
Proposition 3.16.
For any non-degenerate Grothendieck Boolean algebra the theory of -sets realises the variety of -sets. In particular, for any non-degenerate Boolean algebra, the theory of -sets realises the variety of -sets.
Proof.
Suppose first that is a -model. For each , we have the element with and , while for each infinite partition , we have the element given by the inclusion map . It is straightforward to verify that these elements satisfy the axioms of (3.1) and (3.4) in , so their interpretations equip any -model with the structure of a -set.
Suppose conversely that is a -set, and let and . Since is a partition in , we may use the -set structure of to define as the unique element with for all . We now check the two -model axioms. First, we have , i.e., . Second, given and and , we have and for all , and so . Now Lemma 3.12(ii) yields
but is unique with this property, whence .
Starting from a -set structure on , the induced -model on satisfies and , i.e., , and also satisfies for all , i.e., , and so yields the original -set structure back. Conversely, given a -model structure , the model structure induced from the associated -set satisfies , i.e., for each . But by an easy calculation, we have in , and so
Remark 3.17.
We can read off from this proof that the free -set on a set is given by , endowed with the -set structure in which just when for all . Given a partition and family of elements , the element is given by . The function exhibiting as free on is given by .
As a special case, the free -set on two generators can be identified with itself (with generators and ) under the -set structure of “conditioned disjunction”:
4. Hyperaffine theories
In this section, we describe, following [10, 7], the syntactic characterisation of theories of -sets as (non-degenerate) hyperaffine algebraic theories, with the -sets matching under this correspondence with the finitary hyperaffine theories.
As is well known, an algebraic theory is finitary if it corresponds to a finitary variety: which is to say that for each , there exist and such that . The notion of hyperaffine algebraic theory is perhaps slightly less familiar:
Definition 4.1 (Hyperaffine operation, hyperaffine algebraic theory).
Let be an algebraic theory. We say that is affine if in , and hyperaffine if also in . We say that is hyperaffine if each of its operations is so.
Our objective now is to prove:
Proposition 4.2.
A non-degenerate algebraic theory is hyperaffine if, and only if, it is isomomorphic to for some non-degenerate Grothendieck Boolean algebra ; and it is finitary and hyperaffine if, and only if, it is isomorphic to some .
For the “if” direction, we need only show that each is hyperaffine, and that each is finitary. For the first claim, since is a singleton, every operation of must be affine. To see that each is hyperaffine, we observe that and correspond to the elements of given by, respectively,
and these are equal since is an injection of onto a partition of . To show finitariness of each , note that any in has finite support ; so we have the element given by and see easily that . So is finitary.
The “only if” direction of Proposition 4.2 is harder, and we will attack it in stages. We begin by establishing an important property of hyperaffine theories:
Lemma 4.3.
If is a hyperaffine algebraic theory, then every pair of operations and commute, i.e., we have .
Proof.
The operation is hyperaffine, which says that
Now taking gives the desired result:
Now, we observed in Remark 3.17 that, in the theory of -sets, the Boolean algebra appears as the free -set on two generators. This indicates how we should reconstruct a Boolean algebra from a hyperaffine theory.
Proposition 4.4.
If is non-degenerate hyperaffine, then underlies a non-degenerate Boolean algebra with , , and , and determined by
Proof.
According to [3, Theorem 1], to give Boolean algebra structure on is to give constants and a ternary operation (thought of as encoding the Boolean operation “if then else ”) satisfying the five axioms:
(4.1) | ||||||||
and in this presentation, the usual Boolean operations , and are re-found as and and . In the case of , if we take and and to be the substitution operation in , then all but the last-displayed axiom are trivial. For this last axiom, we compute that using affineness of ; commutativity of and via Lemma 4.3; and affineness of . So is a Boolean algebra structure, with operations , and as displayed above; it is non-degenerate by the assumption that . ∎
We now explain how to endow the Boolean algebra of this proposition with a zero-dimensional topology. In this we follow [7, §2] by first introducing binary reducts and proving some important facts about them.
Definition 4.5 (Binary reducts).
Let be an algebraic theory and . For each subset , we write for the binary operation with
When is a singleton , we may write rather than .
Lemma 4.6.
Let be a non-degenerate hyperaffine algebraic theory, let be the Boolean algebra of Proposition 4.4, and let .
-
(i)
If for all then ;
-
(ii)
If then in ;
-
(iii)
For all , we have in .
Proof.
The elements of easily satisfy the axioms of (3.1) in and so via their action by substitution endow each with a -set structure. We claim that, with respect to this structure, we have for each that:
(4.2) |
To see that satisfies the displayed condition, fix and define if and otherwise; then we have as required. To show the unicity, suppose for each , and set if and otherwise; then as desired.
We now prove (i)–(iii). For (i), if for each , then for each , whence by unicity in (4.2). For (ii), (4.2) yields for , i.e., which says . Finally for (iii), observe that (4.2) implies that if and only if for all . Thus, for any , and , we have in just when , just when for all . In particular, if and only if for all , so as desired. ∎
This lemma implies, in particular, that if is hyperaffine and , then the set is a partition of . In this situation, we will say that the operation realises the partition .
Proposition 4.7.
Let be a non-degenerate hyperaffine theory and the Boolean algebra of Proposition 4.4. The set of all partitions realised by operations of constitutes a zero-dimensional topology on . If is finitary, then is necessarily the topology of finite partitions.
Proof.
We first show that any has a canonical realisation by a (necessarily unique) with for all . To this end, let be any realiser for , pick an arbitrary element , and define a function by taking if and otherwise; we now easily see that is the desired canonical realisation for .
We now verify the axioms for a zero-dimensional topology. First observe that the trivial partition is (canonically) realised by ; and that if all -fold partitions are realised, then so is every -fold partition : for indeed, if realises , then is easily seen to realise . So all finite partitions are in .
Now for (i), suppose given and for each . Let and be their canonical realisers, and consider the term with Easily we have so that realises the partition as desired. Finally for (ii), let with canonical realiser , and let be a surjection. Let in ; then by Lemma 4.6(iii), we have , so that realises the partition .
Finally, if is finitary, then we can write any as for some finite list . It follows that unless , so that partitions which realises are precisely the finite ones. ∎
The following result now completes the proof of Proposition 4.2.
Proposition 4.8.
Let be a non-degenerate hyperaffine theory, and the non-degenerate Grothendieck Boolean algebra of Propositions 4.4 and 4.7. The maps
(4.3) |
are the components of an isomorphism of algebraic theories . In particular, if is finitary, then we have an isomorphism .
Proof.
By Lemma 4.6 and definition of , each is injective from its support onto a partition in , so that the maps in (4.3) are well-defined.
For any it is clear that . As for preservation of composition, let and ; we must show for each . To this end, note that the term satisfies
whence, by Lemma 4.6(iii), as desired.
So we have a theory morphism , whose components are injective by Lemma 4.6(i). It remains to show they are also surjective. To this end, let be a distribution. By assumption, is an injection onto some . So let be the injective function sending to , let be the canonical realiser of , and define to be . It is now clear that for all , and that for all . Thus as desired. ∎
We now make the correspondences between non-degenerate Grothendieck Boolean algebras, varieties of -sets, and non-degenerate hyperaffine algebraic theories—and their finitary variants—into functorial equivalences. Let us write:
-
•
(resp., ) for the category of non-degenerate Boolean (resp., Grothendieck Boolean) algebras and their homomorphisms.
-
•
(resp., ) for the full subcategory of on the non-degenerate hyperaffine (resp., finitary hyperaffine) algebraic theories.
-
•
(resp., ) for the full subcategory of on the varieties isomorphic to some (resp. ).
The assignments and can now be made functorial. A homomorphism of non-degenerate Grothendieck Boolean algebras induces, on the one hand, a concrete functor , where assigns to a -set structure on the -set structure with ; and on the other hand, a theory homomorphism with components
(4.4) |
In this way, we obtain functors and as in the statement of:
Theorem 4.9.
We have a triangle of equivalences, commuting to within natural isomorphism, as to the left in:
(4.5) |
which restricts back to a triangle of equivalences as to the right.
Proof.
By Propositions 3.16 and 4.2, the equivalence restricts to one and further back to one . Again because of Proposition 3.16, the triangles commute to within isomorphism. So to complete the proof, it suffices to show that is an equivalence both to the left and the right. We already know by Proposition 4.2 that in both cases it is essentially surjective, so we just need to check it is also full and faithful.
As in the proof of Proposition 3.16, given we write for the element with and , and given we write for the element given by the inclusion . Note that every element of is of the form for a unique ; so given a theory homomorphism there is a unique map such that for each . Since , and in , and preserves these identities, this is a Boolean homomorphism. Moreover, for each and , we have , and so , so that . In particular, must be a homomorphism of Grothendieck Boolean algebras: for indeed, if , then . Moreover, we have that ; now if also , then for all and so . So is full and faithful as claimed, and this completes the proof. ∎
5. Hyperaffine–unary theories
In this section, we prove our first main result, which gives a syntactic characterisation of the algebraic theories which correspond to cartesian closed varieties. This simplifies an existing characterisation due to Johnstone in [10]; as such, we begin by recalling Johnstone’s result, and then use it to deduce ours.
Notation 5.1 (Placed equality, dependency; [10]).
Let be an algebraic theory, let and let . Given , we write (read as “ and are equal in the th place of ”) as an abbreviation for the assertion that
We say that does not depend on if .
Theorem 5.2 ([10]).
A non-degenerate algebraic theory presents a cartesian closed variety if, and only if, the following two conditions hold:
-
(i)
For every , there exist , families , and a function such that
(5.1) -
(ii)
For any , and , if does not depend on , then does not depend on any .
Our improved characterisation says that presents a cartesian closed variety if, and only if, each operation decomposes uniquely into hyperaffine and unary parts.
Definition 5.3 (Hyperaffine–unary decomposition, hyperaffine–unary theory).
Let be an algebraic theory. Given a hyperaffine and a unary , we write for the operation . A hyperaffine–unary decomposition of is a choice of and as above such that . We say that the theory is hyperaffine–unary if every operation admits a unique hyperaffine–unary decomposition.
The crucial lemma which will enable us to prove this is:
Lemma 5.4.
If the algebraic theory satisfies condition (i) of Theorem 5.2, then any affine operation of is hyperaffine.
Proof.
Let be affine, and let be as in Theorem 5.2(i). Note first that, since is affine, on substituting for each in the right-hand equation of (5.1), we have that for all . To show is hyperaffine, it suffices, by the left equation of (5.1), to prove that for all . But we calculate that
using the right equation of (5.1) three times and the fact that once. ∎
Theorem 5.5.
An algebraic theory presents a cartesian closed variety if, and only if, it is hyperaffine–unary.
Proof.
Firstly, if is degenerate then it is both cartesian closed and hyperaffine, so a fortiori hyperaffine–unary. Thus, we may assume henceforth that is non-degenerate and so apply Johnstone’s characterisation theorem.
We first prove the only if direction. To begin with, we show that each has some hyperaffine–unary decomposition. To this end, let be as in Theorem 5.2(i). Let be given by . By the left condition of (5.1) is affine, and so it is hyperaffine by Lemma 5.4. Let be given by . We now calculate that
using in succession, the left equality in (5.1); the right equality twice; the definition of ; and the definition of .
We now show this decomposition of is unique. Suppose we have hyperaffine and with . As and are affine, we have . We must show also that . Note that , so that the right-hand side does not depend on whenever . Thus by Theorem 5.2(ii), we conclude that does not depend on for any . It follows that and so taking , we conclude that so that as desired.
We now prove the if direction. Supposing that every operation of has a unique hyperaffine–unary decomposition, we prove (i) and (ii) of Theorem 5.2. For (i), given with decomposition , we take , , and to obtain the required data satisfying (5.1). It remains to verify condition (ii). So let , and be such that given by does not depend on . Writing , we have
where we define and . Now consider the hyperaffine operations with
Because does not depend on , the operations and are equal. By unicity of decompositions, we have in , so that does not depend on . We claim it follows that does not depend on for any . For indeed, we have that in , since does not depend on . Since, by hyperaffineness of , we have for each , we conclude that, for any , we have so that does not depend on . ∎
The proof of Theorem 5.5 just given provides an intellectually honest account of the genesis of the ideas in this paper; but for good measure, we will also give a direct proof of the theorem which does not rely on [10]. For now we only show that every cartesian closed variety is hyperaffine–unary; we will close the loop in Section 7 once we have a better handle on what hyperaffine–unary theories are.
It will in fact be clearer if we prove something more general. Recall that the copower of some by a set is a coproduct of copies of . We write for the coproduct coprojections, and given maps , write for the unique map with for each .
Definition 5.6 (Complete theory of dual operations).
Let be a category with all set-indexed copowers and let . The complete theory of dual operations of is the algebraic theory with:
-
•
;
-
•
Projection elements ;
-
•
Substitution given by
To a universal algebraist, this is the (infinitary) clone of co-operations of [2]; to a category theorist, it is the structure of the hom-functor [11]. The following standard result is now [11, Theorem III.2]:
Proposition 5.7.
Let be a category with set-indexed copowers and let . For any , the set is a model for with for each . For any , the function is a -homomorphism, and so we induce a factorisation
(5.2) |
which is universal among factorisations of through a variety.
When, in the above proposition, we take itself to be a variety , and take , the free model on one generator, it is visibly the case that and that is an isomorphism. Thus, the fact that any cartesian closed variety is hyperaffine–unary follows from:
Proposition 5.8.
Let be a category with finite products and set-indexed copowers, and suppose that each preserves copowers; in particular, this will be so if is cartesian closed. For any , the complete theory of dual operations is hyperaffine–unary.
Proof.
Since preserves copowers, we may realise the copower as the product via the coprojection maps
Thus, we may write operations in as pairs where and . From the definition of substitution in , such an operation is affine just when
i.e., just when . We claim that any such is in fact hyperaffine. This follows from commutativity in:
whose uppermost composite is the interpretation of and whose lower composite interprets ; here is the canonical isomorphism characterised by .
So the hyperaffine operations of are those of the form ; and, of course, the unary operations are those of the form . Moreover, if is hyperaffine and is unary, then the operation is interpreted by the composite
So each operation has a unique hyperaffine–unary decomposition into the hyperaffine and the unary , as desired. ∎
6. Matched pairs of theories
As the name suggests, a hyperaffine–unary theory has a hyperaffine part and a unary part. In this section, we show that these two parts, together with their actions on each other, provide an entirely equivalent description of the notion of hyperaffine–unary theory. To begin with, let us record how we extract out the two parts of a hyperaffine–unary theory.
Proposition 6.1.
Let be a hyperaffine–unary theory. The hyperaffine operations of form a subtheory , called the hyperaffine part; while forms a monoid under substitution, called the unary part.
Proof.
The only non-trivial point is that hyperaffine operations are closed under substitution. But every affine operation is hyperaffine by Lemma 5.4, and the affine operations in any theory are easily closed under substitution. ∎
Clearly, if we know and then we know every operation of . However, the monoid structure of and the substitution structure of do not determine the substitution structure of . For this, we also need to record how and act on each other via substitution in .
Proposition 6.2.
Let be a hyperaffine–unary theory with hyperaffine and unary parts and . We may determine operations
as follows: if and , then is unique such that
(6.1) |
while if and , then is unique such that
(6.2) |
These operations uniquely determine the substitution structure of via the formulae:
-
•
in , where is the identity element of ;
-
•
If and (i.e., for each ), then
(6.3)
Proof.
For the unique existence of , the composite operation admits a unique hyperaffine–unary decomposition; but since , the unary part of this must be . The corresponding hyperaffine part is thus the unique operation making (6.1) hold. The unique existence of is trivial: take it as the substitution in , and then (6.2) follows from associativity of substitution. It remains to prove that these operations determine the projections and substitutions for . That is trivial; as for (6.3), we calculate that:
definition of | |||||
definition of | |||||
hyperaffineness of | |||||
commutativity in | |||||
associativity in | |||||
definition of . |
∎
So any hyperaffine–unary algebraic theory is determined by its hyperaffine and unary parts, together with the operations of (6.1) and (6.2). However, if given a hyperaffine theory and a monoid , together with operations of the same form, we should not expect to obtain a structure of hyperaffine–unary theory on the sets : for although the preceding proposition indicates how to define substitution from these operations, it does not ensure that the axioms of a theory are satisfied. For this, we must impose axioms on the operations relating and .
Definition 6.3 (Matched pairs of theories).
A matched pair of theories comprises a hyperaffine theory and a monoid together with operations:
(6.4) | ||||||
satisfying the following axioms:
-
(i)
For , the maps give a homomorphism of algebraic theories :
(6.5) (6.6) -
(ii)
The maps in (i) constitute an -action on :
(6.7) (6.8) -
(iii)
The operations make into a -model :
(6.9) (6.10) -
(iv)
Right multiplication by is a -model homomorphism :
(6.11) -
(v)
Left multiplication by is a -model homomorphism , where is the -model obtained by pulling back along the theory homomorphism :
(6.12) -
(vi)
For , the map is a -model homomorphism , where is the free -model structure on :
(6.13)
We call a matched pair of theories finitary or non-degenerate when is so.
A homomorphism of matched pairs of theories is a homomorphism of theories and a monoid homomorphism such that for all , and , we have:
(6.14) |
We now show soundness and completeness of this axiomatisation.
Proposition 6.4.
If is a hyperaffine–unary theory, then its hyperaffine and unary parts and constitute a matched pair of theories under the operations of Proposition 6.2; and is finitary or non-degenerate just when is so.
Proof.
For (6.5)–(6.8), we calculate using (6.1) and the theory axioms of and conclude using unicity of hyperaffine–unary decompositions. For (6.5), the calculation is . For (6.6):
For (6.7), we have , and for (6.8),
Next, (6.9) and (6.10) follow directly from the theory axioms for . Finally, for (6.11)–(6.13), we calculate using (6.1) and (6.2) and conclude using unicity of decompositions. For (6.11) the calculation is that . For (6.12) we have:
and finally, for (6.13) we have:
Proposition 6.5.
For any matched pair of theories , there is a hyperaffine–unary theory , the bicrossed product of and , with .
Proof.
For each set , we take , and write a typical element like before as . We define projection elements and substitution operations by the formula (6.3), and claim that, upon doing so, we obtain an algebraic theory . For this, we must check the three theory axioms. Firstly:
by the definition, axiom (6.5), and axiom (6.10). Secondly,
by the definition, axiom (6.9) and axiom (6.7). Finally, for associativity of substitution, we first compute that is given by
while is given by
Comparing first terms we have:
associativity in | |||
(6.13) | |||
commutativity in | |||
hyperaffinness | |||
(6.8) | |||
(6.6) |
while comparing second terms, we have
(6.11) | |||
(6.10) | |||
commutativity in | |||
hyperaffineness | |||
(6.12) |
as desired. So is an algebraic theory.
We next characterise the unary and hyperaffine operations of . Clearly the unary operations are those of the form . As for the hyperaffines, note that will be hyperaffine when , i.e., when . In particular, we must have ; and such an element will be hyperaffine just when also , i.e., . Since each is hyperaffine, we conclude that the hyperaffines in are all elements of the form . It follows from this characterisation that each has the unique hyperaffine–unary decomposition , whence it follows that is a hyperaffine–unary theory.
It remains to show that . Writing and for the hyperaffine and unary parts of , we have isomorphisms and given by and . Because and in , the maps constitute an isomorphism of theories ; and because and in , the map is a monoid isomorphism .
We now verify the two axioms in (6.14). For the first, observe that the operation on has given by the unique element for which . But and , whence , i.e., as required. For the second axiom in (6.14), note that the operation on is given by , which says that as required.
Finally, it is trivial to observe that is finitary or non-degenerate if and only if is so, i.e., if and only if is so. ∎
So we have a correspondence between hyperaffine–unary theories and matched pairs of theories; we now describe how this correspondence interacts with semantics.
Definition 6.6 (Models of matched pairs of theories).
Let be a matched pair of theories. A -model is a set endowed with both -model structure and -set structure in such a way that
(6.15) |
for all , , and ; while a homomorphism of -models is a function preserving both -model and -set structure. We write for the variety of -models.
Proposition 6.7.
Let be a hyperaffine–unary theory with . The variety of -models is concretely isomorphic to the variety of -models.
Proof.
Firstly, restricting back a -model structure on a set to the hyperaffine and unary parts yields -model and -set structure which satisfy the axioms in (6.15) due to the definitions of the operations and in . Conversely, -model and -set structure on yields -model structure with
(6.16) |
The projection axioms hold as every projection is in . As for substitution:
definition | |||
(6.15) | |||
hyperaffinness | |||
commutativity | |||
(6.15) | |||
-model axiom | |||
definition | |||
(6.3). |
It is easy to see that these assignments are mutually inverse; and in light of (6.16), the homomorphisms match up under the correspondence. ∎
To conclude this section, we make the correspondence between hyperaffine–unary theories and matched pairs of theories functorial. We write:
-
•
(resp., ) for the category of non-degenerate matched pairs (resp., finitary matched pairs) of theories and their homomorphisms;
-
•
(resp., ) for the full subcategory of on the non-degenerate hyperaffine–unary (resp. finitary hyperaffine–unary) theories;
-
•
(resp., ) for the full subcategory of on the non-degenerate cartesian closed (resp., cartesian closed finitary) varieties.
Now the assignment can be made functorial. Indeed, given a homomorphism of non-degenerate matched pairs of theories, we have a concrete functor which acts by and on the -model and -set structures. In this way, we obtain a functor which, in light of Proposition 6.7, the final clause of Proposition 6.4, and Theorem 5.5, must land inside .
The assignment of Proposition 6.4 can also be made functorial:
Proposition 6.8.
The assignment is the action on objects of a functor , which on morphisms takes to the homomorphism .
Proof.
is clearly functorial so long as it is well-defined on morphisms. To show this, let be a homomorphism between hyperaffine–unary theories. Clearly, preserves both hyperaffine operations and unary operations, and so restricts back to and . We must verify that these restrictions satisfy the axioms in (6.14). The second axiom is simply an instance of the homomorphism axiom for ; as for the first, we have:
whence by unicity of decompositions. ∎
Given the above, we are now ready to state the main result of this section:
Theorem 6.9.
We have a triangle of equivalences, commuting to within natural isomorphism, as to the left in:
which restricts back to a triangle of equivalences as to the right.
Proof.
The triangles commute to within isomorphism by Proposition 6.7, and by Theorem 5.5, their left edges are equivalences. So to complete the proof it suffices to show that is an equivalence to the left and the right. We know that in both cases it is essentially surjective by Proposition 6.5, and so it remains only to show it is also full and faithful. For fidelity, note that any homomorphism must, by unicity of decompositions, send to , and so is determined by its hyperaffine and unary restrictions. For fullness, let and let . We must show that the functions
preserve projections and substitution. For projections, we have , while for substitution, we have:
7. Matched algebras and -sets
In this section we use Theorem 4.9 to recast the notion of matched pair of theories in terms of what we will call a matched pair of algebras. This yields a reformulation of Theorem 6.9 giving a functorial equivalence between (non-degenerate) hyperaffine–unary theories, matched pairs of algebras, and cartesian closed varieties. We begin in the finitary case, where a matched pair involves a Boolean algebra and a monoid which act on each in a suitable way—a structure which was already considered in [6, §4], in a related, though different, context.
Definition 7.1 (Matched pair of algebras).
A non-degenerate matched pair of algebras comprises a non-degenerate Boolean algebra , a monoid and:
-
•
-set structure on , which we write as ;
-
•
-set structure on , which we write as ;
such that acts on by Boolean homomorphisms, and such that:
-
•
;
-
•
; and
-
•
,
for all and . Here, in the final axiom, we recall from Remark 3.17 that itself is a -set under the operation of conditioned disjunction . These axioms are equivalently the conditions that:
-
•
;
-
•
;
-
•
, i.e., .
A homomorphism of matched pairs of algebras comprises a Boolean homomorphism and a monoid homomorphism such that, for all and we have:
(7.1) |
or equivalently, such that
(7.2) |
We write for the category of non-degenerate matched pairs of algebras.
We now establish the desired equivalence between finitary matched pairs of theories, and matched pairs of algebras.
Proposition 7.2.
The assignment sending a non-degenerate finitary hyperaffine theory to the Boolean algebra of Proposition 4.4 induces an equivalence of categories .
Proof.
The assignment is, by Theorem 4.9, the action on objects of an equivalence . Under this equivalence, the data and axioms of a matched pair of theories as in Definition 6.3 transform as follows:
-
•
and correspond to the Boolean algebra and monoid ;
-
•
The maps to the left of (6.4), satisfying the bicrossed pair axioms (i) and (ii), correspond to a monoid action of on by Boolean homomorphisms;
-
•
The maps to the right of (6.4), satisfying the axiom (iii), correspond to a -set structure on ;
-
•
The axioms (iv) and (v) correspond directly to the first two axioms for a matched pair of algebras.
As for axiom (vi), we claim that this corresponds to the final axiom for a matched pair of algebras. This is not completely immediate: we must first observe that (vi) can be replaced by the apparently weaker special case which takes :
-
(vi)′
For , the map is an -model map .
To see that this special case implies the general one, we must show that for any , and we have: . By Lemma 4.6(i), it suffices to verify for each the equality of the binary reducts of each side. Since the operations and are theory homomorphisms , we have
and since the are binary, these terms are equal by the special case (vi)′. Observing that the -model structure on corresponds to the -action on by conditioned disjunction, we thus conclude that (vi)′, and hence also (vi), are equivalent to the final axiom for a matched pair of theories.
It remains to show that homomorphisms match up under the above correspondences: for which we must show that the two conditions of (6.14) correspond to the two conditions of (7.1). For the first condition in (6.14), this is achieved by exploiting Lemma 4.6(i) like before to reduce to then case . As for the second condition, we may re-express it as saying that is a homomorphism of -models , from which the correspondence with (7.1) is immediate. ∎
So each finitary matched pair of theories has a more concrete expression as a matched pair of algebras ; we now show that, correspondingly, the variety of -models has a more concrete expression as a variety of -sets:
Definition 7.3 (Variety of -sets).
Let be a non-degenerate matched pair of algebras. A -set is a set endowed with -set structure and -set structure, such that in addition we have:
(7.3) |
for all , and ; or equivalently, such that:
(7.4) |
A homomorphism of -sets is a function which is at once a -set and an -set homomorphism. We write for the variety of -sets.
We noted in the preceding sections that any non-degenerate Boolean algebra is always a -set over itself, and that any monoid is always an -set over itself. If is a matched pair, then by definition we also have that is an -set, and is a -set; it should therefore be no surprise that, when endowed with these actions, both and become -sets. In fact, is the free -set on one generator; while is the coproduct of two copies of the terminal -set.
Proposition 7.4.
The equivalence of Proposition 7.2 fits into a triangle of equivalences, commuting to within natural isomorphism:
Proof.
Given a matched pair of theories with associated matched pair of algebras , we know by Theorem 4.9 that the data of an -model structure on , as in Definition 6.6, will transform as follows:
-
•
The -model and -set structure on correspond to a -set structure and an -set structure;
- •
- •
It is clear that the homomorphisms match up under this correspondence, and so the variety of -models and the variety of -sets are concretely isomorphic. It is easy to check that these isomorphisms are natural in as required. ∎
Now extending the preceding arguments to the non-finitary case is straightforward. First we generalise the notion of matched pair of algebras.
Definition 7.5.
A non-degenerate Grothendieck matched pair of algebras comprises a non-degenerate matched pair of algebras and a zero-dimensional topology on , such that:
-
•
The -set is a -set;
-
•
The -action on is by Grothendieck Boolean homomorphisms .
A homomorphism of Grothendieck matched pairs of algebras is a homomorphism of matched pairs of algebras for which is a Grothendieck Boolean homomorphism. We write for the category of non-degenerate Grothendieck matched pairs of algebras.
We next generalise the correspondence between finitary hyperaffine theories and matched pairs of algebras; the proof of this result is mutatis mutandis the same as Proposition 7.2.
Proposition 7.6.
The assignment sending a non-degenerate hyperaffine theory to the Grothendieck Boolean algebra of Proposition 4.7 induces an equivalence of categories . ∎
Finally, we introduce the varieties associated to Grothendieck matched pairs of algebras , and show that they match up with the models of the corresponding matched pairs of theories.
Definition 7.7 (Variety of -sets).
Let be a non-degenerate Grothendieck matched pair of algebras. A -set is a -set whose underlying -set is in fact a -set; a homomorphism of -sets is just a homomorphism of -sets. We write for the variety of -sets.
Like before, both and are -sets via their canonical actions on themselves and each other.
Proposition 7.8.
The equivalence of Proposition 7.6 fits into a triangle of equivalences, commuting to within natural isomorphism:
∎ |
Remark 7.9.
We can extract from the above development a description of the free -set on a set as given by the product of -sets . Here, is seen as a -set via its canonical structures of - and -set, while is seen as a -set as in Remark 3.17 and as an -set via the action . The function exhibiting as free on is given by .
Combining Propositions 7.6 and 7.8 with Theorem 6.9, we obtain the main theorem of this section, relating (non-degenerate) Grothendieck matched pairs, hyperaffine–unary theories and cartesian closed varieties.
Theorem 7.10.
We have a triangle of equivalences, commuting to within natural isomorphism, as to the left in:
which restricts back to a triangle of equivalences as to the right.
Another way to say this is that every non-degenerate cartesian closed variety is a variety of -sets for some Grothendieck matched pair of algebras . We now make explicit the cartesian closed structure of .
Proposition 7.11.
The variety of -sets is cartesian closed. In particular, the variety of -sets is cartesian closed.
Proof.
Given -sets and , we define the function space to be the set of -set homomorphisms . We make this into an -set under the same action as in Proposition 2.4:
We must check is a -set homomorphism if is one. For the -set aspect this is just as in Proposition 2.4; for the -set aspect, if and then and so , i.e., as desired. We now make into a -set via the equivalence relations:
Axiom (i) of Proposition 3.2 is straightforward, given that each is a Grothendieck Boolean homomorphism; so it now suffices to check axiom (ii)′ of Proposition 3.11. Thus, given a partition and homomorphisms for each , we must show there is a unique with for all , i.e.,
(7.5) |
As is a Grothendieck Boolean homomorphism, the set is in , and so for each there is a unique element satisfying (7.5). It remains to show that the so defined is a -set homomorphism.
To see preserves the -set structure, suppose that in and in ; we must show in . Since we have for each that , and so , using that and and . Thus, for all we have and so by Lemma 3.12(i) that as required. To see preserves the -set structure, we must show . But for each we have , and so . Thus by Lemma 3.12(i).
So is a well-defined -set. We now define the evaluation homomorphism as in Proposition 2.4 by . This preserves -set structure as there; while for the -set structure, if in and in , then as desired.
Finally, given a -set homomorphism , its transpose is given by . As in Proposition 2.4, this is an -set homomorphism, and is the unique such with for all . It remains to show that preserves -set structure. But if , then for all , and so for all , i.e., . ∎
Note that the results of the preceding sections have shown, without reference to [10], that every non-degenerate hyperaffine–unary theory is a theory of -sets. Since every degenerate hyperaffine–unary theory clearly presents a cartesian closed variety, the preceding result thus completes a proof of the “if” direction of Theorem 5.5 that does not rely on [10]. Taken together with Proposition 5.8, we thus obtain our desired independent proof of Theorem 5.5.
As mentioned in the introduction, we defer substantive examples of varieties of -sets to the companion paper [5], where we establish links with topics in operator algebra. However, Proposition 5.8 assures us that there is a plentiful supply of such varieties: we have one for any object of a category with finite products and distributive set-indexed copowers. We can now be more explicit about the associated to such an .
Proposition 7.12.
Let be a category with finite products and set-based copowers for which each functor preserves copowers, and let .
-
(a)
The set is a monoid with unit under the operation of composition in diagrammatic order, i.e.:
-
(b)
Writing for the first and second copower coprojections, the set is a Boolean algebra under the operations
where satisfies for ;
-
(c)
There is a zero-dimensional coverage on in which is in just when there exists a map with for all , where here is given by when and otherwise;
-
(d)
acts on via precomposition;
-
(e)
acts on via:
So long as is non-degenerate, the above operations make into a non-degenerate Grothendieck matched pair of algebras. Moreover, for all , the set becomes a -set, where acts on via precomposition, and acts on via
In this manner, we obtain a factorisation of the hom-functor as
(7.6) |
which is universal among factorisations of through a variety. In particular, if is a non-degenerate cartesian closed variety and is the free model on one generator, then is an isomorphism.
Proof.
By Proposition 5.8, the complete theory of dual operations of is hyperaffine–unary. If is degenerate, then so is the Boolean algebra described above, and there is nothing to do; otherwise, we know that the non-degenerate hyperaffine–unary corresponds to a Grothendieck matched pair for which is concretely isomorphic to . Using that the hyperaffine operations of are, as in the proof of Proposition 5.8, those of the form , and following through the construction of from the hyperaffine–unary theory as in Sections 6 and 7, yields the description above. Finally, the factorisation (7.6) is simply the factorisation (5.2) after transporting across the isomorphism . ∎
We encourage the reader to apply this result in any category satisfying its rather mild hypotheses. For example, when is the category of topological spaces, the monoid associated to a space comprises all continuous endomorphisms of , while the Grothendieck Boolean algebra comprises all clopen subsets of , with the infinite partitions in being all infinite clopen partitions of . Now acts on by inverse image, , while acts on by restriction and glueing: . In this example, is rather large, in much the same way that full automorphism groups of objects tend to be rather large, and a key aspect of [5] will be to apply this result in carefully chosen situations where comes out as something combinatorially tractable and of independent interest.
References
- [1] Bergman, G. M. Actions of Boolean rings on sets. Algebra Universalis 28 (1991), 153–187.
- [2] Csákány, B. Completeness in coalgebras. Acta Sci. Math. (Szeged) 48, 1-4 (1985), 75–84.
- [3] Dicker, R. M. A set of independent axioms for Boolean algebra. Proc. London Math. Soc. 13 (1963), 20–30.
- [4] Fourman, M. P., and Scott, D. S. Sheaves and logic. In Applications of sheaves (1979), vol. 753 of Lecture Notes in Mathematics, Springer, pp. 302–401.
- [5] Garner, R. Cartesian closed varieties II: links to operator algebra. Preprint, available as arXiv:2302.04403, 2023.
- [6] Jackson, M., and Stokes, T. Semigroups with if-then-else and halting programs. International Journal of Algebra and Computation 19 (2009), 937–961.
- [7] Johnstone, P. Cartesian monads on toposes. J. Pure Appl. Algebra 116 (1997), 199–220.
- [8] Johnstone, P. T. Stone spaces, vol. 3 of Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1982.
- [9] Johnstone, P. T. When is a variety a topos? Algebra Universalis 21 (1985), 198–212.
- [10] Johnstone, P. T. Collapsed toposes and Cartesian closed varieties. J. Algebra 129 (1990), 446–480.
- [11] Lawvere, F. W. Functorial semantics of algebraic theories. PhD thesis, Columbia University, 1963.
- [12] McKenzie, R. N., McNulty, G. F., and Taylor, W. F. Algebras, lattices, varieties. Vol. I. The Wadsworth & Brooks/Cole Mathematics Series. Wadsworth & Brooks/Cole, 1987.
- [13] Pattinson, D., and Schröder, L. Sound and complete equational reasoning over comodels. In 31st Conference on Mathematical Foundations of Programming Semantics (MFPS XXXI), vol. 319 of Electronic Notes in Theoretical Computer Science. Elsevier, 2015, pp. 315–331.
- [14] Van Name, J. Boolean Partition Algebras. PhD thesis, University of South Florida, 2013.
- [15] Van Name, J. Ultraparacompactness and ultranormality. Preprint, available as arXiv:1306.6086, 2013.