1 Introduction
Positive model theory replaces the traditional use of full first-order logic with positive logic. This generalises classical model theory, because classical negation can be added back in through Morleyisation. Recently, deep model-theoretic ideas have been generalised to the positive context, with negligible concessions in the strength of the results (see, e.g., [Reference Ben-Yaacov1, Reference Ben-Yaacov and Poizat2, Reference Haykazyan9, Reference Kamsma14]). Meanwhile, in topos theory “positive logic” is known under the name of “coherent logic,” the finitary fragment of geometric logic. Geometric logic, and thus coherent logic, is known to behave extremely well in toposes, through the study of classifying toposes. With the aim of further cultivating this common ground, we initiate the topos-theoretic study of the protagonists of positive model theory: existentially closed models.
Existentially closed models (hereafter, e.c. models) are models of a theory where any (coherent) formula that can be solved in an extension can already be solved in that model itself. The archetypal examples are algebraically closed fields. Any polynomial that can be solved in a field extension of an algebraically closed field already admits a solution in the algebraically closed field itself. In fact, the algebraically closed fields are exactly the e.c. models of the theory of fields. In this case, the class of e.c. models is first-order axiomatisable, but this is not true in general. It is true, however, that the class of e.c. models can always be geometrically axiomatised (see Remark 3.8). This raises the natural question: what does the classifying topos of the e.c. models of a coherent theory look like? A consequence of the axiomatisation is a strong connection between this classifying topos and the notion of zero-dimensionality from topology.
Classically, there are two equivalent definitions of e.c. models (cf. Definition 3.4). One is in terms of the homomorphisms that have the model as a domain, requiring them to both preserve and reflect the satisfaction of coherent formulas, while the other asserts that whenever a coherent formula
$\varphi (x)$
does not hold for a tuple of elements a, then there is a coherent formula
$\psi (x)$
, satisfied by a, that implies
$\neg \psi (x)$
modulo the theory.
We generalise both notions to arbitrary toposes, keeping the name e.c. for the former, but naming the latter “strongly existentially closed” (or s.e.c.). The distinction is important, because in this generality they are no longer equivalent (Example 5.10). The previous appearance of e.c. models in the topos-theoretic literature, in [Reference Blass and Scĕdrov3], uses the latter definition. However, as we shall see, the former is much better behaved topos-theoretically.
1.1 Main results
We leave the precise statement of our main theorem (Theorem 7.1) until after the relevant terminology and notation has been introduced. When only considering coherent theories with models in
$\mathbf {Set}$
, a simplification is possible, yielding the following theorem.
Theorem 1.1. Let T be a coherent theory. Then the following are equivalent for a topos
$\mathcal {G} $
with enough points:
-
(i) $\mathcal {G} \simeq \mathbf {Set}[T^{\mathrm{ec}}]$
; -
(ii) $\mathcal {G}$
is locally zero-dimensional and entwined with
$\mathbf {Set}[T]$
; -
(iii) $\mathcal {G}$
is equivalent to the maximal s.e.c.-subtopos of
$\mathbf {Set}[T]$
with enough points.
We briefly explain some of the terms in the above statement.
-
(1) The theory $T^{\mathrm{ec}}$
is the common geometric theory of all the e.c. models of T in
$\mathbf {Set}$
, that is,
$\mathbf {Set}[T^{\mathrm{ec}}]$
is the classifying topos of the e.c. models of T. -
(2) A topos $\mathcal {G}$
is locally zero-dimensional if it has a generating set of objects whose subobject frames are zero-dimensional (Definition 6.5). -
(3) To say that $\mathcal {G}$
and
$\mathbf {Set}[T]$
are ‘entwined’ should be thought of as follows: there is a theory
$T'$
in an extension of the language of T such that
$G \simeq \mathbf {Set}[T']$
and for every model M of T, there is a model N of
$T'$
admitting a homomorphism
$M \to N$
, and vice versa. -
(4) Finally, $\mathcal {G}$
is an s.e.c.-subtopos of
$\mathbf {Set}[T]$
if the inverse image
$i^*(G_T)$
of the generic model
$G_T$
under the inclusion
$i: \mathcal {G} \hookrightarrow \mathbf {Set}[T]$
is internally s.e.c.
Along the way, we prove other important facts about our generalised notion of existential closedness. For model theory, it is important that every model admits a homomorphism into an e.c. model, which is a well-known fact for coherent theories in
$\mathbf {Set}$
. In Theorem 4.14, we show that the same is true for e.c. models of geometric theories in arbitrary toposes. Finally, based on existing work [Reference Blass and Scĕdrov3, Reference Caramello5], we apply our machinery to topos-theoretically characterise atomic e.c. models (Theorem 8.12) and countably categorical theories (Theorem 9.7) for coherent theories in
$\mathbf {Set}$
.
1.2 Overview
Sections 2 and 3 contain preliminary material. In Section 2, we establish some notation and recall basic facts about classifying toposes and coherent toposes. We recall the two classically equivalent definitions of e.c. models in Section 3, as well as their basic properties.
In Section 4, we generalise from e.c. models in
$\mathbf {Set}$
to e.c. geometric morphisms
$\mathcal {F} \to \mathcal {E}$
. We demonstrate that the property of being e.c. is well-behaved in that it is Morita invariant (Proposition 4.3). We also introduce the classifying topos
$\mathcal {E}_{\mathcal {F}\textrm {-ec}}$
of e.c. geometric morphisms, and the notion of two toposes
$\mathcal {E}$
and
$\mathcal {E}'$
being
$\mathcal {F}$
-entwined. We show that
$\mathcal {F}$
-entwinement is an equivalence relation on toposes and it is equivalent to having equivalent classifying toposes of e.c. morphisms
$\mathcal {E}_{\mathcal {F}\textrm {-ec}} \simeq \mathcal {E}^{\prime }_{\mathcal {F}\textrm {-ec}}$
(Proposition 4.13). The key ingredient for that last result is the aforementioned fact that, in any topos, any model admits a homomorphism into an e.c. model (Theorem 4.14).
For models of a coherent theory in
$\mathbf {Set}$
, the e.c. models and s.e.c. models coincide. In Section 5, we generalise s.e.c. models to arbitrary geometric morphisms
$\mathcal {F} \to \mathcal {E}$
. However, the notion of s.e.c. we introduce is heavily dependent on a particular choice of presentation for
$\mathcal {E}$
, encapsulated by a choice of a generating set
$\mathcal {X}$
and a basis of subobjects
$\mathcal {B}$
for
$\mathcal {X}$
(see Example 5.10). When
$\mathcal {E}$
is coherent, the notion becomes somewhat tamer in that there are canonical choices for
$\mathcal {X}$
and
$\mathcal {B}$
(Theorem 5.8).
In Section 6, we introduce the notion of a locally zero-dimensional topos. Our terminology is justified since a localic topos is locally zero-dimensional if and only if the corresponding locale is locally zero-dimensional (Proposition 6.7).
Section 7 combines the preceding content in our main result—a characterisation, under suitable hypotheses, of the classifying topos of e.c. models. These unspoken hypotheses are satisfied in the motivating case of a coherent theory and models in
$\mathbf {Set}$
. We also provide a class of examples where the hypotheses are satisfied in a topos other than
$\mathbf {Set}$
, namely the topos of “difference sets”
$\mathbf {Set}^{\mathbb {N}}$
(see Proposition 7.9 and Example 7.11).
Finally, in Sections 8 and 9, we relate our work to previous literature on similar topics [Reference Blass and Scĕdrov3, Reference Caramello5]. We give a topos-theoretic characterisation of the model-theoretic notion of an atomic e.c. model in Section 8, and of countably categoricity (in the positive model-theoretic sense) in Section 9. In addition, Section 8 also establishes connections between the property of being a dense subtopos and the various subtoposes that have been studied throughout the article.
2 Preliminaries and notation
2.1 Notation and conventions
We begin by setting out some conventions:
-
(1) Throughout, “topos” will mean a Grothendieck topos.
-
(2) We will often omit the arrow when referring to subobjects in a topos, instead writing $A \leq X$
to denote a subobject (i.e., an equivalence class of monomorphisms
$A \hookrightarrow X$
). Since it will be clear from context, when referring to the subobject lattice of an object, we will also omit the ambient topos, for example, writing
$\mathrm {Sub}(X)$
instead of
$\mathrm {Sub}_{\mathcal {E}}(X)$
. -
(3) When discussing logical formulas, we will follow the standard model-theoretic convention that single letters denote tuples, for example, x and y will denote (finite, potentially empty, and potentially of mixed sorts) tuples of variables, and if M is a model in $\mathbf {Set}$
, then
$a \in M$
refers to a tuple of elements.The interpretation of a logical formula $\varphi (x)$
in a model M will be written as
$\varphi (M)$
. If M is a model in
$\mathbf {Set}$
, then
$\varphi (M)$
is a subset of some product of sorts in M (corresponding to the sorts of x). If M is a model in an arbitrary topos
$\mathcal {F}$
,
$\varphi (M)$
is a subobject of a product of sorts. We will still write
$\varphi (M) \leq M$
regardless.
2.2 Classifying toposes
We now briefly recall the basics of classifying topos theory. Given a geometric theory T, a classifying topos
$\mathbf {Set}[T]$
for T is a topos for which there is a natural equivalence of categories
for any topos
$\mathcal {F}$
, where
$T \text {--} \mathbf {Mod}(\mathcal {F})$
denotes the category of models of T internal to
$\mathcal {F}$
and their homomorphisms, while
$\mathbf {Topos}(\mathcal {F},\mathbf {Set}[T])$
denotes the category of geometric morphisms
$\mathcal {F} \to \mathbf {Set}[T]$
and transformations between these (i.e., natural transformations between the inverse image parts, called geometric transformations in [Reference Johnstone12, Section A4.1]). Every geometric theory has a classifying topos, and every topos is the classifying topos for some geometric theory. The universal property satisfied by the classifying topos of T ensures that it is defined uniquely up to equivalence.
More explicitly, the classifying topos
$\mathbf {Set}[T]$
contains an internal model of T called the generic model
$G_T$
. The above correspondence is then given by sending a geometric morphism
$p: \mathcal {F} \to \mathbf {Set}[T]$
to the model
$p^*(G_T)$
of T in
$\mathcal {F}$
.
Fact 2.1. We note some important facts about the generic model:
-
(i) The interpretations of formulas in the generic model, that is, the objects $\varphi (G_T)$
, generate the topos
$\mathbf {Set}[T]$
. -
(ii) The subobjects in $\mathbf {Set}[T]$
of
$\varphi (G_T)$
are precisely the subobjects of the form
$\psi (G_T) \leq \varphi (G_T)$
[Reference Johnstone12, Lemma D1.4.4(iv)], where
$\psi $
is also a geometric formula, and moreover there is an inclusion of subobjects
$\psi (G_T) \leq \varphi (G_T)$
if and only if T proves the sequent
$\psi (x) \vdash _x \varphi (x)$
.
2.3 Coherent toposes
The assertion that every topos classifies some theory necessitates the consideration of geometric logic. To focus solely on coherent theories, we can restrict to coherent toposes. These are toposes that are, in a strong sense, determined by their compact objects. In this article, we will often restrict to the case of a coherent topos to simplify our conditions.
Definition 2.2 [Reference Johnstone12, Section D3.3].
-
(i) An object X in a topos is said to be compact if every jointly epimorphic family $\{Y_i \to X\}_{i \in I}$
admits a jointly epimorphic finite subfamily. -
(ii) An object X is coherent if, in addition to being compact, it is stable in the sense that for any pair of arrows $Y \to X \leftarrow Z$
with compact domains, their pullback
$Y \times _X Z$
is also compact. -
(iii) A topos is said to be coherent if it has a generating set of coherent objects.
Fact 2.3. We recall some facts about coherent toposes.
-
(i) A topos is coherent if and only if it is the classifying topos of a coherent theory [Reference Johnstone12, Theorem D3.3.1]. Indeed, if T is coherent, then the objects $\varphi ({G_{T}})$
, where
$\varphi (x)$
is a coherent formula, are coherent (and generate the topos). -
(ii) In a coherent topos there is (up to isomorphism) only a set of coherent objects.
-
(iii) A coherent topos $\mathcal {E}$
also has enough points (see, e.g., [Reference MacLane and Moerdijk18, Section IX.11]), meaning that the class of geometric morphisms
$\{p: \mathbf {Set} \to \mathcal {E}\}$
is jointly surjective (i.e., the inverse image functors
$\{p^*: \mathcal {E} \to \mathbf {Set}\}$
are jointly faithful/conservative). If
$\mathcal {E}$
classifies a theory T, this is equivalent to stating that T satisfies a completeness theorem—if
$\varphi (M) = \psi (M)$
for every model M in
$\mathbf {Set}$
, then
$\varphi $
and
$\psi $
are T-provably equivalent.
Generalising the above scenario, we will say that a topos
$\mathcal {E}$
has enough
$\mathcal {F}$
-points to mean that the class of geometric morphisms
$\{\mathcal {F} \to \mathcal {E}\}$
is jointly surjective.
3 Existentially closed models
The motivating objects for this article are the e.c. models (in
$\mathbf {Set}$
) of a coherent theory. In this section, we recall the basics of these objects to inspire and motivate definitions and results later on. As such, we only consider structures and models in
$\mathbf {Set}$
for this section.
Definition 3.1. Recall that a function
$f: M \to N$
between two structures in the same language is called a homomorphism if it preserves satisfaction of coherent formulas. That is, for all
$a \in M$
and all coherent
$\varphi (x)$
we have that
If f also reflects satisfaction of coherent formulas then we call it an immersion. That is, f is an immersion if for all
$a \in M$
and all coherent
$\varphi (x)$
we have that
By induction on the structure of formulas, one easily sees that f is a homomorphism if and only if it preserves satisfaction of all geometric formulas, if and only if it preserves all relations, constants, and function symbols. Similarly, a homomorphism is an immersion if and only if it reflects satisfaction of all geometric formulas.
Remark 3.2. Equivalently, a function
$f: M \to N$
defines a homomorphism if and only if, for any geometric formula
$\varphi $
, there is a factorisation
and f is an immersion if and only if this square is also a pullback of sets (where the map
$f: M \to N$
is interpreted in the appropriate sense, i.e., a product of the arrows on the respective sorts).
Remark 3.3. An immersion
$f: M \to N$
is always injective since
In fact, by the same reasoning, every immersion is an embedding (i.e., a map between structures that preserves and reflects satisfaction of all atomic formulas).
Definition 3.4. Let T be a coherent theory and let
$M \models T$
.
-
(i) We call M existentially closed (or e.c. for short) if every homomorphism $f: M \to N$
with
$N \models T$
is an immersion. -
(ii) We call M s.e.c. if, for every coherent formula $\varphi (x)$
and every
$a \in M$
such that
$M \not \models \varphi (a)$
, there is a coherent formula
$\psi (x)$
such that T proves the formula
$\neg \exists x(\varphi (x) \wedge \psi (x))$
(or equivalently, the sequent
$\varphi (x) \land \psi (x) \vdash _x \bot $
) and
$M \models \psi (a)$
.
Note that the definition of e.c. and s.e.c. depends on the theory T. This will often be omitted when the context is obvious.
It turns out that these definitions, for models of coherent theories in
$\mathbf {Set}$
, are equivalent. Indeed, both characterisations are often used for defining e.c. models in positive logic (also known as coherent logic). However, they both admit generalisations to models of geometric theories in arbitrary toposes, where the equivalence breaks down (see Example 5.10).
Fact 3.5 [Reference Ben-Yaacov and Poizat2, Lemme 14].
A model of a coherent theory T in
$\mathbf {Set}$
is e.c. if and only if it is s.e.c.
Remark 3.6. Some authors reserve the name “existentially closed” for the situation where every relation symbol (including equality) has a negation modulo the theory, or equivalently, when working with respect to embeddings rather than homomorphisms. The term “positive (existentially) closed” is then used for what we call “existentially closed.”
Example 3.7. We give some examples of classes of e.c. models.
-
(i) Let our language consist of infinitely many constant symbols, say $\{c_n\}_{n \in \mathbb {N}}$
, and let T declare all these symbols to be distinct. Then the only e.c. model is the model whose underlying set consists only of the constants (which are all distinct), for example,
$\mathbb {N}$
with
$c_n$
interpreted as n for all
$n \in \mathbb {N}$
. This is because if a model M contains an element
$a \in M$
that is not the interpretation of a constant then we can define a homomorphism
$f: M \to M$
that sends a to (the interpretation of)
$c_0$
and fixes everything else. Then f is not an immersion, as
$M \models f(a) = f(c_0)$
but
$M \not \models a = c_0$
. -
(ii) In the theory of fields, the e.c. models are the algebraically closed fields [Reference Tent and Ziegler19, Section 3.3.4].
-
(iii) Let T be the theory of graphs, with a symbol for inequality $\neq $
and a binary symbol for both the edge relation and its complement (so that homomorphisms between models of T are graph embeddings, that is, injective and they preserve and reflect the edge relation). Then the e.c. models of T are exactly those (infinite) graphs G such that, for any two finite disjoint sets of vertices
$A, B \subseteq G$
, there is a vertex
$v \in G \setminus (A \cup B)$
with an edge to every vertex in A and no edge to any vertex in B. In particular, the unique countable such graph (up to isomorphism) is the random graph or Rado graph [Reference Tent and Ziegler19, Exercise 3.3.1].
Remark 3.8. It is well-known that the class of e.c. models cannot always be axiomatised in finitary logic. Not even in full first-order logic (or equivalently: in coherent logic and allowing an expansion of the language, such as Morleyisation). See, for example, Example 3.7(i), where one quickly runs into issues with compactness. However, using the s.e.c. characterisation together with Fact 3.5, we see that the class of e.c. models of a coherent theory T is always geometrically axiomatisable, by adding to T a sequent
for every coherent formula
$\varphi (x)$
.
Finally, there is the following important fact. It guarantees not only that e.c. models exist, but also that when we care about eventual behaviour of models (as model theorists often do), then we only need to look at the e.c. models of a theory.
Fact 3.9 [Reference Ben-Yaacov and Poizat2, Theoreme 1].
Every model of a coherent theory T admits a homomorphism into an e.c. model of T.
4 Existentially closed geometric morphisms
We now generalise the notion of being e.c. from models to geometric morphisms. Any topos
$\mathcal {E}$
can be seen as the classifying topos of some geometric theory T, so geometric morphisms
$\mathcal {F} \to \mathcal {E}$
correspond to models of T in
$\mathcal {F}$
, while transformations between such geometric morphisms correspond to homomorphisms between the corresponding models.
As interpretations of geometric formulas correspond to subobjects (of the generic model) in
$\mathcal {E}$
, and following Remark 3.2, the following seems a straightforward generalisation of the definitions in Section 3.
Definition 4.1. Let
$p, q: \mathcal {F} \to \mathcal {E}$
be geometric morphisms. A transformation
is called an immersion if for any monomorphism
$a: A \hookrightarrow X$
in
$\mathcal {E}$
, the induced commuting square
is a pullback.
We say that a geometric morphism
$p: \mathcal {F} \to \mathcal {E}$
is e.c. if every transformation to any geometric morphism
$q: \mathcal {F} \to \mathcal {E}$
is an immersion.
Remark 4.2. Since writing this article, further equivalent conditions for a transformation to be an immersion have been identified in [Reference Kanalas16].
We gave an explanation for the reasoning behind this condition, at least when the object A is the interpretation of a geometric formula in the generic model of the theory that is classified by
$\mathcal {E}$
. It turns out that when this condition is met for a generating set of objects in
$\mathcal {E}$
(such as the set of interpretations of formulas in the generic model), then it will hold for all objects in
$\mathcal {E}$
. This makes being e.c. presentation independent, and so Morita-equivalent theories have the same categories of e.c. models. In particular, we see that our terminology is justified, because in the case of
$\mathcal {F} = \mathbf {Set}$
and coherent T it specialises back to the existing terminology (Corollary 4.5).
Proposition 4.3. Let
$\eta : p \Rightarrow q$
be a transformation of geometric morphisms
$p, q: \mathcal {F} \to \mathcal {E}$
, then
$\eta $
is an immersion if the condition in Definition 4.1 is met for all monomorphisms whose codomains are contained in some generating set of objects for
$\mathcal {E}$
. In particular, it suffices to check existential closedness for a geometric morphism on a generating set.
Proof. This follows from the fact that, in a Grothendieck topos
$\mathcal {E}$
, colimits are stable under pullback (see [Reference Giraud8] or [Reference MacLane and Moerdijk18, Appendix]), that is,
and that every object in
$\mathcal {E}$
is a colimit of objects in the generating set
$\mathcal {X}$
of
$\mathcal {E}$
.
Let
$X \cong \mathrm {colim}_{i \in I} X_i$
, where
$X_i \in \mathcal {X}$
. Then for any monomorphism
$A \leq X$
in
$\mathcal {E}$
, there is a chain of isomorphisms
where
$A_i$
denotes the pullback
$A \times _{X} X_i$
.
By composing the pullback squares
(the left-hand square is a pullback by hypothesis, while the right-hand square is a pullback since
$q^*$
preserves pullbacks), we have that
$p^*(A_i) \cong p^*(X_i) \times _{q^*(X)} q^*(A)$
, and hence we conclude that
as desired (using the fact that
$p^*$
commutes with colimits).
Remark 4.4. The proof given in Proposition 4.3 is valid if we replace ‘monomorphism’ in Definition 4.1 with any other property of an arrow that is stable under pullback in a topos, for example, epimorphism.
Corollary 4.5. A model M of a coherent theory T in
$\mathbf {Set}$
is e.c. according to Definition 3.4 if and only if the corresponding geometric morphism
$p: \mathbf {Set} \to \mathbf {Set}[T]$
is e.c. according to Definition 4.1.
Proof. By definition M is e.c. if and only if every homomorphism
$f: M \to N$
into a model of T is an immersion. Letting
$q: \mathbf {Set} \to \mathbf {Set}[T]$
be the geometric morphism corresponding to N, we can view f as a transformation
$p \Rightarrow q$
. Then by Remark 3.2 we see that f is an immersion in the classical sense (Definition 3.1) if it is an immersion as a transformation in the sense of Definition 4.1. The converse follows from Proposition 4.3, because the objects of the form
$\varphi (G_T)$
generate
$\mathbf {Set}[T]$
and by Remark 3.2 (and the pullback lemma) the naturality squares involving their subobjects, which are of the form
$\varphi \land \psi (G_T) \leq \varphi (G_T)$
, are pullbacks.
We have already seen examples of e.c. models, and thus e.c. geometric morphisms from
$\mathbf {Set}$
, in Example 3.7. We defer further examples to Example 5.10, once we have also generalised the notion of being strongly e.c. to geometric morphisms, so that we can compare the two.
Proposition 4.6. Given a geometric morphism
$p: \mathcal {F} \to \mathcal {E}$
and a jointly surjective family of geometric morphisms
$\{q_i: \mathcal {G} \to \mathcal {F}\}_{i \in I}$
, if the composite
$pq_i$
is e.c. for each
$i \in I$
, then so too is p.
Proof. Let
$\eta : p \Rightarrow r$
be a transformation into any geometric morphism
$r: \mathcal {F} \to~\mathcal{E}$
. Then we obtain a transformation
$q_i^*(\eta ): p q_i \Rightarrow r q_i$
, for each
$i \in I$
. As
$pq_i$
is e.c., for any subobject
$A \leq X$
in
$\mathcal {E}$
, we have that
$q_i^* p^*(A) = (q^*(\eta _X))^{-1}(q_i^* r^*(A)) = q_i^*(\eta _X^{-1}(r^*(A)))$
. As
$\{q_i: \mathcal {G} \to \mathcal {F}\}_{i \in I}$
is a jointly surjective family, we conclude that
$p^*(A) = \eta _X^{-1}(r^*(A))$
, and therefore that p is e.c.
4.1 The topos of existentially closed points
Given a geometric morphism
$p:~\mathcal {F} \to \mathcal {E}$
we write its (surjection, embedding)-factorisation as
$\mathcal {F} \twoheadrightarrow p(\mathcal {F}) \hookrightarrow \mathcal {E}$
. In particular,
$p(\mathcal {F})$
is a subtopos of
$\mathcal {E}$
, called the image of
$\mathcal {F}$
under p.
Definition 4.7. Given toposes
$\mathcal {F}$
and
$\mathcal {E}$
, let
$\mathcal {E}_{\mathcal {F}\text {-ec}} \hookrightarrow \mathcal {E}$
denote the subtopos
where the union is taken in the (complete) lattice of subtoposes of
$\mathcal {E}$
.
We can view the topos
$\mathcal {E}_{\mathcal {F}\textrm {-ec}}$
as a topos in its own right, or as a specified subtopos
$\mathcal {E}_{\mathcal {F}\textrm {-ec}} \hookrightarrow \mathcal {E}$
of
$\mathcal {E}$
. We will write
$\mathcal {E}_{\mathcal {F}\textrm {-ec}}$
alone to mean the topos, that is, the domain of the inclusion
$\mathcal {E}_{\mathcal {F}\textrm {-ec}} \hookrightarrow \mathcal {E}$
, and instead speak of the canonical inclusion
$\mathcal {E}_{\mathcal {F}\textrm {-ec}} \hookrightarrow \mathcal {E}$
when we mean
$\mathcal {E}_{\mathcal {F}\textrm {-ec}}$
as a subtopos of
$\mathcal {E}$
.
If we view
$\mathcal {E}$
as the classifying topos
$\mathbf {Set}[T]$
on some theory T then
$\mathcal {E}_{\mathcal {F}\text {-ec}}$
is the classifying topos of the common theory of the e.c. models of T in
$\mathcal {F}$
, that is,
$\mathcal {E}_{\mathcal {F}\text {-ec}} \simeq \mathbf {Set}[T^{\mathcal {F}\text {-ec}}]$
and
Proposition 4.8. The canonical inclusion
$\mathcal {E}_{\mathcal {F}{-ec}} \hookrightarrow \mathcal {E}$
is itself e.c.
Proof. The collection of geometric morphisms
$p: \mathcal {F} \to \mathcal {E}_{\mathcal {F}\textrm {-ec}}$
, such that the composition
$\mathcal {F} \xrightarrow {p} \mathcal {E}_{\mathcal {F}\textrm {-ec}} \hookrightarrow \mathcal {E}$
is e.c., is by construction jointly surjective. The statement thus follows from Proposition 4.6.
4.2 Entwined toposes
Different geometric theories can have the same category of e.c. models. For example, following Example 3.7(ii), the theories of fields and algebraically closed fields have the same e.c. models in
$\mathbf {Set}$
, namely the algebraically closed fields. Since we are interested in theories up to their e.c. models, we introduce the notion of entwinement. As we will see, two theories have equivalent categories of e.c. models if and only if they are entwined.
Definition 4.9. Fix a topos
$\mathcal {F}$
. We say that toposes
$\mathcal {E}$
and
$\mathcal {E}'$
are
$\mathcal {F}$
-entwined if we can find a topos
$\mathcal {G}$
and a pair of geometric embeddings
$i: \mathcal {E} \hookrightarrow \mathcal {G}$
and
$i': \mathcal {E}' \hookrightarrow \mathcal {G}$
such that, for every geometric morphism
$p: \mathcal {F} \to \mathcal {E}$
, there is a geometric morphism
$q: \mathcal {F}' \to \mathcal {E}'$
and a natural transformation
$\eta : ip \Rightarrow i'q$
, as in the diagram
and vice versa.
Remark 4.10. The definition of entwinement is motivated by the model-theoretic notion of a model companion
$T'$
of a theory T (see, e.g., [Reference Tent and Ziegler19, Definition 3.2.8]). Recall that this is a theory
$T'$
that is model complete (all its models are e.c. with respect to embeddings) and such that every model of T embeds into one of
$T'$
and vice versa. Entwinement is the weaker condition where models merely admit a homomorphism to one another.
Another difference between entwinement and model companions is that the former is a language-free version. That is, the question of whether T and
$T'$
are model companions only makes sense if they are formulated in the same language, as only then it makes sense to ask for embeddings between their models. Asking for the existence of
$\mathcal {G}$
in Definition 4.9 can be seen as asking for the existence of such a common language. That is, there are theories T and
$T'$
in the same language such that
$\mathcal {E}$
and
$\mathcal {E}'$
are the classifying toposes of T and
$T'$
, respectively.
Example 4.11. The choice of witnessing embeddings in entwinement matters. For example, take
$\mathcal {F} = \mathcal {E} = \mathcal {E}' = \mathbf {Set}$
. Then
$\mathcal {E}$
and
$\mathcal {E}'$
are
$\mathcal {F}$
-entwined, as witnessed by the trivial embeddings into
$\mathcal {G} = \mathbf {Set}$
. However, if we would take
$\mathcal {G} = \mathbf {Set} \times \mathbf {Set}$
, that is, the topos of sheaves on the discrete space with two points, and embed
$\mathcal {E}$
and
$\mathcal {E}'$
as disjoint subtoposes then the conclusion of Definition 4.9 does not hold. In the context of the intuition of Remark 4.10, this amounts to requiring there to be some common language, but not every common language may work.
Lemma 4.12. Being
$\mathcal {F}$
-entwined, for fixed
$\mathcal {F}$
, is an equivalence relation on toposes.
Proof. Only transitivity requires an argument. Suppose that
$\mathcal {E}$
and
$\mathcal {E}'$
are
$\mathcal {F}$
-entwined, as witnessed by
$\mathcal {E} \hookrightarrow \mathcal {G} \hookleftarrow \mathcal {E}'$
, and
$\mathcal {E}'$
and
$\mathcal {E}"$
are
$\mathcal {F}$
-entwined, as witnessed by
$\mathcal {E}' \hookrightarrow \mathcal {G}' \hookleftarrow \mathcal {E}"$
. By [Reference Johnstone12, Scholium B3.4.4] we can consider the pushout of
$\mathcal {G} \hookleftarrow \mathcal {E}' \hookrightarrow \mathcal {G}'$
to obtain a diagram of inclusions of toposes:
It is then straightforward to see that the cospan
$\mathcal {E} \hookrightarrow \mathcal {G}^* \hookleftarrow \mathcal {E}"$
witnesses that
$\mathcal {E}$
and
$\mathcal {E}"$
are
$\mathcal {F}$
-entwined.
The following makes precise how entwinement sees toposes (which can be viewed as geometric theories) up to e.c. models (i.e., e.c. geometric morphisms into them).
Proposition 4.13. Let
$\mathcal {F}$
,
$\mathcal {E,}$
and
$\mathcal {E}'$
be three toposes. Then
$\mathcal {E}$
and
$\mathcal {E}'$
are
$\mathcal {F}$
-entwined if and only if
$\mathcal {E}_{\mathcal {F}\mathrm{-ec}} \simeq \mathcal {E}^{\prime }_{\mathcal {F}\mathrm{-ec}}$
.
It follows from our proof that the category of e.c. geometric morphisms
$\mathcal {F} \to \mathcal {E}$
is equivalent to the category of e.c. geometric morphisms
$\mathcal {F} \to \mathcal {E}'$
. The converse holds if we additionally specify how this equivalence is induced (i.e., by composing with arrows into some fixed
$\mathcal {G}$
witnessing entwinement), but we will not make use of this.
The main ingredient in proving Proposition 4.13 is the following generalisation of Fact 3.9, which is of interest on its own as it shows that e.c. geometric morphisms are abundant.
Theorem 4.14. For any geometric morphism
$p: \mathcal {F} \to \mathcal {E}$
, there is an e.c. geometric morphism
$q: \mathcal {F} \to \mathcal {E}$
together with a transformation
$\eta : p \Rightarrow q$
.
We note that neither q nor
$\eta $
is in any way unique. For example, a field embeds into many different algebraically closed fields of various transcendence degrees, and can embed in such fields in many different ways (cf. Example 3.7(ii)).
Proof. Essentially the standard construction for models in
$\mathbf {Set}$
of a coherent theory, as found in [Reference Ben-Yaacov and Poizat2, Theoreme 1], can be adapted using the fact that
$\mathcal {F}$
is locally
$\lambda $
-presentable for some
$\lambda $
[Reference Johnstone12, Corollary D2.3.7]. For that reason, we temporarily adopt a more logical notation—let T be a geometric theory such that
$\mathcal {E}$
classifies T, that is,
$\mathcal {E} \simeq \mathbf {Set}[T]$
. Then p corresponds to a model M of T internal to
$\mathcal {F}$
. We will build an e.c. model N in
$\mathcal {F}$
, together with a homomorphism
$M \to N$
by constructing N as the colimit of a chain of T-models
$M = M^0 \to M^1 \to \cdots $
of length
$\lambda $
, which we construct by transfinite induction. This is enough, as we can then take q to be the geometric morphism corresponding to N and
$\eta $
the transformation corresponding to the homomorphism
$M \to N$
.
We take
$M_0$
as M, and at limit stages, we take the colimit of the chain we have constructed so far, which just leaves the successor step. Having constructed
$M^i$
we consider the set of all pairs
$(\varphi (x), a)$
, where
$\varphi (x)$
is a geometric formula in the language of T and
$a: A \to M^i$
is an arrow with
$\lambda $
-presentable domain. There is indeed only a set of those, because (up to provable equivalence) there is only a set of geometric formulas and (up to isomorphism) there is also only a set of
$\lambda $
-presentable objects. Enumerate the members of this set of pairs as
$\{(\varphi _j(x), a_j)\}_{j < \kappa _i}$
. We will construct
$M^{i+1}$
as the colimit of a chain of T-models
$M^i = M^i_0 \to M^i_1 \to \cdots $
of length
$\kappa _i$
. Again, at limit stages, we take the colimit of the chain we have constructed so far, which leaves us with the successor step.
Having constructed
$M^i_j$
, we consider two cases. If
$A \xrightarrow {a_j} M^i \to M^i_j$
does not factor through
$\varphi _j(M_j^i)$
, but there is a homomorphism
$h: M^i_j \to M'$
into a model of T such that
$A \xrightarrow {a_j} M^i \to M^i_j \xrightarrow {h} M'$
factors through
$\varphi _j(M')$
then we take
$M^i_{j+1} = M'$
with the homomorphism
$M^i_j \to M^i_{j+1}$
to be h. If this is not the case then we simply take
$M^i_{j+1} = M^i_j$
and the relevant arrow is the identity.
This completes the construction of N. We now show that N is indeed e.c. Let
$\varphi (x)$
be a geometric formula in the language of T and let
$g: N \to N'$
be a homomorphism into a model of T. Suppose we are given arrows
$a: A \to N$
and
$A \to \varphi (N')$
making the diagram below commute, we desire an arrow
making the whole diagram
commute. Note that, since
$\varphi (N) \hookrightarrow N$
is a monomorphism, such an arrow is automatically unique, and so this is enough to conclude that the bottom square is a pullback, and hence that N is e.c. as desired.
We first perform this for the case where A is
$\lambda $
-presentable. In that case the arrow
$a: A \to N$
will factor as
$A \xrightarrow {a'} M^i \to N$
for some
$i < \lambda $
. Let
$j < \kappa _i$
be such that
$(\varphi (x), a') = (\varphi _j(x), a_j)$
. We distinguish two cases to show that a factors through
$\varphi (N) \hookrightarrow N$
.
-
1. If $A \xrightarrow {a_j} M^i \to M^i_j$
factors through
$\varphi ({M^i_j}) \hookrightarrow M^i_j$
then it follows immediately by composing with the coprojections
$M^i_j \to M^{i+1} \to N$
. -
2. If $A \xrightarrow {a_j} M^i \to M^i_j$
does not factor through
$\varphi ({M^i_j} ) \hookrightarrow M^i_j$
then $$\begin{align*}M^i_j \to M^{i+1} \to N \xrightarrow{g} N'\end{align*}$$
yields a homomorphism, let’s denote it by k, into a model of T such that the composite $A \xrightarrow {a_j} M^i \to M^i_j \xrightarrow {k} N'$
factors through
$\varphi (N') \hookrightarrow N'$
. So by construction we must have that
$A \xrightarrow {a_j} M^i \to M^i_j \to M^i_{j+1}$
factors through
$\varphi ({M^i_{j+1}}) \hookrightarrow M^i_{j+1}$
. The claim then follows by composing with the coprojections
$M^i_{j+1} \to M^{i+1} \to N$
.
We thus have an arrow
such that in the diagram (2) the bottom triangle, the square, and the outer square commute. A simple diagram chase together with the fact that
$\varphi (N') \hookrightarrow N'$
is a monomorphism then shows that the top triangle also commutes, as desired.
Now let A be any object of
$\mathcal {F}$
, which can therefore be written as the
$\lambda $
-directed colimit of
$\lambda $
-presentable objects
$A = \mathrm {colim}_{i \in I} A_i$
. By composing with the coprojection
$A_i \to A$
, each
$A_i$
can be fitted into a diagram as in (2) and thus admits a commuting arrow
. The uniqueness of these arrows makes
$\varphi (N)$
into a cocone for
$(A_i)_{i \in I}$
. Thus, by the universal property of the colimit, we obtain the required arrow
.
Corollary 4.15. The toposes
$\mathcal {E}$
and
$\mathcal {E}_{\mathcal {F}-\mathrm{ec}}$
are
$\mathcal {F}$
-entwined.
Proof. Both toposes
$\mathcal {E}$
and
$\mathcal {E}_{\mathcal {F}\textrm {-ec}}$
are subtoposes of
$\mathcal {E}$
. Vacuously, every geometric morphism
$\mathcal {F} \to \mathcal {E}_{\mathcal {F}\textrm {-ec}} \hookrightarrow \mathcal {E}$
admits a transformation to a geometric morphism
. The converse is provided by Theorem 4.14.
Lemma 4.16. If
$i: \mathcal {E} \hookrightarrow \mathcal {G}$
is a subtopos, then any transformation between composite geometric morphisms
and
admits a horizontal factorisation, that is,
Proof. Recall that
$i: \mathcal {E} \hookrightarrow \mathcal {G}$
being a subtopos means that
$\mathcal {E}$
is a full reflective subcategory of
$\mathcal {G}$
. Hence, the component
$\eta ^{\prime }_X$
at an object
$X \in \mathcal {E}$
can be taken as
$p^*(X) \cong p^* i^* i_* (X) \xrightarrow {\eta _{i_*(X)}} q^* i^* i_* (X) \cong q^*(X)$
.
Proof of Proposition 4.13.
We first prove the left to right direction. Let
$i: \mathcal {E} \hookrightarrow \mathcal {G}$
and
$j: \mathcal {E}' \hookrightarrow \mathcal {G}$
witness that
$\mathcal {E}$
and
$\mathcal {E}'$
are
$\mathcal {F}$
-entwined. We first show that if
$p: \mathcal {F} \to \mathcal {E}$
is e.c., then
factors as
, after which we will show that the factor
$\mathcal {F} \xrightarrow {p'} \mathcal {E}'$
is also e.c.
Recall, from [Reference Johnstone12, Proposition A4.3.11] say, that the subtopos
$j: \mathcal {E}' \hookrightarrow \mathcal {G}$
is induced by a closure operator c on subobjects in
$\mathcal {G}$
, and that
factors through
$j: \mathcal {E}' \hookrightarrow \mathcal {G}$
if and only if
$p^*i^*(m)$
is an isomorphism for every c-dense monomorphism.
By
$\mathcal {F}$
-entwinement, there is a diagram
Let
$m: A \hookrightarrow X$
be a c-dense monomorphism in
$\mathcal {G}$
. In the commuting diagram
the morphism
$q^* j^* (m)$
is invertible. Also, by Lemma 4.16,
$\theta \eta $
admits a horizontal factorisation
$\theta ' \eta ': p \Rightarrow r$
, and so because p is e.c., the outside square is also a pullback. We aim to show that
$p^* i^* (m)$
is an isomorphism. This is equivalent to saying that there is a factorisation of subobjects
Such a factorisation is obtained via the universal property of the pullback, as in the diagram
where the necessary commutativity condition is given by
Hence,
factors as
.
We now show that
$p': \mathcal {F} \to \mathcal {E}'$
is e.c. Given a transformation
$\eta : p' \Rightarrow q$
to an arbitrary
$q: \mathcal {F} \to \mathcal {E}'$
, we will show that
$\eta $
is an immersion. By
$\mathcal {F}$
-entwinement there exists a diagram
and hence, for any
$A \leq X$
in
$\mathcal {G}$
, a commuting diagram
in
$\mathcal {F}$
. The outer square is a pullback since p is e.c., and so the left square is a pullback because the vertical arrows are monomorphisms. We conclude by noting that because
$\mathcal {E}'$
is a subtopos of
$ \mathcal {G}$
, and therefore a reflective subcategory, we may assume that any subobject inclusion in
$\mathcal {E}'$
is of the form
$j^*(A) \leq j^*(X)$
for
$A \leq X$
in
$\mathcal {G}$
(see also Lemma 7.3).
We have thus shown that if
$p: \mathcal {F} \to \mathcal {E}$
is an e.c. geometric morphism then
factors as
with
$p'$
also e.c. It follows that, as subtoposes of
$\mathcal {G}$
, the image
$p(\mathcal {F})$
is included in
$\mathcal {E}^{\prime }_{\mathcal {F}\textrm {-ec}}$
and so
$\mathcal {E}_{\mathcal {F}\textrm {-ec}}$
is included in
$\mathcal {E}^{\prime }_{\mathcal {F}\textrm {-ec}}$
. By symmetry, we have that the other inclusion also holds, hence
$\mathcal {E}_{\mathcal {F}\textrm {-ec}} \simeq \mathcal {E}^{\prime }_{\mathcal {F}\textrm {-ec}}$
.
Conversely, suppose that
$\mathcal {E}_{\mathcal {F}\textrm {-ec}} \simeq \mathcal {E}^{\prime }_{\mathcal {F}\textrm {-ec}}$
. By [Reference Johnstone12, Scholium B3.4.4] we can form the pushout of
$\mathcal {E} \hookleftarrow \mathcal {E}_{\mathcal {F}\textrm {-ec}} \simeq \mathcal {E}^{\prime }_{\mathcal {F}\textrm {-ec}} \hookrightarrow \mathcal {E}'$
to obtain
$\mathcal {E} \hookrightarrow \mathcal {G} \hookleftarrow \mathcal {E}'$
. Now let
$p: \mathcal {F} \to \mathcal {E}$
be any geometric morphism. By Theorem 4.14 there is an e.c. geometric morphism
$q: \mathcal {F} \to \mathcal {E}$
together with a transformation
$\eta : p \Rightarrow q$
. By the definition of
$\mathcal {E}_{\mathcal {F}\textrm {-ec}}$
, we have that q factors as
$\mathcal {F} \xrightarrow {q'} \mathcal {E}_{\mathcal {F}\textrm {-ec}} \hookrightarrow \mathcal {E}$
. We thus have that
$\mathcal {F} \xrightarrow {q'} \mathcal {E}_{\mathcal {F}\textrm {-ec}} \hookrightarrow \mathcal {E} \hookrightarrow \mathcal {G}$
is the same as
$\mathcal {F} \xrightarrow {q'} \mathcal {E}^{\prime }_{\mathcal {F}\textrm {-ec}} \hookrightarrow \mathcal {E}' \hookrightarrow \mathcal {G}$
, and so we can view
$\eta $
as a transformation from
$\mathcal {F} \xrightarrow {p} \mathcal {E} \hookrightarrow \mathcal {G}$
to the latter, as depicted below.
We conclude by symmetry that
$\mathcal {E}$
and
$\mathcal {E}'$
are
$\mathcal {F}$
-entwined.
Corollary 4.17. For any two toposes
$\mathcal {E}$
and
$\mathcal {F}$
we have
${\left (\mathcal {E}_{\mathcal {F}-\mathrm{ec}}\right )}_{\mathcal {F}-\mathrm{ec}} \simeq \mathcal {E}_{\mathcal {F}-\mathrm{ec}}$
.
5 Strongly existentially closed geometric morphisms
We now consider a topos-theoretic generalisation of s.e.c. models. Unlike e.c. models, the notion of being an s.e.c. model is highly dependent on the particular presentation of the theory (i.e., it is not a Morita invariant property, see Example 5.10). We will therefore need to include extra information about a choice of generating set and subobject basis for our topos. We will show in Theorem 5.8 that, in the case of coherent toposes, this choice can be removed.
Definition 5.1. Let
$\mathcal {E}$
be a topos, and let
$\mathcal {X}$
be a generating set of objects for
$\mathcal {E}$
. A subobject basis (for
$\mathcal {X}$
) is an indexed set
$\mathcal {B} = (\mathcal {B}_X)_{X \in \mathcal {X}}$
where, for each
$X \in \mathcal {X}$
,
$\mathcal {B}_X$
is a set of subobjects of X such that
$\mathcal {B}_X$
generates
$\mathrm {Sub}(X)$
under infinite joins.
For a generating set
$\mathcal {X}$
and a subobject basis
$\mathcal {B}$
we say that a geometric morphism
$p: \mathcal {F} \to \mathcal {E}$
is s.e.c. with respect to
$(\mathcal {X}, \mathcal {B})$
, or
$(\mathcal {X}, \mathcal {B})$
-s.e.c., if, for each subobject
$A \leq X$
in
$\mathcal {B,}$
For such subobjects
$A \leq X$
, we say that A is complemented along p.
We say that p is s.e.c. if p is
$(\mathcal {X}, \mathcal {B})$
-s.e.c. for some generating set
$\mathcal {X}$
and subobject basis
$\mathcal {B}$
.
In Corollary 5.9 we will see the motivation for this definition of s.e.c., and how it coincides with the classical notion from Definition 3.4.
Remark 5.2. Here,
$\neg A$
denotes the pseudo-complement of A in
$\mathrm {Sub}(X)$
(i.e., the subobject
$A \rightarrow \bot $
). For any geometric morphism
$p: \mathcal {F} \to \mathcal {E}$
, it is easily checked that
$p^*(\neg A) \leq \neg p^*(A)$
. The condition
$p^*(A \lor \neg A) = p^*(X)$
is equivalent to requiring that
$p^*(A)$
is complemented in
$\mathrm {Sub}(p^*(X))$
, and that
$p^*(\neg A)$
is that complement, in particular
$p^*(\neg A) = \neg p^*(A)$
.
Lemma 5.3. Let
$\mathcal {E}$
be some topos, let
$\mathcal {X}$
be a generating set for
$\mathcal {E,}$
and let
$\mathcal {B}$
be a subobject basis.
-
(i) If $p: \mathcal {F} \to \mathcal {E}$
is
$(\mathcal {X}, \mathcal {B})$
-s.e.c. then any composite
$pq: \mathcal {G} \to \mathcal {F} \to \mathcal {E}$
is
$(\mathcal {X}, \mathcal {B})$
-s.e.c. as well. -
(ii) If $\{q_i: \mathcal {G} \to \mathcal {F}\}_{i \in I}$
is a jointly surjective family of geometric morphisms and
$pq_i$
is
$(\mathcal {X}, \mathcal {B})$
-s.e.c. for all
$i \in I$
then p is
$(\mathcal {X}, \mathcal {B})$
-s.e.c.
Proof. The first statement is obvious from the definition: for each
$X \in \mathcal {X}$
, the subobject lattice
$\mathrm {Sub}(X)$
is generated by subobjects
$A \leq X$
in
$\mathcal {B}_X$
such that
$p^*(A \lor \neg A) = p^*(X)$
, and so
$q^* p^* (A \lor \neg A) = q^* p^*(X)$
as well.
For the second statement we note that
$q_i^* p^*(A \vee \neg A) = q_i^* p^*(X)$
for all subobjects
$A \leq X$
in
$\mathcal {B}_X$
and all
$i \in I$
. So since
$\{q_i: \mathcal {G} \to \mathcal {F}\}_{i \in I}$
is jointly surjective, we have that
$p^*(A \vee \neg A) = p^*(X)$
for all such
$A \leq X$
.
Definition 5.4. We call a subtopos
$i: \mathcal {F} \hookrightarrow \mathcal {E}\ (\mathcal {X}, \mathcal {B})$
-s.e.c. if the embedding i is
$(\mathcal {X}, \mathcal {B})$
-s.e.c. We call a subtopos s.e.c. if it is
$(\mathcal {X}, \mathcal {B})$
-s.e.c. for some
$(\mathcal {X}, \mathcal {B})$
.
Corollary 5.5. Let
$\mathcal {E}$
be some topos, let
$\mathcal {X}$
be a generating set for
$\mathcal {E,}$
and let
$\mathcal {B}$
be a subobject basis. A geometric morphism
$p: \mathcal {F} \to \mathcal {E}$
is
$(\mathcal {X}, \mathcal {B})$
-s.e.c. if and only if p factors through an
$(\mathcal {X}, \mathcal {B})$
-s.e.c. subtopos of
$\mathcal {E}$
.
Proof. If
$\mathcal {E}' \hookrightarrow \mathcal {E}$
is
$(\mathcal {X}, \mathcal {B})$
-s.e.c., then the composite
$\mathcal {F} \to \mathcal {E}' \hookrightarrow \mathcal {E}$
is
$(\mathcal {X}, \mathcal {B})$
-s.e.c. by Lemma 5.3(i). Conversely, consider the image factorisation
$\mathcal {F} \twoheadrightarrow p(\mathcal {F}) \hookrightarrow \mathcal {E}$
of p. The composite is
$(\mathcal {X}, \mathcal {B})$
-s.e.c. and
$\mathcal {F} \twoheadrightarrow p(\mathcal {F})$
is surjective, so by Lemma 5.3(ii)
$p(\mathcal {F}) \hookrightarrow \mathcal{E}$
is
$(\mathcal {X}, \mathcal {B})$
-s.e.c.
As suggested by the terminology, being s.e.c. is a stronger property than being e.c. See Example 5.10 for examples of e.c. morphisms that are not s.e.c.
Proposition 5.6. Any s.e.c. geometric morphism
$p: \mathcal {F} \to \mathcal {E}$
is also e.c.
The proof of Proposition 5.6 is an application of the following lemma.
Lemma 5.7. Let
$p: \mathcal {F} \to \mathcal {E}$
be a geometric morphism and suppose that
$A \leq X$
is complemented along p. Then for any geometric morphism
$q: \mathcal {F} \to \mathcal {E}$
and any transformation
$\eta : p \Rightarrow q$
the naturality square below is a pullback
$:$
Proof. Recall from Remark 5.2 that the requirement
$p^*(X) = p^*(A \lor \neg A)$
ensures that
$p^*(A)$
is complemented in
$\mathrm {Sub}(p^*(X))$
and that
$p^*(\neg A)$
is that complement.
We aim to show that
$p^*(A) = \eta ^{-1}_X(q^*(A))$
. One inequality,
$p^*(A) \leq \eta ^{-1}_X(q^*(A))$
, is provided by the commutativity of the naturality square. We also have that
Therefore, we compute that
Hence,
$\eta _X^{-1}(q^*(A)) \leq p^*(A)$
, concluding the proof.
Proof of Proposition 5.6.
Let
$(\mathcal {X}, \mathcal {B})$
be such that p is
$(\mathcal {X}, \mathcal {B})$
-s.e.c., and let
$\eta : p \Rightarrow q$
be any transformation into some geometric morphism
$q: \mathcal {F} \to \mathcal {E}$
. By Proposition 4.3 it suffices to show that, for every subobject
$A \leq X$
with
$X \in \mathcal {X}$
, the naturality square as in Lemma 5.7 is a pullback.
By assumption, there is a family of subobjects
$\{A_i \leq X\}_{i \in I}$
in
$\mathcal {B}_X$
that are complemented along p such that
$A = \bigvee _{i \in I} A_i$
. Using Lemma 5.7, we conclude that
as desired.
When the codomain topos of a geometric morphism is coherent, we can safely omit the choice of generating set and subobject basis since there exists a canonical choice.
Theorem 5.8. Let
$\mathcal {E}$
be a coherent topos and suppose that
$p: \mathcal {F} \to \mathcal {E}$
is s.e.c. Then for any coherent X and any compact subobject
$A \leq X$
, we have that A is complemented along p. In particular, taking
$\mathcal {E}_{\text {coh}}$
to be the set of coherent objects in
$\mathcal {E}$
and
$\mathcal {E}_{\text {comp}}$
to be the set of compact subobjects of coherent objects, we have that p is
$(\mathcal {E}_{\text {coh}}, \mathcal {E}_{\text {comp}})$
-s.e.c.
Proof. The “in particular” bit follows from the former because the coherent objects generate
$\mathcal {E}$
and because in a coherent topos, for any object X, its compact subobjects generate
$\mathrm {Sub}(X)$
.
Let
$(\mathcal {X},\mathcal {B})$
be such that p is
$(\mathcal {X},\mathcal {B})$
-s.e.c. We may assume that
$\mathcal {X}$
is closed under finite coproducts and subobjects. This can be done by closing
$\mathcal {X}$
first under finite coproducts and then under subobjects, as coproducts of subobjects are subobjects of coproducts. We quickly argue why these operations preserve the property that p is
$(\mathcal {X},\mathcal {B})$
-s.e.c.
Let
$\{X_i\}_{i \in I}$
be a (finite)Footnote
1
set of objects in
$\mathcal {X}$
. For each
$i \in I$
,
$\mathcal {B}_{X_i} $
is a family
$ \{A_j \leq X_i\}_{j \in J_i}$
of subobjects that generates
$\mathrm {Sub}(X_i)$
, each of which is complemented along p. Composing with the coprojection
$X_i \hookrightarrow \coprod _{i \in I} X_i$
, we may also view this as a family of subobjects of
$\coprod _{i \in I} X_i$
. Using the fact that coproducts in a Grothendieck topos are disjoint, one straightforwardly checks that, for each
$j \in J_i$
,
$A_j$
is also complemented along p as a subobject of
$\coprod _{i \in I} X_i$
. Letting i vary, we thus conclude that
$\{A_j \leq \coprod _{i \in I} X_i \mid i \in I, j \in J_i\}$
is a family of subobjects that generates
$\mathrm {Sub}(\coprod _{i \in I} X_i)$
, each of which is complemented along p. For closure under subobjects, let
$Y \leq X$
with
$X \in \mathcal {X}$
. Then
$\{A \wedge Y \leq Y \mid A \leq X \text { in } \mathcal {B}_X \}$
is generating for
$\mathrm {Sub}(Y)$
and each member is complemented along p.
Let
$A \leq X$
be a compact subobject of a coherent object, as in the statement. Then X admits a covering
$\{B_i \to X\}_{i \in I}$
by objects in
$\mathcal {X}$
, and each
$B_i$
admits a covering
$\{C_j \to B_i\}_{j \in J_i}$
by coherent objects. For each
$i \in I$
and each
$j \in J_i$
, the image
$C_j \twoheadrightarrow B^{\prime }_j \hookrightarrow B_i$
is compact, since
$B^{\prime }_j$
has a cover
$C_j \twoheadrightarrow B^{\prime }_j$
by a compact object (see [Reference Johnstone12, Lemma D3.3.3]). Thus, X admits a covering by compact objects in
$\mathcal {X}$
(as we assumed
$\mathcal {X}$
to be closed under subobjects). Moreover, as X is coherent, this covering can be taken to finite, and hence by taking the coproduct
$B = \coprod B^{\prime }_j$
, there is an epimorphism
$k: B \twoheadrightarrow X$
whose domain is a compact object in
$\mathcal {X}$
(by [Reference Johnstone12, Lemma D3.3.3] and the assumption that
$\mathcal {X}$
is closed under finite coproducts).
Since A and B are both compact, we have that the pullback
is compact too. By assumption, there is a family
$\{A_i\}_{i \in I}$
of subobjects of B such that
$k^{-1}(A) = \bigvee _{i \in I} A_i$
and
$A_i$
is complemented along p for all
$i \in I$
. Since
$k^{-1}(A)$
is compact, we may assume I to be finite. Using general facts about Heyting algebras, we have that
We thus compute that
and so we see that
$k^{-1}(A)$
is complemented along p.
The maps
$k^{-1}: \mathrm {Sub}(X) \to \mathrm {Sub}(B)$
and
$p^*(k)^{-1}: \mathrm {Sub}(p^*(X)) \to \mathrm {Sub}(p^*(B))$
are open frame homomorphisms (see [Reference MacLane and Moerdijk18, Exercise III.16]). In particular, they are morphisms of Heyting algebras. Using this, together with the fact that p preserves pullbacks and that
$k^{-1}(A)$
is complemented along p, we compute that
Since k is an epimorphism,
$p^*(k)$
is also an epimorphism, and so
$p^*(k)^{-1}$
is injective. Since
$p^*(B) = p^*(k^{-1}(X)) = p^*(k)^{-1}(p^*(X))$
, we thus conclude that
$p^*(A \vee \neg A) = p^*(X)$
, and so A is complemented along p, as required.
Corollary 5.9. A model of a coherent theory T in
$\mathbf {Set}$
is s.e.c. according to Definition 3.4 if and only if the corresponding geometric morphism
$p: \mathbf {Set} \to \mathbf {Set}[T]$
is s.e.c. according to Definition 5.1.
Proof. For the right to left direction we could string together Proposition 5.6, Corollary 4.5, and Fact 3.5. However, a direct proof will add intuition to Definition 5.1.
Let
$\mathcal {X}$
be the set of interpretations of coherent formulas in the generic model
$G_T$
in
$\mathbf {Set}[T]$
. For each
$\varphi (G_T) \in \mathcal {X}$
, we take
$\mathcal {B}_{\varphi (G_T)}$
as the set of subobjects
$\psi (G_T) \leq \varphi (G_T)$
where
$\psi $
is also a coherent formula, which are precisely the subobjects of
$\varphi (G_T)$
that are compact. By Theorem 5.8, it suffices to show that M is s.e.c. (in the sense of Definition 3.4) if and only if every
$\psi (G_T) \leq \varphi (G_T)$
, with
$\varphi $
and
$\psi $
coherent, is complemented along p.
We can compute the pseudo-complement of
$\psi (G_T)$
in
$\mathrm {Sub}(\varphi (G_T))$
, as
which can be further reduced to
So
$\psi (G_T) \leq \varphi (G_T)$
is complemented along p if and only if the sequent
holds in M. We conclude by noting the above sequent holding for every pair of coherent formulas
$\varphi (x)$
and
$\psi (x)$
exactly axiomatises M being s.e.c. (in the sense of Definition 3.4, see also Remark 3.8).
Example 5.10. We consider various (non-)examples of being s.e.c. or e.c. for models in
$\mathbf {Set}$
. Once the notion of a locally zero-dimensional topos has been introduced, we will give an example of a geometric morphism that is e.c. but not s.e.c. with respect to any choice of generating set or subobject basis in Example 6.12.
-
(i) Let T be any of the coherent theories from Example 3.7. In that example we classified the e.c. models of T. So, by Corollaries 4.5 and 5.9, a geometric morphism $p: \mathbf {Set} \to \mathbf {Set}[T]$
is e.c. and s.e.c. if and only if the corresponding model is e.c. (and hence s.e.c., by Fact 3.5). We will see additional examples where being e.c. and s.e.c. coincide in toposes different from
$\mathbf {Set}$
in Example 7.11. -
(ii) Let X be a topological space. Then we can view X as a propositional theory $T_X$
by introducing a propositional symbol for each open set of X, and have the geometric propositional theory
$T_X$
capture unions and intersections, so that
$\mathbf {Sh}(X) \simeq \mathbf {Set}[T_X]$
. An element
$x \in X$
becomes a
$\mathbf {Set}$
-model of
$T_X$
by setting
$x \models U$
if and only if
$x \in U$
. A homomorphism
$x \to y$
between two elements
$x, y \in X$
is just an inequality
$x \leq y$
in the specialisation order on X (i.e., for all opens
$U \subseteq X$
, if
$x \in U$
then
$y \in U$
). Let us now assume that X is sober, so its
$\mathbf {Set}$
-models correspond precisely to its elements. Then a point
$x \in X$
is e.c. if, whenever
$x \leq y$
, then
$y \in U$
also implies
$x \in U$
, and so
$y \leq x$
. In other words, a point
$x \in X$
is e.c. if and only if the point x is maximal in the pre-order
$(X, \leq )$
. In particular, in a sober T
$_1$
space all points are e.c. -
(iii) We continue the previous point. Suppose that X is a zero-dimensional space. Let $\mathcal {X}$
be the set of subterminal objects in
$\mathbf {Sh}(X)$
, and let
$\mathcal {B}$
be the set of complemented subobjects of subterminal objects. As X is zero-dimensional, we have that
$\mathcal {B}$
is a subobject basis for the generating set
$\mathcal {X}$
. As a result, every point of
$\mathbf {Sh}(X)$
is
$(\mathcal {X}, \mathcal {B})$
-s.e.c.If X is locally zero-dimensional, but not necessarily zero-dimensional (e.g., the space Y in Example 6.3) we can adjust the above by taking $\mathcal {X}$
to consist of all those subterminal objects in
$\mathbf {Sh}(X)$
that correspond to open zero-dimensional subspaces of X. Again, we take
$\mathcal {B}$
to be the set of complemented subobjects of objects in
$\mathcal {X}$
, and then every point of
$\mathbf {Sh}(X)$
is
$(\mathcal {X}, \mathcal {B})$
-s.e.c.When X is not locally zero-dimensional, being $(\mathcal {X}, \mathcal {B})$
-s.e.c. heavily depends on the choice of
$\mathcal {X}$
and
$\mathcal {B}$
. At least when X is Hausdorff, such a choice can always be made. Fix some
$x \in X$
. Let
$\mathcal {U}_0 = \{U \subseteq X \text { open} \mid x \in U\}$
and
$\mathcal {U}_1 = \{U \subseteq X \text { open} \mid x \in \neg U\}$
, where
$\neg U$
denotes the interior of
$X \setminus U$
, that is, the pseudo-complement of U in the Heyting algebra of opens of X. By Hausdorffness,
$\mathcal {U}_0 \cup \mathcal {U}_1$
is a basis for X. Once again, we take
$\mathcal {X}$
to be the set of subterminal objects in
$\mathbf {Sh}(X)$
and we let
$\mathcal {B}$
be the set of subobjects of subterminals corresponding to an open in
$\mathcal {U}_0 \cup \mathcal {U}_1$
. The geometric morphism
$p: \mathbf {Set} \to \mathbf {Sh}(X)$
corresponding to x is then
$(\mathcal {X}, \mathcal {B})$
-s.e.c. Indeed, let
$V \in \mathcal {X}$
. If
$x \not \in V$
then
$p^*$
evaluates V and all its subobjects to
$0$
. Otherwise, let
$U \leq V$
in
$\mathcal {B}_V$
, we either have
$U \in \mathcal {U}_0$
, and so
$p^*(U \vee \neg U) = p^*(U) \vee p^*(\neg U) = 1 \vee 0 = 1 = p^*(V)$
, or we have
$U \in \mathcal {U}_1$
, and so
$p^*(U \vee \neg U) = p^*(U) \vee p^*(\neg U) = 0 \vee 1 = 1 = p^*(V)$
.The above choice heavily depends on the point $x \in X$
. For example, when
$X = \mathbb {R}$
with the usual Euclidean topology, then the above choice will be different for different points. One easily checks that if
$(\mathcal {X}, \mathcal {B})$
is as above for some
$x \in \mathbb {R}$
, then for any
$x' \neq x$
we have that the morphism
$p': \mathbf {Set} \to \mathbf {Sh}(X)$
corresponding to
$x'$
is not
$(\mathcal {X}, \mathcal {B})$
-s.e.c.
We note that the above shows that there can be no version of Theorem 4.14 for
$(\mathcal {X}, \mathcal {B})$
-s.e.c. That is, any of the above examples of an e.c. model that is not
$(\mathcal {X}, \mathcal {B})$
-s.e.c. cannot admit a homomorphism into an
$(\mathcal {X}, \mathcal {B})$
-s.e.c. model, as that homomorphism would then be an immersion (since the domain is e.c.) and one quickly verifies that this implies that the domain then has to be
$(\mathcal {X}, \mathcal {B})$
-s.e.c. as well.
6 Locally zero-dimensional toposes
The axiomatisation of s.e.c. models described in Remark 3.8 is reminiscent of the notion of zero-dimensionality in topology. Indeed, Theorem 7.1 will solidify this connection. To that end, in this section we introduce the notion of a locally zero-dimensional topos.
6.1 Zero-dimensional locales
Before defining locally zero-dimensional toposes, we recall some facts regarding zero-dimensional and locally zero-dimensional locales. Zero-dimensional locales extend the classical notion of a zero-dimensional space from topology, that is, those spaces with a basis of clopen subsets.
Definition 6.1. A locale L is called zero-dimensional if every element is a join of complemented elements. A locale L is called locally zero-dimensional if there exists an open cover
$\mathcal {U} \subseteq L$
such that, for every
$U \in \mathcal {U}$
, the open sub-locale
$U \hookrightarrow L$
, that is, the locale
$U = \{V \in L \mid V \leq U\}$
, is zero-dimensional.
As one would expect, a topological space is (locally) zero-dimensional if and only if its locale of open sets is (locally) zero-dimensional.
Recall that a morphism of locales
$f: X \to Y$
is a local homeomorphism if X admits an open covering
$\mathcal {U}$
such that, for each
$U \in \mathcal {U}$
there is
$V \in Y$
such that f restricts to a homeomorphism
$U \to V$
(see, e.g., [Reference MacLane and Moerdijk18, Exercise IX.9]).
Lemma 6.2. Suppose that
$f: X \to Y$
is a local homeomorphism of locales. If Y is locally zero-dimensional, then so is X. Conversely, if f is epic and X is locally zero-dimensional, then Y is locally zero-dimensional too.
Proof. Suppose that Y is locally zero-dimensional. Then X admits an open covering
$\mathcal {U}$
such that each
$U \in \mathcal {U}$
is homeomorphic to an open sub-locale of Y, which is therefore locally zero-dimensional.
Conversely, suppose that f is epic and X is locally zero-dimensional. There is an open covering
$\mathcal {U}$
of X such that
$f(U)$
is open and
$f|_U: U \to f(U)$
is a homeomorphism for each
$U \in \mathcal {U}$
. Since zero-dimensionality is inherited by sub-locales, each
$U \in \mathcal {U}$
admits a covering by opens that are zero-dimensional, so we may as well assume that each
$U \in \mathcal {U}$
is zero-dimensional, and thus
$f(U)$
is zero-dimensional too. Finally, as f is epic,
$\{ f(U) \mid U \in \mathcal {U} \}$
describes an open covering of Y.
Example 6.3. The statement in Lemma 6.2 cannot be modified by replacing ‘locally zero-dimensional’ with ‘zero-dimensional’. The idea of this counterexample is due to Peter Johnstone, and appears in [Reference Bunge and Funk4, Example 3.3]. Let
$X = \mathbb {N} \cup \{\infty \}$
be the one-point compactification of the natural numbers (which carry the discrete topology) and let
$Y = (X + X) / {\sim }$
be the quotient space that is obtained by identifying the two copies of
$\mathbb {N}$
. The evident quotient maps
are both epic local homeomorphisms. Moreover, X and
$X+X$
are zero-dimensional, but Y is only locally zero-dimensional.
6.2 Locally zero-dimensional toposes
Definition 6.4. We call an object X in a topos
$\mathcal {E}$
a zero-dimensional object (resp. locally zero-dimensional object) if
$\mathrm {Sub}(X)$
is a zero-dimensional (resp. locally zero-dimensional) as a locale.
Our definition of locally zero-dimensional topos requires a choice of a generating set of objects, but like we have seen for s.e.c. geometric morphisms, there is a canonical choice if the topos is coherent (see Theorem 6.10).
Definition 6.5. We say that a topos
$\mathcal {E}$
is locally zero-dimensional if there is a generating set of zero-dimensional objects.
Remark 6.6. Evidently, a topos is locally zero-dimensional if and only if there is a generating set of locally zero-dimensional objects, because each locally zero-dimensional object is covered by zero-dimensional objects.
The following justifies our terminology of locally zero-dimensional topos.
Proposition 6.7. For a locale L, the following are equivalent:
-
(i) L is a locally zero-dimensional locale;
-
(ii) $\mathbf {Sh}(L)$
is a locally zero-dimensional topos; -
(iii) every object in $\mathbf {Sh}(L)$
is locally zero-dimensional.
Proof. Clearly, using
$\mathrm {Sub}(1) \cong L$
and that the subterminals in
$\mathbf {Sh}(L)$
generate the topos, (i) implies (ii) and (iii) implies (i). It remains to show that (ii) implies (iii). We will use the description of
$\mathbf {Sh}(L)$
as the slice
$\mathbf {LH}/L$
of local homeomorphisms over L. For each local homeomorphism
$f: Y \to L$
, there is a diagram
in which both arrows are local homeomorphisms (see, for instance, [Reference Johnstone12, Theorem C1.4.7]). The coproduct
$\coprod _{i \in I} L$
is locally zero-dimensional since L is locally zero-dimensional; hence, the sub-locale U inherits this local zero-dimensionality. Finally, Y is locally zero-dimensional by an application of Lemma 6.2.
Remark 6.8. Recall from Example 6.3 that there exists a local homeomorphism
$Y \to L$
where L is zero-dimensional but Y is only locally zero-dimensional. Thus, a locale L being zero-dimensional does not imply that every subobject frame in
$\mathbf {Sh}(L)$
is zero-dimensional.
Question 6.9. For any topos
$\mathcal {E}$
, it quickly follows that if all objects in
$\mathcal {E}$
are locally zero-dimensional then
$\mathcal {E}$
is locally zero-dimensional. Does the converse hold in general?
Theorem 6.10. Let
$\mathcal {E}$
be a locally zero-dimensional coherent topos, then every coherent object in
$\mathcal {E}$
is zero-dimensional.
Proof. We could prove the statement directly. But we have already proved a stronger version in the form of Theorem 5.8. We describe how to massage a locally zero-dimensional coherent topos into the form needed by Theorem 5.8.
Let
$\mathcal {X}$
be a generating set of zero-dimensional objects, and let
$\mathcal {B}$
be the set of subobjects of objects in
$\mathcal {X}$
that are complemented. Then the identity functor
${id}_{\mathcal {E}}$
is
$(\mathcal {X}, \mathcal {B})$
-s.e.c., because being complemented along
${id}_{\mathcal {E}}$
is equivalent to just being complemented. We can thus apply Theorem 5.8 to see that
${id}_{\mathcal {E}}$
is
$(\mathcal {E}_{\text {coh}}, \mathcal {E}_{\text {comp}})$
-s.e.c. This precisely means that compact subobjects of coherent objects are complemented. As such subobjects generate
$\mathrm {Sub}(X)$
in a coherent topos, we conclude that X is indeed zero-dimensional.
The relevance of local zero-dimensionality for us is the following.
Proposition 6.11. Any geometric morphism
$p: \mathcal {F} \to \mathcal {E}$
into a locally zero-dimensional topos
$\mathcal {E}$
is s.e.c. More precisely, if
$\mathcal {X}$
is a generating set of zero-dimensional objects in
$\mathcal {E}$
then, letting
$\mathcal {B}_X$
be the set of complemented subobjects of
$X \in \mathcal {X}$
, any geometric morphism
$p: \mathcal {F} \to \mathcal {E}$
is
$(\mathcal {X}, \mathcal {B})$
-s.e.c.
Proof. This amounts to writing out definitions: any subobject
$A \leq X$
in
$\mathcal {B}_X$
is complemented in
$\mathrm {Sub}(X)$
, so
$A \vee \neg A = X$
. Therefore, such a subobject is complemented along any geometric morphism into
$\mathcal {E}$
.
Example 6.12. We return to the problem of finding an e.c. geometric morphism that is not s.e.c. with respect to any generating set and subobject basis. Let X be a sober,
$T_1$
space that is not locally zero-dimensional and consider the identity geometric morphism
${id}_{\mathbf {Sh}(X)}$
. Since X is
$T_1$
,
${id}_X$
is maximal in the specialisation order on endomorphisms on X, and so for the same reason as in Example 5.10(ii),
${id}_{\mathbf {Sh}(X)}$
is an e.c. geometric morphism. But to say that
${id}_{\mathbf {Sh}(X)}$
is s.e.c. (with respect to some generating set and subobject basis) is to say that
$\mathbf {Sh}(X)$
is locally zero-dimensional, which is not the case by Proposition 6.7.
7 The classifying topos of e.c. models
In this section, we return to the study of the topos
$\mathcal {E}_{\mathcal {F}\textrm {-ec}}$
of e.c.
$\mathcal {F}$
-points. We give a characterisation of
$\mathcal {E}_{\mathcal {F}\textrm {-ec}}$
under the assumption that the e.c. morphisms
$\mathcal {F} \to \mathcal {E}$
are all
$(\mathcal {X},\mathcal {B})$
-s.e.c. for some choice of
$(\mathcal {X},\mathcal {B})$
. Thus, we will recover our motivating case, where
$\mathcal {E}$
classifies a coherent theory and
$\mathcal {F} = \mathbf {Set}$
, but we will also see other examples where
$\mathcal {F}$
does not have to be taken as
$\mathbf {Set}$
.
Theorem 7.1. Let
$\mathcal {F}$
and
$\mathcal {E}$
be any two toposes. Suppose that for some generating set
$\mathcal {X}$
of
$\mathcal {E}$
, with subobject basis
$\mathcal {B}$
, we have that every e.c. geometric morphism
$p: \mathcal {F} \to \mathcal {E}$
is
$(\mathcal {X}, \mathcal {B})$
-s.e.c. Then the following are equivalent for a topos
$\mathcal {G}$
with enough
$\mathcal {F}$
-points:
-
(i) $\mathcal {G} \simeq \mathcal {E}_{\mathcal {F}\textrm {-ec}}$
; -
(ii) $\mathcal {G}$
is locally zero-dimensional and
$\mathcal {F}$
-entwined with
$\mathcal {E}$
; -
(iii) $\mathcal {G}$
is equivalent to the maximal
$(\mathcal {X}, \mathcal {B})$
-s.e.c. subtopos of
$\mathcal {E}$
with enough
$\mathcal {F}$
-points.
Remark 7.2. We note that, by a simple application of Corollary 5.5, the assumptions of Theorem 7.1 are necessary as well as sufficient. Specifically, if the canonical inclusion
$\mathcal {E}_{\mathcal {F}\textrm {-ec}} \hookrightarrow \mathcal {E}$
is an
$(\mathcal {X},\mathcal {B})$
-s.e.c. subtopos of
$\mathcal {E}$
, then every e.c. geometric morphism
$p: \mathcal {F} \to \mathcal {E}$
is
$(\mathcal {X},\mathcal {B})$
-s.e.c.
In order to prove the theorem, we must show that, under the assumptions of the theorem,
$\mathcal {E}_{\mathcal {F}\textrm {-ec}}$
is
$(\mathcal {X},\mathcal {B})$
-s.e.c./locally zero-dimensional. This is a consequence of the following results.
Lemma 7.3. Let
$i: \mathcal {F} \hookrightarrow \mathcal {E}$
be a geometric embedding. Then the induced map on subobjects
$i^*: \mathrm {Sub}(X) \to \mathrm {Sub}(i^*(X))$
is surjective for all X in
$\mathcal {E}$
.
Proof. Let
$B \leq i^*(X)$
be a subobject. We first form the following pullback in
$\mathcal {E}$
:
where
$\eta $
is the unit of the adjunction
$i^* \dashv i_*$
. Then we take the transpose of that square under this adjunction, which is pictured on the left below, and decomposes as the diagram on the right below:
where
$\varepsilon $
is the counit of the adjunction
$i^* \dashv i_*$
. In the diagram on the right both squares are pullbacks: the left square because it is the image of a pullback under the finite limit preserving functor
$i^*$
, and the right square because
$\varepsilon $
is an isomorphism. The transposed square is thus a pullback, and so the arrow
$i^*(A) \to B$
is an isomorphism. We conclude that
$i^*(A) = B$
as subobjects of
$i^*(X)$
.
Proposition 7.4. If
$i: \mathcal {F} \hookrightarrow \mathcal {E}$
is an s.e.c. subtopos, then
$\mathcal {F}$
is locally zero-dimensional.
Proof. Let
$(\mathcal {X}, \mathcal {B})$
be such that the inclusion
$i: \mathcal {F} \hookrightarrow \mathcal {E}$
is
$(\mathcal {X}, \mathcal {B})$
-s.e.c. Then
$i^*(\mathcal {X}) = \{i^*(X) \mid X \in \mathcal {X}\}$
is a generating set for
$\mathcal {F}$
, so it suffices to show that
$\mathrm {Sub}(i^*(X))$
is zero-dimensional for each
$X \in \mathcal {X}$
. For each
$A \leq X$
in
$\mathcal {B}_X$
we have that
$i^*(A)$
is complemented in
$\mathrm {Sub}(i^*(X))$
. We thus conclude by noting that
$\{i^*(A) \mid A \leq X \text { in } \mathcal {B}_X\}$
generates
$\mathrm {Sub}(i^*(X))$
, as
$i^*$
induces a surjection
$\mathrm {Sub}(X) \to \mathrm {Sub}(i^*(X))$
by Lemma 7.3 and it preserves joins of subobjects.
Proposition 7.5. Let
$\mathcal {F}$
and
$\mathcal {E}$
be any two toposes. Suppose that for some generating set
$\mathcal {X}$
of
$\mathcal {E}$
, with subobject basis
$\mathcal {B}$
, we have that every e.c. geometric morphism
$p: \mathcal {F} \to \mathcal {E}$
is
$(\mathcal {X}, \mathcal {B})$
-s.e.c. Then the canonical inclusion
$\mathcal {E}_{\mathcal {F}\textrm {-ec}} \hookrightarrow \mathcal {E}$
is
$(\mathcal {X}, \mathcal {B})$
-s.e.c., and so in particular
$\mathcal {E}_{\mathcal {F}\textrm {-ec}}$
is locally zero-dimensional.
Proof. By construction,
$\mathcal {E}_{\mathcal {F}\textrm {-ec}}$
has enough
$\mathcal {F}$
-points, and each
$\mathcal {F} \to \mathcal {E}_{\mathcal {F}\textrm {-ec}} \hookrightarrow \mathcal {E}$
is
$(\mathcal {X}, \mathcal {B})$
-s.e.c. by assumption. So
$\mathcal {E}_{\mathcal {F}\textrm {-ec}} \hookrightarrow \mathcal {E}$
is
$(\mathcal {X}, \mathcal {B})$
-s.e.c. by Lemma 5.3(ii), and the final remark then follows from Proposition 7.4.
Proof of Theorem 7.1.
We first prove (i)
$\Leftrightarrow $
(ii). The left to right direction follows from Propositions 4.13 and 7.5. For the converse we note that, as a subtopos of itself,
$\mathcal {G} = \bigcup \{ p(\mathcal {F}) \mid p: \mathcal {F} \to \mathcal {G} \text { a geometric morphism}\}$
because
$\mathcal {G}$
has enough
$\mathcal {F}$
-points. As
$\mathcal {G}$
is locally zero-dimensional, by Propositions 5.6 and 6.11, every geometric morphism
$\mathcal {F} \to \mathcal {G}$
is e.c., and so we have that
$\mathcal {G} \simeq \mathcal {G}_{\mathcal {F}\textrm {-ec}}$
. Finally, since
$\mathcal {G}$
and
$\mathcal {E}$
are
$\mathcal {F}$
-entwined, by Proposition 4.13 we conclude that
$\mathcal {G} \simeq \mathcal {G}_{\mathcal {F}\textrm {-ec}} \simeq \mathcal {E}_{\mathcal {F}\textrm {-ec}}$
.
We prove (i)
$\Leftrightarrow $
(iii) by showing that the canonical inclusion
$\mathcal {E}_{\mathcal {F}\textrm {-ec}} \hookrightarrow \mathcal {E}$
is the maximal
$(\mathcal {X}, \mathcal {B})$
-s.e.c. subtopos of
$\mathcal {E}$
with enough
$\mathcal {F}$
-points. Firstly,
$\mathcal {E}_{\mathcal {F}\textrm {-ec}}$
has enough
$\mathcal {F}$
-points by construction and is
$(\mathcal {X}, \mathcal {B})$
-s.e.c. by Proposition 7.5. Let
$\mathcal {H} \hookrightarrow \mathcal {E}$
be any
$(\mathcal {X}, \mathcal {B})$
-s.e.c. subtopos with enough
$\mathcal {F}$
-points. From being s.e.c. it follows from Lemma 5.3 and Proposition 5.6 that any composite
$\mathcal {F} \to \mathcal {H} \hookrightarrow \mathcal {E}$
is e.c. So by construction of
$\mathcal {E}_{\mathcal {F}\textrm {-ec}}$
, any such composite factors through
$\mathcal {E}_{\mathcal {F}\textrm {-ec}}$
. As before, from the assumption that
$\mathcal {H}$
has enough
$\mathcal {F}$
-points it follows that
$\mathcal {H} = \bigcup \{ p(\mathcal {F}) \mid p: \mathcal {F} \to \mathcal {H} \text { a geometric morphism}\}$
, and so we conclude that
$\mathcal {H} \hookrightarrow \mathcal {E}$
factors through
$\mathcal {E}_{\mathcal {F}\textrm {-ec}} \hookrightarrow \mathcal {E}$
. Thus,
$\mathcal {E}_{F\textrm {-ec}} \hookrightarrow \mathcal {E}$
is the maximal
$(\mathcal {X},\mathcal {B})$
-s.e.c. subtopos of
$\mathcal {E}$
with enough
$\mathcal {F}$
-points as claimed, from which the equivalence (i)
$\Leftrightarrow $
(iii) immediately follows.
Corollary 7.6. Suppose that a topos
$\mathcal {E}'$
is
$\mathcal {F}$
-entwined with a topos
$\mathcal {E}$
that satisfies the assumptions of Theorem 7.1. Then for a topos
$\mathcal {G}$
we have
$\mathcal {G} \simeq \mathcal {E}^{\prime }_{\mathcal {F}\textrm {-ec}}$
if and only if
$\mathcal {G}$
has enough
$\mathcal {F}$
-points, is locally zero-dimensional, and is
$\mathcal {F}$
-entwined with
$\mathcal {E}'$
.
Proof. By Proposition 4.13 we have that
$\mathcal {E}^{\prime }_{\mathcal {F}\textrm {-ec}} \simeq \mathcal {E}_{\mathcal {F}\textrm {-ec}}$
, and so we simply apply Theorem 7.1.
The hypotheses of Theorem 7.1 are satisfied in our original motivating case of e.c. models in
$\mathbf {Set}$
of some coherent theory T. We discuss the simplifications of Theorem 7.1 that can be made.
Remark 7.7. If
$\mathcal {E}$
is a coherent topos, then by Theorem 5.8 we do not need to worry about the generating set
$\mathcal {X}$
and subobject basis
$\mathcal {B}$
as these can be taken to be
$\mathcal {E}_{\text {coh}}$
and
$\mathcal {E}_{\text {comp}}$
, respectively. So the assumptions of Theorem 7.1 simplify to “every e.c. geometric morphism
$\mathcal {F} \to \mathcal {E}$
is s.e.c.” In the conclusion of that theorem, we can now also simplify (iii) to characterise
$\mathcal {E}_{\mathcal {F}\textrm {-ec}}$
as the maximal s.e.c.-subtopos of
$\mathcal {E}$
with enough
$\mathcal {F}$
-points.
After Definition 4.7 we discussed how
$\mathbf {Set}[T]_{\mathcal {F}\textrm {-ec}}$
is the classifying topos of the common geometric theory
$T^{\mathcal {F}\textrm {-ec}}$
of the e.c. models of T in
$\mathcal {F}$
. We simplify the notation for the case where
$\mathcal {F} = \mathbf {Set}$
and T is coherent.
Definition 7.8. Let T be a coherent theory. We define
$T^{\mathrm{ec}}$
to be the common geometric theory of all e.c. models of T in
$\mathbf {Set}$
. That is:
In particular,
$T^{\mathrm{ec}}$
axiomatises the class of e.c. models of T in
$\mathbf {Set}$
(see Remark 3.8).
Theorem 1.1. repeated, Let T be a coherent theory. Then the following are equivalent for a topos
$\mathcal {G}$
with enough points:
-
(i) $\mathcal {G} \simeq \mathbf {Set}[T^{\mathrm{ec}}]$
; -
(ii) $\mathcal {G}$
is locally zero-dimensional and
$\mathbf {Set}$
-entwined with
$\mathbf {Set}[T]$
; -
(iii) $\mathcal {G}$
is equivalent to the maximal s.e.c.-subtopos of
$\mathbf {Set}[T]$
with enough points.
Proof. Note that
$\mathbf {Set}[T^{\mathrm{ec}}] \simeq \mathbf {Set}[T]_{\mathbf {Set}\textrm {-ec}}$
by the discussion after Definition 4.7. Then the statement is just a simplification of Theorem 7.1, following Remark 7.7 and using Fact 3.5, which states that e.c. models of T in
$\mathbf {Set}$
are s.e.c.
7.1 Models with an endomorphism
Of course, the generality of Theorem 7.1 allows for more applications than just the case
$\mathcal {F} = \mathbf {Set}$
. We finish this section by giving a class of such examples when
$\mathcal {F}$
is taken to be the topos
$\mathbf {Set}^{\mathbb {N}}$
or
$\mathbf {Set}^{\mathbb {Z}}$
(where
$\mathbb {N}$
and
$\mathbb {Z}$
are considered as monoids). In particular, a model of a theory T in
$\mathbf {Set}^{\mathbb {N}}$
(resp.
$\mathbf {Set}^{\mathbb {Z}}$
) is a pair
$(M, \sigma )$
consisting of a
$\mathbf {Set}$
-model M of T and an endomorphism (resp. automorphism)
$\sigma : M \to M$
of the model.
Proposition 7.9. Let T be a coherent theory with the amalgamation property for
$\mathbf {Set}$
-models, that is, any span of homomorphisms
$M_1 \leftarrow M_0 \to M_2$
of
$\mathbf {Set}$
-models can be completed to a commuting square. Then, for a model
$(M, \sigma )$
of T in
$\mathbf {Set}^{\mathbb {N}}$
, the following are equivalent:
-
(i) $(M, \sigma )$
is e.c. in
$\mathbf {Set}^{\mathbb {N}}$
; -
(ii) $(M, \sigma )$
is s.e.c. in
$\mathbf {Set}^{\mathbb {N}}$
; -
(iii) M is e.c. in $\mathbf {Set}$
; -
(iv) M is s.e.c. in $\mathbf {Set}$
.
The same is true when
$\mathbf {Set}^{\mathbb {N}}$
is replaced by
$\mathbf {Set}^{\mathbb {Z}}$
.
Proof. The implications (ii)
$\Rightarrow $
(i) and (iii)
$\Leftrightarrow $
(iv) follow from Proposition 5.6 and Fact 3.5. Furthermore, (iv)
$\Rightarrow $
(ii) easily follows from forgetting
$\sigma $
, as the interpretation of geometric formulas remains the same (equivalently stated, we apply Lemma 5.3(ii) with the surjective geometric morphism
$\mathbf {Set} \twoheadrightarrow \mathbf {Set}^{\mathbb {N}}$
).
We prove (i)
$\Rightarrow $
(iv) by showing that M immerses into an s.e.c.
$\mathbf {Set}$
-model of T, which straightforwardly implies that M is s.e.c. too. We note that there exists a homomorphism of models
$f: M \to N$
where N is an
$|M|^+$
-homogeneous and e.c. model of T (and so N is also s.e.c. by Fact 3.5). Recall that an e.c. model N is
$\kappa $
-homogeneous if for any two tuples a and b of the same length
$< \kappa $
, we have that
$\mathrm {tp}(a; N) = \mathrm {tp}(b; N)$
implies that there is an automorphism
$\tau : N \to N$
that sends a to b (pointwise). Here,
$\mathrm {tp}(a; N)$
is the model-theoretic notion of (positive) type: the set of all coherent formulas satisfied by a in N. Such a homomorphism
$f: M \to N$
can be constructed by the usual model-theoretic methods (see, e.g., [Reference Tent and Ziegler19, Section 6.1]). We must show that f is an immersion.
By our assumption on T, the span
$N \xleftarrow {\, f \, } M \xrightarrow {f \sigma } N$
can be amalgamated to obtain a commuting square of
$\mathbf {Set}$
-models
Let m be an (infinite) tuple that enumerates the model M. As N is e.c., the homomorphisms g and h are immersions, and so they both preserve and reflect the satisfaction of coherent formulas. Therefore, we have that
and so by homogeneity there is an automorphism
$\tau : N \to N$
sending
$f(m)$
to
$f \sigma (m)$
. As m enumerated all of M, this is equivalent to saying that
$\tau f = f \sigma $
. Now viewing
$(N, \tau )$
as a model of T in
$\mathbf {Set}^{\mathbb {N}}$
, it follows that
$f: (M, \sigma ) \to (N, \tau )$
is a homomorphism of models internal to
$\mathbf {Set}^{\mathbb {N}}$
. Since
$(M,\sigma )$
was assumed to be e.c. in
$\mathbf {Set}^{\mathbb {N}}$
, this means that f is an immersion as desired, thus concluding the proof that M is s.e.c.
The same proof applies if
$\sigma $
is assumed to be an automorphism, and since the
$\tau $
we construct is an automorphism, the statement for
$\mathbf {Set}^{\mathbb {Z}}$
also follows.
Corollary 7.10. If T is a coherent theory with the amalgamation property for
$\mathbf {Set}$
-models, the hypotheses of Theorem 7.1 are satisfied for
$\mathcal {E} = \mathbf {Set}[T]$
and
$\mathcal {F} = \mathbf {Set}^{\mathbb {N}}$
or
$\mathbf {Set}^{\mathbb {Z}}$
.
Example 7.11. We give some examples of coherent theories with the amalgamation property for
$\mathbf {Set}$
-models.
-
(i) The theory of fields has the amalgamation property. It follows that a difference field (i.e., a field with an endomorphism) is e.c. in $\mathbf {Set}^{\mathbb {N}}$
(or
$\mathbf {Set}^{\mathbb {Z}}$
) if and only if the underlying field is algebraically closed (see Example 3.7(ii)). Difference fields have been studied model-theoretically before by adding the endomorphism to the language [Reference Chatzidakis and Hrushovski7, Reference Macintyre17]. Note that the e.c. models of a field with an endomorphism in the language differ from the e.c. models of fields in
$\mathbf {Set}^{\mathbb {N}}$
. This is because, in the former case, since the endomorphism forms part of the language, an e.c. model also needs to contain solutions to certain difference polynomials (i.e., polynomials where the endomorphism can be applied to the variables, called basic systems in [Reference Macintyre17]). -
(ii) The theory of algebraically closed exponential fields. These are algebraically closed fields with a group homomorphism from the additive group to the multiplicative group, called the exponential map. This is clearly coherently axiomatisable, and any span of such fields can be amalgamated by [Reference Haykazyan and Kirby10, Theorem 4.3]. The requirement that the underlying field is algebraically closed is important for the amalgamation property. If we would just consider exponential fields then the amalgamation property fails in a strong sense: for any exponential field $F_0$
whose underlying field is not algebraically closed, we can find a span
$F_1 \leftarrow F_0 \to F_2$
of exponential fields that cannot be amalgamated (this is also [Reference Haykazyan and Kirby10, Theorem 4.3]). -
(iii) The theory of decidable graphs, see also Example 3.7(iii), has the amalgamation property, given by the pushout of graphs. If we remove the requirement that the graphs are decidable we still have the amalgamation property, but the theory trivialises from the point of view of e.c. models: the only e.c. model is the graph with one vertex (i.e., the terminal object in the category of graphs).
8 Atomic e.c. models and double negation sheaves
As an application of the above, we replicate [Reference Blass and Scĕdrov3, Theorem 6], using a different proof, to characterise those points on a coherent topos that factorise through the double negation sheaves on that topos (Theorem 8.12). It turns out, these are precisely the e.c. models that are atomic (see Definition 8.8).
8.1 Denseness and e.c. models
The topos of double negation sheaves
$\mathbf {Sh}_{\neg \neg }(\mathcal {E})$
is the smallest dense subtopos of
$\mathcal {E}$
(see [Reference Johnstone12, Corollary A4.5.20]). Therefore, we first relate the notion of a dense subtopos to our ongoing study of the canonical inclusion
$\mathcal {E}_{\mathcal {F}\textrm {-ec}} \hookrightarrow \mathcal {E}$
of the topos of e.c.
$\mathcal {F}$
-points.
Definition 8.1. Recall that a subtopos
$i: \mathcal {F} \hookrightarrow \mathcal {E}$
is called dense if
$i^*(X) \cong 0$
implies
$X \cong 0$
for all
$X \in \mathcal {E}$
.
Lemma 8.2. If
$i: \mathcal {F} \hookrightarrow \mathcal {E}$
is dense, then
$i^*$
preserves pseudo-complements. That is, for any subobject
$A \leq X$
in
$\mathcal {E}$
we have
$i^*(\neg A) = \neg i^*(A)$
in
$\mathrm {Sub}(i^*(X))$
.
Proof. We can explicitly compute
$\neg A$
as
$\bigvee \{ B \leq X \mid B \wedge A \cong 0 \}$
. Similarly, using that
$i^*: \mathrm {Sub}(X) \to \mathrm {Sub}(i^*(X))$
is surjective (Lemma 7.3), we have that
$\neg i^*(A) = \bigvee \{i^*(B) \mid B \leq X \text { and } i^*(B) \wedge i^*(A) \cong 0 \}$
. We deduce the result because
$i^*(B) \wedge i^*(A) \cong i^*(B \wedge A) \cong 0$
if and only if
$B \wedge A \cong 0$
, by denseness.
Proposition 8.3. Let
$\mathcal {E}$
be any topos and let
$\mathcal {X}$
be a generating set for
$\mathcal {E}$
with subobject basis
$\mathcal {B}$
. Then a dense subtopos of
$\mathcal {E}$
is
$(\mathcal {X}, \mathcal {B})$
-s.e.c. if and only if
$i^*(A)$
is complemented in
$\mathrm {Sub}(i^*(X))$
for every subobject
$A \leq X$
in
$\mathcal {B}_X$
.
Proof. Recall from Remark 5.2 that a subobject
$A \leq X$
in
$\mathcal {E}$
being complemented along i is equivalent to
$i^*(A)$
being complemented in
$\mathrm {Sub}(i^*(X))$
and
$i^*(\neg A) = \neg i^*(A)$
. The statement thus follows from Lemma 8.2.
Proposition 8.4. If a topos
$\mathcal {E}$
has enough
$\mathcal {F}$
-points, then the canonical inclusion
$i: \mathcal {E}_{\mathcal {F}\text {-ec}} \hookrightarrow \mathcal {E}$
is dense.
Proof. Let X be any object in
$\mathcal {E}$
and suppose that
$i^*(X) \cong 0$
. We must show that
$X \cong 0$
. Since
$\mathcal {E}$
has enough
$\mathcal {F}$
-points, it suffices to show that
$p^*(X) \cong 0$
for each geometric morphism
$p: \mathcal {F} \to \mathcal {E}$
. By Theorem 4.14, there is a transformation
$\eta : p \Rightarrow q$
where q is an e.c. geometric morphism, which therefore factors through i, and so
$q^*(X) \cong 0$
. Then there is an arrow
$\eta _X: p^*(X) \to q^*(X) \cong 0$
. As the initial object in a topos is strict (see [Reference Johnstone12, Lemma A1.4.1]), this implies that
$p^*(X) \cong 0$
.
Corollary 8.5. For a coherent theory T, the inclusion
$\mathbf {Set}[T^{\mathrm{ec}}] \hookrightarrow \mathbf {Set}[T]$
is dense.
Proof. Proposition 8.4 applies, because T is coherent, so
$\mathbf {Set}[T]$
has enough points.
Remark 8.6. By viewing an arbitrary topos
$\mathcal {E}$
as the classifying topos
$\mathbf {Set}[T]$
of some geometric theory T, we can view a subtopos
$\mathcal {F} \hookrightarrow \mathcal {E}$
as the classifying topos
$\mathbf {Set}[T']$
of some quotient theory
$T'$
of T [Reference Caramello6, Theorem 3.2.5]. In particular, following [Reference Caramello6, Section 4.2.4], a subtopos
$\mathbf {Set}[T'] \hookrightarrow \mathbf {Set}[T]$
is dense if and only if, for every regular formula
$\varphi (x)$
, we have that the sequent
$\varphi (x) \vdash _x \bot $
(i.e.,
$\forall x \neg \varphi (x)$
) is derivable from T if and only if it is derivable from
$T'$
.
Let now T be a coherent theory. By combining the above with Corollary 8.5 we arrive at the well-known fact that the common universal theory of e.c. models of T in
$\mathbf {Set}$
is the same as the universal consequences of T. That is, for any regular
$\varphi (x)$
, we have that
$\forall x \neg \varphi (x)$
holds in every e.c. model of T in
$\mathbf {Set}$
if and only if
$\forall x \neg \varphi (x)$
can be derived from T.
Corollary 8.7. If T is a coherent theory, then
$\mathbf {Sh}_{\neg \neg }(\mathbf {Set}[T]) \simeq \mathbf {Sh}_{\neg \neg }(\mathbf {Set}[T^{\mathrm{ec}}])$
.
Proof. This follows immediately from the characterisation of the double negation sheaves as the smallest dense subtopos combined with Proposition 8.4.
8.2 Atomic e.c. models
We now turn to replicating [Reference Blass and Scĕdrov3, Theorem 6].
Definition 8.8. We call a model M in
$\mathbf {Set}$
of a (coherent) theory T atomic if each finite tuple in M is supported, that is, for each
$a \in M$
, there is a geometric formula
$\varphi (x)$
with
$M \models \varphi (a)$
such that, for each geometric formula
$\psi (x)$
with
$M \models \psi (a)$
, we have that
$\varphi (x) \vdash _x \psi (x)$
is derivable from T. We say that
$\varphi (x)$
supports a.
We could have equivalently assumed that the formulas
$\varphi (x)$
and
$\psi (x)$
in Definition 8.8 were both regular, because every geometric formula is provably equivalent to a disjunction of regular formulas.
Remark 8.9. We also briefly note that what we call “supported” is called “isolated” in classical model theory, because it means exactly that the type of a is an isolated point in the space of types. However, in positive model theory this correspondence no longer holds, and so “isolated” would not be a good term. See also the discussion after [Reference Kamsma14, Definition 5.1].
Remark 8.10. In [Reference Blass and Scĕdrov3, pp. 135–136] the notion in Definition 8.8 is called “strongly atomic.” As is explained there, this is to distinguish from the notion where we replace “
$\!\varphi (x) \vdash _x \psi (x)$
is derivable from T” with “
$\!\varphi (x) \vdash _x \psi (x)$
is valid in M.” We chose this terminology because it coincides with modern terminology [Reference Caramello5, Reference Haykazyan9, Reference Kamsma14]. Even though [Reference Kamsma14, Definition 5.4] focuses only on coherent logic, Definition 8.8 is still equivalent, because we may restrict to regular formulas, as mentioned above. Our notion of atomic is the same as that from [Reference Haykazyan9, Definition 6.1], as is explained in [Reference Kamsma14, Definition 5.2]. If we add the requirement that the model is e.c., then our notion coincides with [Reference Caramello5, Definition 3.15], at least for coherent theories, because the requirement there that every type realised in M is “complete” is equivalent to saying that M is e.c.
Example 8.11. Being atomic alone does not imply being e.c. For example, let T be the empty theory in the empty language. Then its models in
$\mathbf {Set}$
are pure sets, and the singletons are e.c. models. However, every non-empty set is an atomic model. For a tuple a in some non-empty set M this is witnessed by the formula
$\varphi $
, which is a conjunction of all the equalities between the singletons in a, together with
$\exists x(x=x)$
.
Theorem 8.12. Let T be a coherent theory. Then a point
$p: \mathbf {Set} \to \mathbf {Set}[T]$
factors through the double negation subtopos
$\mathbf {Sh}_{\neg \neg }(\mathbf {Set}[T])$
if and only if the model M in
$\mathbf {Set}$
corresponding to p is an atomic e.c. model (atomic with respect to
$T^{\mathrm{ec}}$
).
One step in the proof immediately follows from Proposition 8.3 above.
Lemma 8.13. If
$p: \mathbf {Set} \to \mathbf {Set}[T]$
factors through
$\mathbf {Sh}_{\neg \neg }(\mathbf {Set}[T])$
, then the corresponding model M is e.c.
Proof. Since
$\mathbf {Sh}_{\neg \neg }(\mathbf {Set}[T]) \hookrightarrow \mathbf {Set}[T]$
is a dense, Boolean subtopos, by Proposition 8.3, it is an s.e.c. subtopos. The result now follows by Corollary 5.5 and Proposition 5.6.
The remainder of the proof is based on a useful fact (Fact 8.15) about sub-open geometric morphisms, for which we use the characterisation in [Reference Johnstone11, Lemma 1.7] as a definition.
Definition 8.14 [Reference Johnstone11].
Recall that a frame homomorphism
$h: X \to Y$
is called sub-open if h preserves the Heyting implication. In particular, an open frame homomorphism is sub-open (by [Reference Joyal and Tierney13, Proposition V.1.1]).
A geometric morphism
$f: \mathcal {F} \to \mathcal {E}$
is then called sub-open if for every object X in
$\mathcal {E}$
the induced frame homomorphism
$f^*: \mathrm {Sub}(X) \to \mathrm {Sub}(f^*(X))$
is sub-open.
Fact 8.15 [Reference Johnstone11, Proposition 3.6].
A geometric morphism
$f: \mathcal {F} \to \mathcal {E}$
, with
$\mathcal {F}$
a Boolean topos, is sub-open if and only if it factors through
$\mathbf {Sh}_{\neg \neg }(\mathcal {E})$
.
Example 8.16. Recall that a frame homomorphism is open if it is a complete Heyting algebra homomorphism. An example of a frame homomorphism that is sub-open but not open, that is, preserves the Heyting implication but not infinite meets, is described in [Reference Johnstone11, Example 2.4]. Take the set
$X = \omega + 2^\omega $
and let
$X^{\mathrm {cof}}$
and
$X^{\mathrm {coc}}$
denote, respectively, the topological spaces obtained by endowing the set X with the cofinite and cocountable topologies. The frame homomorphism corresponding to the identity on X, acting as a continuous map
${id}_X \colon X^{\mathrm {coc}} \to X^{\mathrm {cof}}$
, is sub-open, since for both the cofinite and cocountable topologies the Heyting implication
$U \rightarrow V$
between two opens is given by
$(X \setminus U) \cup V$
, but it is not open—one meet that is not preserved is
$\bigwedge _{n \in \mathbb {N}} \{x \in \omega : n \leq x\} + 2^\omega $
.
Lemma 8.17. It suffices to check sub-openness on a generating set. Explicitly, let
$\mathcal {E}$
be a topos with a choice of generating set
$\mathcal {X}$
and let
$f: \mathcal {F} \to \mathcal {E}$
be a geometric morphism. If, for each
$X \in \mathcal {X}$
, the induced map
$f^*: \mathrm {Sub}(X) \to \mathrm {Sub}(f^*(X))$
is sub-open, then
$f^*: \mathrm {Sub}(Y) \to \mathrm {Sub}(f^*(Y))$
is sub-open for all objects Y in
$\mathcal {E}$
.
Proof. There exists a jointly epimorphic family of morphisms
$\{g_i: X_i \to Y\}_{i \in I}$
in
$\mathcal {E}$
with
$X_i \in \mathcal {X}$
. Thus, there exists a commuting square of frames
where the vertical maps are open and yield jointly injective families
$\{g_i^{-1}\}_{i \in I}$
and
$\{f^*(g_i)^{-1}\}_{i \in I}$
. Therefore, we compute that, for each
$i \in I$
and
$A,B \leq Y$
,
Now using that the family of maps
$\{f^*(g_i)^{-1}\}_{i \in I}$
is jointly injective, we conclude that
$f^*(A \rightarrow B) = f^*(A) \rightarrow f^*(B)$
as desired.
Proof of Theorem 8.12.
First consider the case where
$p: \mathbf {Set} \to \mathbf {Set}[T]$
factors through
$\mathbf {Sh}_{\neg \neg }(\mathbf {Set}[T]) \simeq \mathbf {Sh}_{\neg \neg }(\mathbf {Set}[T^{\mathrm{ec}}])$
. By Lemma 8.13, p is e.c., and so p factors as
$\mathbf {Set} \xrightarrow {q} \mathbf {Set}[T^{\mathrm{ec}}] \hookrightarrow \mathbf {Set}[T]$
, where q is also sub-open by Fact 8.15. It remains to show that M is atomic (modulo
$T^{\mathrm{ec}}$
). For a given
$a \in M$
, we note that, via De Morgan’s law (which is valid in
$\mathbf {Set}$
),
where i denotes the subtopos inclusion
$i \colon \mathbf {Set}[T^{\mathrm{ec}}] \hookrightarrow \mathbf {Set}[T]$
. As q is sub-open,
$q^*$
is a sub-open map on subobjects, in particular
$q^*$
preserves Heyting negation, in addition to arbitrary joins. Thus, we have that
But
$\neg \bigvee \{\neg i^* (\psi (G_T) )\mid \psi (x) \text { coherent, } M \models \psi (a) \}$
is a subobject of the inverse image of the generic model
$i^*(G_T)$
in
$\mathbf {Set}[T^{\mathrm{ec}}]$
, and every such subobject is of the form
$i^*(\varphi (G_T))$
by Lemma 7.3. Finally, we note that, modulo the theory
$T^{\mathrm{ec}}$
, every coherent formula has a complement as a subobject of the generic model. Thus, we can again use the validity of De Morgan’s law for complemented subobjects to arrive at the equality of subobjects
in
$\mathbf {Set}[T^{\mathrm{ec}}]$
. It is now easily checked that
$\varphi (x)$
supports a (modulo
$T^{\mathrm{ec}}$
).
Conversely, suppose that M is both e.c. and atomic with respect to
$T^{\mathrm{ec}}$
, which entails that M is s.e.c. by Fact 3.5. Let
$q \colon \mathbf {Set} \to \mathbf {Set}[T^{\mathrm{ec}}]$
denote the factorisation of p through
$i \colon \mathbf {Set}[T^{\mathrm{ec}}] \hookrightarrow \mathbf {Set}[T]$
. We aim to show that
$q^*$
preserves Heyting implication of subobjects. By Lemma 8.17, it suffices to show that
$q^*$
preserves Heyting implication of subobjects of the form
$i^*(\varphi (G_T))$
, since the interpretations of formulas in the generic model generate the topos
$\mathbf {Set}[T^{\mathrm{ec}}]$
. That is, we aim to show that
is equal to
One inclusion, namely that
$q^*(i^*(\varphi (G_T)) \rightarrow i^*(\psi (G_T)))$
is included in
$\varphi (M) \rightarrow \psi (M)$
, follows from the universal property of the Heyting implication. We prove the other inclusion.
Clearly, if
$M \models \psi (a)$
, then tautologically
$T^{\mathrm{ec}}$
proves
$\varphi (x) \land \psi (x) \vdash _x \psi (x)$
and so
$a \in \psi (M) \subseteq q^*(i^*(\varphi (G_T)) \rightarrow i^*(\psi (G_T)))$
. Suppose instead that
$M \not \models \varphi (a)$
. Since M is atomic, there is some formula
$\xi (x)$
that supports a. We claim that
$T^{\mathrm{ec}}$
proves
$\varphi (x) \land \xi (x) \vdash _x \psi (x)$
, and hence
$a \in \xi (M) \subseteq q^*(i^*(\varphi (G_T)) \rightarrow i^*(\psi (G_T)))$
. First, express
$\varphi (x)$
as a disjunction
$\bigvee _{i \in I} \varphi _i(x)$
of coherent formulas. Now let
$i \in I$
be arbitrary. As M is s.e.c. and
$M \not \models \varphi _i(a)$
, there is some
$\zeta _i(x)$
such that
$M \models \zeta _i(a)$
and
$T^{\mathrm{ec}}$
proves
$\varphi _i(x) \land \zeta _i(x) \vdash _x \bot $
. By the choice of
$\xi (x)$
,
$T^{\mathrm{ec}}$
proves
$\xi (x) \vdash _x \zeta _i(x)$
, and so
$T^{\mathrm{ec}}$
also proves
$\varphi _i(x) \wedge \xi (x) \vdash _x \bot $
. As
$i \in I$
was arbitrary, the chain of derivations
can be derived from
$T^{\mathrm{ec}}$
. Thus, q is sub-open and so factors through
$\mathbf {Sh}_{\neg \neg }(\mathbf {Set}[T^{\mathrm{ec}}])$
. Finally, we apply the equivalence
$\mathbf {Sh}_{\neg \neg }(\mathbf {Set}[T^{\mathrm{ec}}]) \simeq \mathbf {Sh}_{\neg \neg }(\mathbf {Set}[T])$
from Corollary 8.7 to have that p factors through
$\mathbf {Sh}_{\neg \neg }(\mathbf {Set}[T])$
as desired.
9 Countably categorical theories and atomic toposes
Finally, using [Reference Caramello5], we relate atomic e.c. models to the notion of countable categoricity from positive model theory [Reference Haykazyan9, Reference Kamsma14]. For this section, we revert to our convention that a “model” intends a model in
$\mathbf {Set}$
.
Definition 9.1. A coherent theory T is called countably categorical if, up to isomorphism, there is one (at most) countable e.c. model of T.
Remark 9.2. We have taken the definition of countably categorical from positive model theory here (see, e.g., [Reference Haykazyan9, Theorem 6.5] or [Reference Kamsma14, Definition 5.1]). Note that this definition restricts to e.c. models, and so it allows T to have non-isomorphic countable models. This is in contrast to, for example, [Reference Caramello5, Definition 3.14], where a geometric theory T is called countably categorical if any two countable models are isomorphic. The two major differences between these definitions are then that [Reference Caramello5] considers all models and that the version in [Reference Caramello5] can be vacuously satisfied. Hence, a coherent theory T is countable categorical (in our sense) if and only if
$T^{\mathrm{ec}}$
has a countable model and is countably categorical in the sense of [Reference Caramello5]. The requirement that
$T^{\mathrm{ec}}$
has a countable model is automatic in most practical cases: if T is a countable theory, then this follows from the downward Löwenheim–Skolem theorem.
Example 9.3. The reason for restricting ourselves to e.c. models in Definition 9.1 is because positive model theory only studies the e.c. models. For example, take the theory from Example 3.7(i), which consisted of a countable infinity of distinct constant symbols and nothing more. Clearly this theory has many non-isomorphic countable models: namely one for every
$n \leq \omega $
, which corresponds to having n elements that are not the interpretation of a constant symbol. When
$n = 0$
this describes the only e.c. model. In particular, there is only one countable e.c. model, and so this theory is countably categorical.
A more natural example comes from [Reference Kamsma14, Definition 2.1] by considering the common theory of K-bilinear spaces for a fixed field K, that is, the theory consisting of those coherent sequents satisfied by all K-bilinear spaces. If K is countable then this theory turns out to be countably categorical [Reference Kamsma14, Corollary 5.9]. However, there are still many non-isomorphic countable models, but these will in general not even be K-bilinear spaces. For example, by compactness there will be countable models with a realisation for the set of formulas
$\{[x,y] \neq \lambda \mid \lambda \in K\}$
, but which nonetheless satisfies the same coherent sequents as held in common by all K-bilinear spaces.
Remark 9.4. Our definition of countably categorical allows for having a unique finite model. Model-theoretically, this case is often ignored, because a complete first-order theory with a finite model has that model as its only model. Analogously, a coherent theory with JCP (see Definition 9.5) with a finite e.c. model has that model as its only e.c. model. However, there is no harm in allowing this trivial case.
Definition 9.5. A coherent theory T is said to have the joint continuation property, or JCP, if for any two of its models M and
$M'$
, there is a third model N admitting homomorphisms
$M \to N \leftarrow M'$
.
In light of the fact that every model of T admits a homomorphism into an e.c. model (Fact 3.9), we may assume that the model N above is an e.c. model.
Lemma 9.6. A consistent coherent theory has JCP if and only if
$T^{\mathrm{ec}}$
is complete in the sense of [Reference Caramello5, Definition 3.4], that is, every geometric sentence is
$T^{\mathrm{ec}}$
-provably equivalent to either
$\top $
or
$\bot $
, but not both.
Proof. Suppose that T has JCP. Let
$\varphi $
be any geometric sentence and let M and
$M'$
be a pair of e.c. models of T. Then there is a model N admitting homomorphisms
$M \to N \leftarrow M'$
. As M and
$M'$
are both e.c., these homomorphisms are immersions, and so we have that
We thus see that the truth value of
$\varphi $
in M determines its truth value in all e.c. models of T, and so we must have that either
$\top \vdash \varphi $
or
$\varphi \vdash \bot $
is in
$T^{\mathrm{ec}}$
.
For the converse, let M and
$M'$
be models of T. We extend our language with constant symbols for the elements of M and
$M'$
(which we may assume to be disjoint) and define a theory
We define
$T_{M'}$
analogously. Now consider the theory
$T' = T \cup T_M \cup T_{M'}$
. We will show that
$T'$
has a model N. Such a model
$N \models T'$
demonstrates that T has JCP because
$N \models T$
, and we can define a function
$M \to N$
by sending an element of M to the interpretation of the corresponding constant in N, which is a homomorphism because
$N \models T_M$
. Similarly,
$N \models T_{M'}$
yields a homomorphism
$M' \to N$
.
Note that as
$T'$
is a coherent theory, we can apply a compactness argument to show that it has a model. First observe that, by taking a finite conjunction of the sentences involved, every finite sub-theory
$S \subseteq T_M$
is equivalent to the theory
$\{\top \vdash _x \varphi (a)\}$
for a finite tuple
$a \in M$
and
$\varphi (x)$
a conjunction of atomic formulas for which
$M \models \varphi (a)$
. Using Fact 3.9, there exists a homomorphism
$f: M \to N$
with N an e.c. model of T. Thus,
$N \models \varphi (f(a))$
and so
$N \models \exists x \varphi (x)$
. As
$T^{\mathrm{ec}}$
is complete,
$\exists x \varphi (x)$
must be derivable from
$T^{\mathrm{ec}}$
. Now let
$g: M' \to N'$
be another homomorphism with
$N'$
an e.c. model of T. Then
$N' \models \exists x \varphi (x)$
, so let
$b \in N'$
be such that
$N' \models \varphi (b)$
. We can now expand
$N'$
to a model of
$T \cup T_{M'} \cup \{\top \vdash _x \varphi (a)\}$
over our expanded language: for each element
$c \in M'$
, the corresponding constant symbol is interpreted by
$g(c)$
, and we interpret constant symbols corresponding to the tuple a as b. The interpretation of the remaining constant symbols coming from
$M $
does not matter, and so we obtain a model of
$T \cup T_{M'} \cup \{\top \vdash _x \varphi (a)\}$
. We have thus shown that
$T'$
is finitely satisfiable, and so it has a model by compactness, which concludes our proof.
Theorem 9.7. Let T be a coherent theory in a countable language with JCP. Then T is countably categorical if and only if
$\mathbf {Set}[T^{\mathrm{ec}}]$
is atomic and non-degenerate.
Proof. Under either assumption in the result,
$T^{\mathrm{ec}}$
is consistent. Indeed, if T is countably categorical, then by definition
$T^{\mathrm{ec}}$
has a model, namely the unique countable e.c. model of T. On the other hand,
$\mathbf {Set}[T^{\mathrm{ec}}]$
has enough points by construction and so it is non-degenerate if and only if it has a point, that is,
$T^{\mathrm{ec}}$
has a model. Thus, by Lemma 9.6,
$T^{\mathrm{ec}}$
is complete in the sense of [Reference Caramello5].
We can thus apply [Reference Caramello5, Theorem 3.16], which (once specialised to our situation) states that the following are equivalent:
-
(i) any two countable models of $T^{\mathrm{ec}}$
are isomorphic and
$\mathbf {Set}[T^{\mathrm{ec}}]$
is Boolean; -
(ii) $\mathbf {Set}[T^{\mathrm{ec}}]$
is atomic; -
(iii) every model of $T^{\mathrm{ec}}$
is atomic.
We deduce the result by using the characterisation of countably categorical coherent theories [Reference Haykazyan9, Theorem 6.5], which asserts that (iii) is satisfied if and only if T is countably categorical.
Corollary 9.8. Let T be a countably categorical coherent theory with JCP in a countable language. Then every infinitary full first-order formula in
$\mathcal {L}_{\infty , \omega }$
is
$T^{\mathrm{ec}}$
-provably equivalent to a geometric formula, modulo the deduction system for classical infinitary first-order logic.
Proof. By Theorem 9.7,
$\mathbf {Set}[T^{\mathrm{ec}}]$
is atomic, and hence Boolean. Therefore, the deducibility of infinitary first-order sequents modulo the deduction system for classical infinitary first-order logic coincides with validity in the generic model in
$\mathbf {Set}[T^{\mathrm{ec}}]$
(see [Reference Kamsma15, Theorem 5.14]). We conclude by noting that every subobject of the generic model in
$\mathbf {Set}[T^{\mathrm{ec}}]$
is the interpretation of some geometric formula.
Acknowledgments
We would like to thank our local research group (Ivan Tomašić, Behrang Noohi, Ming Ng, Luka Ilic, and Cameron Michie) at Queen Mary University of London, where we wrote this article, for the many useful discussions. We are also grateful for the anonymous reviewer’s helpful feedback and their suggestion of Example 4.11.
Funding statement
M.K. was supported by the EPSRC grant EP/X018997/1, and M.K. and J.W. were supported by EPSRC grant EP/V028812/1.
Open access
