We begin with the way in which powersets are defined in topos theory, i.e. using the subobject classifier (Section 11) and exponentials, but expressed in a slightly more flexible way. We may arrive at the same definitions from type-theoretic considerations [Tay99, §9.5]. But, whereas the uniqueness of the characteristic map φ is a moot point in that discipline, it is essential to this paper.
The subobject classifier was originally defined by Bill Lawvere in 1969, and the basic theory of elementary toposes was developed in collaboration with Myles Tierney during the following year [Law71, Law00]. Giuseppe Rosolini generalised the definition to classes of supports [Ros86] and developed a theory of partial maps, but the Frobenius law (Propositions 3.11, 8.2 and 10.13) is also required for relational algebra.
Definition 2.1
A class M of morphisms (written ↪) of any category C, such that
is called a class of supports or a dominion.
Definition 2.2 An M-map ⊤:1→Σ
is called a support classifier or a dominance (for M)
if for every M-map i:U↪ X
there is a unique characteristic map φ:X→Σ
making the square a pullback:
Set-theoretically, U is obtained from φ as {x:X ∣ φ[x]} by the axiom of comprehension (separation or subset-selection), though we shall find the abbreviation [φ]↪ X convenient here. Because of the topological intuition we call i:U↪ X (the inclusion of) an open subset. (We shall write
for closed subsets and ↣ for Σ-split ones.)
Notice that this pullback is also an equaliser
The relationship between the axiom of comprehension and the monadic ideas of this paper is explored in Section B 8, which also sets out the λ-calculus that we need in a more explicitly symbolic fashion.
Remark 2.3
This classification property deals only with
a single subobject of (or predicate on) X,
but in practice we need to consider Γ-indexed families of subobjects,
or predicates containing parameters z
whose types form the context Γ.
These may equivalently be seen as binary relations Γ↽⇀ X
or as subobjects of Γ× X,
which are classified by maps Γ× X→Σ.
We would like these to be given by maps from Γ,
i.e. by generalised elements of the internal object of
maps X→Σ.
Hence we want to use the exponential ΣX.
In Set, this is the same as the powerset ℘(X).
To summarise, there is a correspondence amongst
| i |
| :U |
| ↪ X, φ |
| [x], φ:Γ× X→Σ and ∼ φ: Γ→ΣX≡℘(X) |
where ∼ φ(z ) is the subset Uz for (z )∈Γ.
Remark 2.4
We do not intend C to be cartesian closed,
because this does not follow from our axioms
and we want to use the category of locally compact spaces as an example.
Recall that to say that the exponential YX exists in a category C
(as a property of these objects individually)
means that the functor C(− × X,Y):Cop→Set
is representable,
i.e. it is naturally isomorphic to C(−,Z) for some object Z,
which we rename Z≡ YX.
For this to be meaningful,
all binary products Γ× X must first exist in C.
Notice that we ask for exponentials of the form YX for all X and fixed Y, whereas the word exponentiability refers to a property of a particular object X for arbitrary Y. Peter Freyd [FS90] has used the word baseable for the property that we require of Σ, but recognising the meaning of that word out of context depends on already knowing its association with exponents, whereas exponentiating suggests its own meaning more readily. (The word exponent seems to have come from the French exposant [Bar88].)
Remark 2.5
We shall make use of the λ-calculus to define morphisms to and from
exponentials such as these.
However, since we are only assuming the existence of ΣX,
and not cartesian closure,
the body of any λ-expression that we use
must be of type Σ,
or some other provably exponentiating object, such as a retract of ΣY.
The range, i.e. the type of the bound variable, is arbitrary
(cf. Definition 7.7).
[The restricted λ-calculus that we require, i.e. with just ΣY instead of general exponentials, is sketched in Section A 2.]
We leave it to the reader, making use of some account of λ-calculus and cartesian closed categories such as [Tay99, §4.7], to rewrite juxtapositions like φ(f y) categorically in terms of evaluation (ev:ΣX× X→Σ), and λ-abstractions as adjoint transpositions. When we write x∈ X, φ∈ΣX etc., we mean generalised elements, i.e. C-morphisms x:Γ→ X and φ:Γ→ΣX, or expressions of type X or ΣX involving parameters whose types form an unspecified context Γ; to make Γ explicit in our categorical expressions often involves forming products of various objects with Γ. On the other hand, when we write f:X→ Y, it is sufficient for our purposes to regard this as a particular C-morphism, i.e. a global element of its hom-set, though in most cases parametrisation is possible by reading f as a morphism Γ× X→ Y. At first we need to make the parametrising object explicit (calling it X), as we are considering a new logical principle, but from Section 6 it will slip into the background.
Symbolically, our λ-calculus is peculiar only in that there is a restriction on the applicability of the (→)-formation rule; such a calculus has been set out by Henk Barendregt [Bar92, §5.2], although this is vastly more complicated than we actually need here. We shall instead adopt a much simpler notational convention: lower case Greek letters, capital italics, Σ(−)≡(−)* and the logical connectives and quantifiers denote terms of exponentiating type (predicates), whilst lower case italics denote terms of non-exponentiating type (individuals and functions). The capital italics could be thought of as “generalised quantifiers”.
The objects, unlike the morphisms, are never parametric in this paper (except in Proposition 5.4).
[We also refer to an equation between λ-terms as a statement.]
Remark 2.6 As exponentials are defined by a universal property,
the assignment X↦ΣX extends to a contravariant endofunctor,
Σ(−):C→Cop. It takes f:Y→ X to
| Σf:ΣX→ΣY by Σf(φ) ≡ φ∘ f ≡ f;φ ≡ λ y.φ(f y). |
The effect of Σf is to form the pullback or inverse image along f:
Remark 2.7
Returning to the powerset, we write SubM(X) for
the collection of isomorphism classes of M-maps into X∈obC.
Then Definition 2.2 says that the contravariant functor
SubM:Cop→Set is representable, i.e. that it is naturally isomorphic
to C(− ,Σ) for some object Σ.
As a special case of the conditions on M,
the pullback (intersection) of any two M-maps into X exists,
and the composite across the pullback square is in M,
so SubM(X) is a semilattice.
In fact, SubM(−) is a presheaf of semilattices
on the category C,
so C(− ,Σ) is an internal semilattice in the topos of presheaves
[Fre66a].
Since the Yoneda embedding is full and faithful and preserves products,
Σ was already an internal semilattice in C.
It is well known that this argument makes unnecessary use of the category of sets, which it is the whole point of this paper to avoid (there are also size conditions on C), although we may suppose instead that C is an internal category in some pretopos. However, it is not difficult to disentangle this result from the sheaf theory and prove it directly instead. (The details of this proof would be a useful exercise in diagram-chasing for new students of category theory.)
Proposition 2.8
Any dominance Σ carries a ∧-semilattice structure,
and pullback along {⊤}↪Σ induces an
external semilattice isomorphism [ ]:C(X,Σ)→SubM(X).
Moreover, each ΣX is an internal ∧-semilattice
and each Σf is a semilattice homomorphism.
(We shall consider the existence and preservation of joins
in Section 9.)
Proof The fifth diagram defines ∧ as sequential and in terms of composition in M; manipulation of the pullbacks in the sixth establishes the relationship with intersection. By construing the monos {<⊤,⊤>}↪Σ×Σ and {<⊤,⊤,⊤>}↪Σ×Σ×Σ as pullbacks in various ways, the semilattice laws follow from the uniqueness of their characteristic maps. These laws are expressed by the four commutative diagrams above involving products, i.e. Σ is an internal semilattice. Moreover, ΣX is also an internal semilattice because the functor (−)X (that is defined for powers of Σ and all maps between them) preserves products and these commutative diagrams. Similarly, Σf is a homomorphism because (−)f is a natural transformation. ▫
Remark 2.9
In the next section we give a new characterisation of support classifiers
as semilattices satisfying a further equation (the Euclidean principle),
rather than by means of a class of supports.
This characterisation depends on another hypothesis, that the adjunction
| Σ(−)⊣Σ(−) |
(which is defined for any exponentiating object Σ) be monadic. The way in which this hypothesis is an abstract form of Stone duality is explored in Examples B 1. In many cases the category C that first comes to mind does not have the monadic property, but [B] constructs the monadic completion ↝ C of any category C with an exponentiating object Σ. In fact ↝ C is the opposite of the category Alg of Eilenberg–Moore algebras for the monad.
Ultimately our interest is in developing some mathematics according to a new system of axioms, i.e. in the free model (Remark 3.8, Theorem 4.2), but first we introduce the concrete situations on which the intuitions are based. They and Example 4.5 also provide examples and counterexamples to gauge the force of the Euclidean and monadic principles. Even when C is not monadic, its properties are usually close enough to our requirements to throw light on the concepts, without shifting attention to the more complicated ↝ C.
[In fact most of the results of this paper can be developed in the similar but alternative framework of equideductive logic, without the monadic principle [DD].]
With excluded middle, all objects are overt, but (unlike Set) LKSp and LKLoc are not cartesian closed, complete or cocomplete. For LKLoc, the adjunction Σ(−)⊣Σ(−) is monadic (§O 5.10 and Theorem B 3.11), as it is for LKSp, assuming the axiom of choice.
It is by regarding (locally compact) frames as finitary algebras over the category of spaces (in which directed joins are “part of the wallpaper”), rather than as infinitary ones over the category of sets, that we achieve complete open–closed duality for the ideas discussed in this paper.
In any given category, there may be many classes M of supports, each class possibly being classified by some object ΣM.
Remark 2.13
Many of the ideas in this paper evolved from synthetic domain theory,
a model of which is a topos (with a classifier Ω for all monos)
that also has a classifier Σ for recursively enumerable subsets
[Ros86, Pho90a, Pho90b, Hyl91, Tay91, FR97, BR98]
.
In this case, Σ is a subsemilattice of Ω.
Such models exist wherein the full subcategory of replete objects satisfies
the monadicity property discussed in this paper for Σ
[Theorem I 15.10],
in addition to that for the whole category for Ω
[RT98].