Theory and Applications of Categories, Vol. 26, No. 6, 2012, pp. 176–193.

SYNTACTIC CHARACTERIZATIONS OF PROPERTIES OF CLASSIFYING TOPOSES

OLIVIA CARAMELLO

Abstract. We give characterizations, for various fragments of geometric logic, of the class of theories classified by a locally connected (respectively connected and locally connected, atomic, compact, presheaf) topos, and exploit the existence of multiple sites of definition for a given topos to establish various results on quotients of theories of presheaf type.

1. Introduction

Given the fact that Grothendieck toposes are ‘the same thing as’ Morita-equivalence classes of geometric theories, it is naturally of interest to investigate how classical topostheoretic properties of toposes translate into logical properties of the theories they classify.

Characterizations of the class of geometric theories classified by a Boolean (respectively De Morgan) topos have been provided in [Caramello, 2009a]. In section 3 of this paper, we provide syntactic characterizations, for various fragments of geometric logic, of the class of theories classified by a locally connected (respectively connected and locally connected, atomic, compact, presheaf) topos. Also, we establish criteria for a geometric theory over a given signature to be cartesian (respectively regular, coherent).

In section 4, given a quotient 𝕋′ of a theory of presheaf type 𝕋 corresponding to a Grothen- -dieck topology J on the opposite of the category of finitely presentable 𝕋-models via the duality of [Caramello, 2009c], we discuss how ‘geometrical’ properties of J translate into syntactic properties of 𝕋′. In this context, we also show that, given a theory of presheaf type 𝕋, the finitely presentable 𝕋-models coincide with the finitely presented 𝕋-models, in such a way that the opposite of the category of finitely presentable models of 𝕋 is equivalent to a full subcategory of the syntactic category of 𝕋. This generalizes the well-known result for finitary algebraic (or more generally, cartesian) theories.

SYNTACTIC CHARACTERIZATIONS OF PROPERTIES OF CLASSIFYING TOPOSES 177

Our technique to establish these latter results is to transfer topos-theoretic invariants (that is, properties of objects of toposes which are stable under topos-theoretic equivalence) from one site of definition of a given topos to another, according to the principles introduced in [Caramello, 2010]. This paper thus represents a natural companion to [Caramello, 2009c] and [Caramello, 2009b], where subtoposes and universal models are investigated in particular in the context of theories of presheaf type.

Received by the editors 2011-06-20 and, in revised form, 2012-02-29.

Transmitted by Jiri Rosicky. Published on 2012-03-06.

2000 Mathematics Subject Classification: 03G30, 18C10, 18B25.

Key words and phrases: Grothendieck topos, site characterizations, geometric logic, presheaf topos.

\begin{matrix}c \\ ◯ \end{matrix} Olivia Caramello, 2012. Permission to copy for private use granted.

The terminology used in the paper is borrowed from [Johnstone, 2002a] and [Johnstone, 2002b], if not otherwise stated. Our notion of site is that of a small Grothendieck site; anyway, all the results on sites established in the paper can be (trivially) extended to essentially small sites of the form (C, J) where C is an essentially small category.

2. Some geometric invariants

Let us start with some general facts about dense subcategories. We recall from [Johnstone, 2002b] the following definition.

2.1. Definition. Let (C, J) be a site. We say a subcategory D of C is J-dense if

(a) every object c of C has a covering sieve R ∈ J(c) generated by morphisms whose domains are in D; and

(b) for any morphism f : c → d in C with d ∈ D, there is a covering sieve R ∈ J(c) generated by morphisms g : b → c for which the composite f ∘ g is in D.

Let us denote by 𝔊𝔯𝔬𝔱𝔥(C) the Heyting algebra of Grothendieck topologies on a category C (cfr. [Caramello, 2009c]). Given a subcategory C′ of C, we denote by 𝔊𝔯𝔬𝔱𝔥_{C′}(C) the subset of 𝔊𝔯𝔬𝔱𝔥(C) formed by the Grothendieck topologies J on C such that C′ is J-dense.

There is an obvious notion of intersection of subcategories; specifically, given a collection {C_{i} — i ∈ I} of subcategories of a category C, we can define their intersection C′ by putting ob(C′) = ∩_{i∈I}ob(C_{i}) and arr(C′) = ∩_{i∈I}arr(C_{i}), that is, given an arrow f : a → b in

C, f belongs to arr(C′) if and only if it belongs to arr(C_{i}) for every i ∈ I. It is immediate to see that C′ is a subcategory of C.

We note that, for any Grothendieck topology J on C, any finite intersection of subcategories of C which are J-dense is again J-dense; indeed, this easily follows from the fact that a finite intersection of J-covering sieves is again J-covering.

The following result provides a couple of useful facts about dense subcategories.

2.2. Proposition. Let C be a category. Then

(i) 𝔊𝔯𝔬𝔱𝔥_{C′}(C) is closed in 𝔊𝔯𝔬𝔱𝔥(C) under arbitrary (non-empty) intersections (that is, meets in 𝔊𝔯𝔬𝔱𝔥(C)) and under taking larger topologies, and hence it is an Heyting algebra inheriting the Heyting operations from 𝔊𝔯𝔬𝔱𝔥(C) whose maximal element is the maximal Grothendieck topology on C and minimal element is the intersection of all the topologies in 𝔊𝔯𝔬𝔱𝔥_{C′}(C);

(ii) Let C′ and C′′ subcategories of C such that C′ is a subcategory of C′′. Then C′ is J-dense if and only if C′ is J|_{C′′}-dense (as a subcategory of C′′) and C′′ is J-dense.

Proof. (i) The first assertion is obvious while the second easily follows from the fact that arbitrary (non-empty) unions of J-covering sieves are J-covering.

(ii) Suppose that C′ is J-dense. Then, by part (i) of the proposition, C′′ is J-dense, and it is immediate to see that C′ is J|_{C′′}-dense (as a subcategory of C′′). The converse follows from the fact that ‘composition’ of J-covering sieves (in the sense of Definition 2.3 [Caramello, 2009c]) is J-covering.

We note that a small full subcategory of a Grothendieck topos E is J_{E}-dense, where J_{E} is the canonical Grothendieck topology on E, if and only if it is a separating set for E.

Let us also recall the following notions.

2.3. Definition. Let E be a Grothendieck topos and A an object of E. Then

(a) A is said to be an atom if the only subobjects of A in E are the identity on A and the zero subobject, and they are distinct from each other;

(b) A is said to be indecomposable if does not admit any non-trivial coproduct decompositions;

(c) A is said to be irreducible if it is J_{E}-irreducible, where J_{E} is the canonical topology on E; in other words, if any sieve in E containing a small epimorphic family contains the identity on A;

(d) A is said to be compact if every small covering family {A_{i} → A — i ∈ I} contains a finite covering subfamily;

(e) A is said to be coherent if it is compact and, whenever we are given a morphism f : B → A with B compact, the domain of the kernel-pair of f is compact;

(f) A is said to be supercompact if every small covering family {A_{i} → A — i ∈ I} contains a cover;

(g) A is said to be regular if it is supercompact and, whenever we are given a morphism f : B → A with B supercompact, the domain of the kernel-pair of f is supercompact.

Recall that an object in a locally connected topos is indecomposable if and only if it is connected (cfr. the discussion after the proof of Lemma C3.3.6 [Johnstone, 2002b]).

2.4. Remark. It readily follows from the definitions that every coherent (respectively regular) object is compact (respectively supercompact), every atom is an indecomposable object, every irreducible object is supercompact, every supercompact object is indecomposable.

Let us recall from [Johnstone, 2002b] the following terminology.

A site (C, J) is said to be locally connected if every J-covering sieve is connected, that is, for any R ∈ J(c), R is connected as a full subcategory of C/c.

A site (C, J) is said to be atomic if C satisfies the right Ore condition and J is the atomic topology on C.

Given a site (C, J), (a) we say an object c of C is J-irreducible if the only J-covering sieve on c is the maximal

sieve M(c);

(b) we say J is rigid if, for every c ∈ C, the family of all morphisms from J-irreducible objects to c generates a J-covering sieve.

A site (C, J) is said to be rigid if J is rigid as a Grothendieck topology on C.

We will say that a site (C, J) is coherent (respectively regular) if C is cartesian and J is a finite-type Grothendieck topology on C (respectively a Grothendieck topology J such that every J-covering sieve is generated by a single arrow).

Given a site (C, J), we denote by l_{J}^{C} : C → Sh(C, J) the composite of the Yoneda embedding C → [C^{op}, Set] with the associated sheaf functor a_{J} : [C^{op}, Set] → Sh(C, J). We have the following result.

2.5. Proposition. Let (C, J) be a site. Then

(i) if (C, J) is locally connected then for each c ∈ C, l_{J}^{C}(c) is an indecomposable (equivalently, connected) object in Sh(C, J);

(ii) if (C, J) is atomic then for each c ∈ C, l_{J}^{C}(c) is an atom in Sh(C, J);

(iii) if (C, J) is rigid then for each c ∈ C such that c is J-irreducible, l_{J}^{C}(c) is an indecomposable projective (equivalently, an irreducible object) of Sh(C, J);

(iv) if (C, J) is coherent (respectively regular) then for each c ∈ C, l_{J}^{C}(c) is a coherent (respectively regular) object of Sh(C, J).

Proof. (i) and (ii) were proved in [Caramello, 2011].

To prove (iii), we note that if (C, J) is rigid then the Comparison Lemma yields Sh(C, J) ≃ [D^{op}, Set] where D is the full subcategory of C on the J-irreducible objects (cfr. the discussion after Definition C2.2.18 [Johnstone, 2002b]) and, under this equivalence, for each c ∈ D, l_{J}^{C}(d) corresponds to the representable y(d) : D^{op} → Set. Now, it is well-known that all the representables on D are indecomposable projective objects in [D^{op}, Set], from which our thesis follows.

Part (iv) was proved in [Johnstone, 2002b] (cfr. Theorem D3.3.7 and Remark D3.3.10).

We note that if E is equivalent to a presheaf topos then any object of E is irreducible if and only if it is indecomposable and projective. Indeed, by the argument in the proof of Lemma C2.2.20 [Johnstone, 2002b], any indecomposable projective object in E is irreducible. Conversely, if G is the full subcategory of E on the irreducible objects then, by Lemma C2.2.20, G is essentially small and (G, J_{E}|_{G}) is a rigid site; moreover, by the Comparison Lemma E ≃ Sh(G, J_{E}|_{G}) and hence Proposition 2.5(iii) implies our thesis.

Let us recall from [Johnstone, 2002b] (C2.3.2(c)) that, for any essentially small site (C, J), a sieve R on l_{J}^{C}(c) in Sh(C, J) is epimorphic iff the sieve {f : d → c — l_{J}^{C}(f) ∈ R} is J-covering in C. This fact enables us to express properties of objects of the form l_{J}^{C}(c) like compactness, supercompactness or irreducibility in terms of properties of J-covering sieves on c, as follows (point (i) of the following proposition was proved in [Johnstone, 2002b] as Lemma D3.3.4).

2.6. Proposition. Let (C, J) be a site. Then, with the notation above, we have:

(i) l_{J}^{C}(c) is compact if and only if every J-covering sieve on c contains a finite family of arrows which generates a J-covering sieve;

(ii) l_{J}^{C}(c) is supercompact if and only if every J-covering sieve on c contains a single arrow which generates a J-covering sieve;

(iii) l_{J}^{C}(c) is irreducible if and only if every J-covering sieve on c is maximal, that is, c is J-irreducible.

It turns out that one can rephrase many interesting properties of Grothendieck toposes in terms of the existence of separating sets for them with particular properties. For example, it is well-known (cfr. Lemma C2.2.20 [Johnstone, 2002b]) that a Grothendieck topos is equivalent to a presheaf topos if and only if it has a separating set of indecomposable projective objects; moreover, we have the following characterizations.

2.7. Theorem. Let E be a Grothendieck topos. Then

(i) E is locally connected if and only if it has a separating set of indecomposable objects;

(ii) E is connected and locally connected if and only if it has a separating set of indecomposable objects containing the terminal object of E;

(iii) E is atomic if and only if it has a separating set of atoms;

(iv) E is coherent (respectively regular) if and only if it has a separating set of coherent (respectively regular) objects which is closed in E under finite limits.

Proof. (i) Suppose that E is locally connected; then, by Theorem C3.3.10 [Johnstone, 2002b], E is of the form Sh(C, J) for a locally connected small site (C, J). Then the objects of the form l_{J}^{C}(c) for c ∈ C are indecomposable (by Proposition 2.5(i)) and hence they form a separating set for E. Conversely, suppose that E has a separating set of indecomposable objects; then, by arguing as in the proof of Theorem C3.3.10 [Johnstone, 2002b], we obtain that the full subcategory I of E on the indecomposable objects, equipped with the Grothendieck topology J_{E}|_{I} on I induced by the canonical coverage on E is a locally connected site; but, by the Comparison Lemma, E is equivalent to Sh(I, J_{E}|_{I}), so that the thesis follows from Theorem C3.3.10 [Johnstone, 2002b].

(ii) This follows analogously to part (i), by using the ‘connected and locally connected’ version of Theorem C3.3.10 [Johnstone, 2002b].

(iii) This was already proved in [Caramello, 2011] (Proposition 1.3(i)).

(iv) One direction follows from Theorem D3.3.7 [Johnstone, 2002b] and Remarks D3.3.9 and D3.3.10 [Johnstone, 2002b]. Conversely, suppose that E has a separating set G of coherent (respectively regular) objects which is closed in E under finite limits. Then G is a cartesian category and, by the Comparison Lemma, E is equivalent to Sh(G, J_{E}|_{G}); now, by Proposition 2.6(i) (respectively Proposition 2.6(ii)), the site (G, J_{E}|_{G}) is coherent (respectively regular), and hence, by Theorem D3.3.1 [Johnstone, 2002b], E is a coherent (respectively regular) topos, as required.

2.8. Remark. Notice that it follows from the theorem and Remark 2.4 that any presheaf topos is locally connected, any regular topos is locally connected and any atomic topos is locally connected. Moreover, it is clear that if E is a Boolean topos then for any object A of E, A is an atom if and only if it is non-zero and indecomposable, from which it follows that any Boolean locally connected topos is atomic.

2.9. Remark. We note that the theorem implies that, given a site (C, J), if all the objects of the form l_{J}^{C}(c) for c ∈ C are indecomposable objects (respectively atoms) of Sh(C, J) then the topos Sh(C, J) is locally connected (respectively atomic). Also, provided that C is cartesian, if all the objects of the form l_{J}^{C}(c) for c ∈ C are regular (respectively coherent) in Sh(C, J) then the topos Sh(C, J) is regular (respectively coherent). An application of this remark in the context of quotients of theories of presheaf type will be provided in section 4 below.

3. Syntactic criteria

Let 𝕋 be a cartesian (respectively regular, coherent, geometric) theory over a signature Σ. We denote by C_{𝕋}^{cart} (respectively C_{𝕋}^{reg}, C_{𝕋}^{coh}, C_{𝕋}^{geom}) the cartesian (respectively regular, coherent, geometric) syntactic category of 𝕋 and by J_{𝕋}^{reg} the regular (respectively coherent, geometric) topology on C_{𝕋}^{reg} (respectively C_{𝕋}^{coh}, C_{𝕋}^{geom}). Recall from [Johnstone, 2002b] that if 𝕋 is cartesian (respectively regular, coherent, geometric) then [C_{𝕋}^{cart}^{op}, Set] (respectively Sh(C_{𝕋}^{reg}, J_{𝕋}^{reg}), Sh(C_{𝕋}^{coh}, J_{𝕋}^{coh}), Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom})) is a classifying topos for 𝕋. Let us denote by y_{𝕋}^{cart} : C_{𝕋}^{cart} → [C_{𝕋}^{cart}^{op}, Set] (respectively y_{𝕋}^{reg} : C_{𝕋}^{reg} → Sh(C_{𝕋}^{reg}, J_{𝕋}^{reg}), y_{𝕋}^{coh} : C_{𝕋}^{coh} → Sh(C_{𝕋}^{coh}, J_{𝕋}^{coh}), y_{𝕋}^{geom} : C_{𝕋}^{geom} → Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom})) the Yoneda embeddings.

Let us introduce the following notions. Below, by a 𝕋-provably functional geometric formula from {x⃗.ϕ} to {y⃗.ψ} we mean a geometric formula θ(x⃗, y⃗) such that the sequents (ϕ ⊢x⃗ (∃y⃗)θ), (θ ⊢_{x⃗,y⃗} ϕ ∧ ψ) and (θ ∧ θ[z⃗/y⃗] ⊢_{x⃗,y⃗,z⃗} y⃗ = z⃗) are provable in 𝕋.

3.1. Definition. Let 𝕋 be a geometric theory over a signature Σ and ϕ(x⃗) a geometric formula-in-context over Σ. Then

(a) we say that ϕ(x⃗) is 𝕋-complete if the sequent (ϕ ⊢x⃗ ⊥) is not provable in 𝕋, and for every geometric formula ϕ in the same context either (χ ⊢x⃗ ⊥) or (χ ∧ ϕ ⊢x⃗ ⊥) is provable in 𝕋;

(b) we say that ϕ(x⃗) is 𝕋-indecomposable if for any family {ψ_{i}(x⃗) — i ∈ I} of geometric formulae in the same context such that for each i, ψ_{i} 𝕋-provably implies ϕ and for any distinct i, j ∈ I, ψ_{i} ∧ ψ_{j} ⊢x⃗ ⊥ is provable in 𝕋, we have that ϕ ⊢x⃗ ∨_{i∈I}ψ_{i} provable in 𝕋 implies ϕ ⊢x⃗ ψ_{i} provable in 𝕋 for some i ∈ I;

(c) we say that ϕ(x⃗) is 𝕋-irreducible if for any family {θ_{i} — i ∈ I} of 𝕋-provably functional geometric formulae {x⃗_{i}, x⃗.θ_{i}} from {x⃗_{i}.ϕ_{i}} to {x⃗.ϕ} such that ϕ ⊢x⃗ ∨_{i∈I}(∃x⃗_{i})θ_{i} is provable in 𝕋, there exist i ∈ I and a 𝕋-provably functional geometric formula {x⃗, x⃗_{i}.θ′} from {x⃗.ϕ} to {x⃗_{i}.ϕ_{i}} such that ϕ ⊢x⃗ (∃x⃗_{i})(θ′ ∧ θ_{i}) is provable in 𝕋;

(d) we say that ϕ(x⃗) is 𝕋-compact if for any family {ψ_{i}(x⃗) — i ∈ I} of geometric formulae in the same context, ϕ ⊢x⃗ ∨_{i∈I}ψ_{i} provable in 𝕋 implies ϕ ⊢x⃗ ∨_{i∈I′}ψ_{i} provable in 𝕋 for

some finite subset I′ of I;

(e) we say that ϕ(x⃗) is 𝕋-supercompact if for any family {ψ_{i}(x⃗) — i ∈ I} of geometric formulae in the same context, ϕ ⊢x⃗ ∨_{i∈I}ψ_{i} provable in 𝕋 implies ϕ ⊢x⃗ ψ_{i} provable in 𝕋 for some i ∈ I.

3.2. Lemma. Let 𝕋 be a geometric theory over a signature Σ and ϕ(x⃗) a geometric formula-in-context over Σ. Then

(i) ϕ(x⃗) is 𝕋-complete if and only if y_{𝕋}^{geom}({x⃗.ϕ}) is an atom of Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom});

(ii) ϕ(x⃗) is 𝕋-indecomposable if and only if y_{𝕋}^{geom}({x⃗.ϕ}) is an indecomposable object of Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom});

(iii) ϕ(x⃗) is 𝕋-irreducible if and only if y_{𝕋}^{geom}({x⃗.ϕ}) is an irreducible object of Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom});

(iv) ϕ(x⃗) is 𝕋-compact if and only if y_{𝕋}^{geom}({x⃗.ϕ}) is a compact object of Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom});

(v) ϕ(x⃗) is 𝕋-supercompact if and only if y_{𝕋}^{geom}({x⃗.ϕ}) is a supercompact object of Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom}).

Proof. Parts (iii), (iv) and (v) follow immediately from Proposition 2.6, by using Lemma D1.4.4(iv) [Johnstone, 2002b] and the fact that cover-mono factorizations of arrow exist in C_{𝕋}^{geom}.

Parts (i) and (ii) follow from the fact that in a topos coproducts are the same thing as disjoint unions, since y_{𝕋}^{geom}(C_{𝕋}^{geom}) is closed in Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom}) under taking subobjects and y_{𝕋}^{geom} : C_{𝕋}^{geom} → Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom}) is a full and faithful geometric functor.

Recall from [Johnstone, 2002b] that a Grothendieck topos E is compact if and only if the terminal object of E is compact; hence, a geometric theory 𝕋 over a signature Σ is classified by a compact topos if and only if y_{𝕋}^{geom}({[].⊤}) is compact in Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom}), if and only if for any family {ψ_{i} — i ∈ I} of geometric sentences, ϕ ⊢ ∨_{i∈I}ψ_{i} provable in

𝕋 implies ϕ ⊢ ∨_{i∈I′}ψ_{i} provable in 𝕋 for some finite subset I′ of I.

We note that any cartesian (respectively regular, coherent) theory 𝕋 over a signature Σ can be regarded as a geometric theory, and hence we have an equivalence of classifying toposes

[C_{𝕋}^{cart}^{op}, Set] ≃ Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom})

(respectively

Sh(C_{𝕋}^{reg}, J_{𝕋}^{reg}) ≃ Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom}),
Sh(C_{𝕋}^{coh}, J_{𝕋}^{coh}) ≃ Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom})).

Moreover, it is immediate to see that for any cartesian (respectively regular, coherent) formula ϕ(x⃗) over Σ, y_{𝕋}^{cart}({x⃗.ϕ}) (respectively y_{𝕋}^{reg}({x⃗.ϕ}), y_{𝕋}^{coh}({x⃗.ϕ})) corresponds under the equivalence to y_{𝕋}^{geom}({x⃗.ϕ}).

This remark, combined with Propositions 2.5 and 2.6, leads to the following results. Below, given a geometric theory 𝕋 over a signature Σ, by saying that 𝕋 is equivalent to a cartesian (respectively regular, coherent) theory we mean that 𝕋 can be axiomatized by cartesian (respectively regular, coherent) sequents over Σ.

3.3. Theorem. Let 𝕋 be a geometric theory over a signature Σ. Then 𝕋 is equivalent to a cartesian theory if and only if for any cartesian formula {x⃗.ϕ} over Σ, for any family {θ_{i} — i ∈ I} of 𝕋-provably functional geometric formulae {x⃗_{i}, x⃗.θ_{i}} from {x⃗_{i}.ϕ_{i}} to {x⃗.ϕ} such that ϕ ⊢x⃗ ∨_{i∈I}(∃x⃗_{i})θ_{i} is provable in 𝕋, there exist i ∈ I and a 𝕋-provably functional

geometric formula {x⃗, x⃗_{i}.θ′} from {x⃗.ϕ} to {x⃗_{i}.ϕ_{i}} such that ϕ ⊢x⃗ (∃x⃗_{i})(θ′ ∧ θ_{i}) is provable in 𝕋.

Proof. Let us suppose that 𝕋 is cartesian. Then the property of {x⃗.ϕ} in the statement of the proposition is equivalent, by Lemma 3.2(iii), to saying that y_{𝕋}^{geom}({x⃗.ϕ}) is irreducible in Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom}). But this condition corresponds, under the equivalence

[C_{𝕋}^{cart}^{op}, Set] ≃ Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom}),

to saying that y_{𝕋}^{cart}({x⃗.ϕ}) is irreducible (equivalently, indecomposable projective) in the topos [C_{𝕋}^{cart}^{op}, Set], and this true (cfr. Proposition 2.5(iii)).

Conversely, if 𝕋 is geometric and for any cartesian formula ϕ(x⃗) over Σ, y_{𝕋}^{geom}({x⃗.ϕ}) is irreducible in Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom}) then, denoted by G the full subcategory of C_{𝕋}^{geom} on the cartesian formulae, equivalently the cartesian syntactic category C_{𝕋′}^{cart} of the cartesianization 𝕋′ of 𝕋 (that is, the theory axiomatized by all the cartesian sequents over Σ which are provable in 𝕋), we have that G is J_{𝕋}^{geom}-dense (by Lemma D1.3.8 [Johnstone, 2002b]) and J_{𝕋}^{geom}|_{G} is the trivial Grothendieck topology. Thus the Comparison Lemma yields an equivalence

Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom}) ≃ [C_{𝕋′}^{cart}^{op}, Set].

Clearly, this equivalence sends the universal model of 𝕋 in Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom}) to the universal model of 𝕋′ in [C_{𝕋′}^{cart}^{op}, Set], and hence, universal models being conservative, 𝕋 and 𝕋′ prove exactly the same geometric sequents over Σ, that is, they are equivalent, as required.

The ‘only if’ direction in the following result extends Lemma D3.3.11 [Johnstone, 2002b].

3.4. Theorem. Let 𝕋 be a geometric theory over a signature Σ. Then 𝕋 is equivalent to a regular theory if and only if for any regular formula {x⃗.ϕ} over Σ, for any family {ψ_{i}(x⃗) — i ∈ I} of geometric formulae in the same context, ϕ ⊢x⃗ ∨_{i∈I}ψ_{i} provable in 𝕋 implies ϕ ⊢x⃗ ψ_{i} provable in 𝕋 for some i ∈ I.

Proof. This follows similarly to Theorem 3.3 by using Lemma 3.2(v) and Proposition 2.5(iv).

3.5. Theorem. Let 𝕋 be a geometric theory over a signature Σ. Then 𝕋 is equivalent to a coherent theory if and only if for any coherent formula {x⃗.ϕ} over Σ, for any family {ψ_{i}(x⃗) — i ∈ I} of geometric formulae in the same context, ϕ ⊢x⃗ ∨_{i∈I}ψ_{i} provable in 𝕋

implies ϕ ⊢x⃗ ∨_{i∈I′}ψ_{i} provable in 𝕋 for some finite subset I′ of I.

Proof. This follows similarly to Theorem 3.3 by using Lemma 3.2(iv) and Proposition 2.5(iv).

3.6. Locally connected theories The following result gives a syntactic characterization of the class of geometric theories classified by a locally connected (respectively connected and locally connected) topos.

3.7. Theorem. Let 𝕋 be a geometric theory over a signature Σ. Then 𝕋 is classified by a locally connected topos (respectively connected and locally connected topos) if and only if for any geometric formula ϕ(x⃗) over Σ there exists a (unique) family {ψ_{i}(x⃗) — i ∈ I} of 𝕋-indecomposable geometric formulae in the same context (respectively, containing {[].⊤}) such that

(i) for each i, ψ_{i} 𝕋-provably implies ϕ,

(ii) for any distinct i, j ∈ I, ψ_{i} ∧ ψ_{j} ⊢x⃗ ⊥ is provable in 𝕋, and

(iii) ϕ ⊢x⃗ ∨_{i∈I}ψ_{i} is provable in 𝕋.

Proof. Let us suppose that the classifying topos Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom}) of 𝕋 is locally connected. Then, by Lemma D3.3.6 [Johnstone, 2002b], given a geometric formula ϕ(x⃗) over Σ, the object y_{𝕋}^{geom}({x⃗.ϕ}) of the topos Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom}) is uniquely expressible as a coproduct of indecomposable objects. Now, since y_{𝕋}^{geom}(C_{𝕋}^{geom}) is closed in Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom}) under taking subobjects (the topos Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom}) being the ∞-pretopos completion of C_{𝕋}^{geom}), we can suppose that all the subobjects of y_{𝕋}^{geom}({x⃗.ϕ}) in Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom}), and in particular the indecomposable objects arising in our coproduct, are of the form y_{𝕋}^{geom}(c) for some c ∈ C_{𝕋}^{geom}. The condition of the criterion then follows from Lemma 3.2(ii) and the fact that the functor y_{𝕋}^{geom} is geometric and full and faithful.

Conversely, if the condition of the criterion is satisfied then we have, by Lemma 3.2(ii) and Proposition 2.2(ii), that the objects of the form y_{𝕋}^{geom}({y⃗.ψ}) for a 𝕋-indecomposable formula ψ(y⃗) form a separating set for Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom}) made of indecomposable objects; then Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom}) is locally connected by Theorem 2.7(i).

The following result is the coherent analogue of this theorem.

3.8. Theorem. Let 𝕋 be a coherent theory over a signature Σ. Then 𝕋 is classified by a locally connected topos (respectively connected and locally connected topos) if and only if for any coherent formula ϕ(x⃗) over Σ there exists a (unique) finite family {ψ_{i}(x⃗) — i ∈ I} of 𝕋-indecomposable geometric formulae in the same context (resp. containing {[].⊤}) such that

(i) for each i, ψ_{i} 𝕋-provably implies ϕ,

(ii) for any distinct i, j ∈ I, ψ_{i} ∧ ψ_{j} ⊢x⃗ ⊥ is provable in 𝕋, and

(iii) ϕ ⊢x⃗ ∨_{i∈I}ψ_{i} is provable in 𝕋.

Proof. The proof proceeds analogously to the proof of Theorem 3.7, by using Theorem 3.5.

3.9. Remark. From the proof of the theorems it is clear that, by using the notion of dense subcategory, one can obtain alternative (although equivalent) versions of the criteria. For example, a weaker (in the ‘if’ direction) version of the criterion of Theorem 3.7 reads as follows: a geometric theory 𝕋 is classified by a locally connected topos (respectively connected and locally connected topos) if and only if there exists a collection F (respectively, a collection F containing {[].⊤}) of 𝕋-indecomposable geometric formulaein-context over Σ such that for any geometric formula {y⃗.ψ} over Σ, there exist objects {x⃗_{i}.ϕ_{i}} in F as i varies in I and 𝕋-provably functional geometric formulae {x⃗_{i}, y⃗.θ_{i}} from {x⃗_{i}.ϕ_{i}} to {y⃗.ψ} such that ψ ⊢y⃗ ∨_{i∈I}(∃x⃗_{i})θ_{i} is provable in 𝕋. Naturally, the ‘coherent’ version of this criterion also holds.

We note that, by Theorem 3.5, if 𝕋 is coherent and ϕ(x⃗) is a coherent formula over Σ then ϕ(x⃗) is 𝕋-indecomposable if and only if for any finite family {ψ_{i}(x⃗) — i ∈ I} of geometric formulae in the same context such that for each i, ψ_{i} 𝕋-provably implies ϕ and for any distinct i, j ∈ I, ψ_{i} ∧ ψ_{j} ⊢x⃗ ⊥ is provable in 𝕋, we have that ϕ ⊢x⃗ ∨_{i∈I}ψ_{i} provable in 𝕋 implies ϕ ⊢x⃗ ψ_{i} provable in 𝕋 for some i ∈ I.

Regarding regular theories, their classifying toposes are always connected and locally connected; this was already observed in [Johnstone, 2002b], and also follows from our Remark 2.4.

We have already noticed that any atomic topos E is locally connected; in fact, as it is observed in [Johnstone, 2002b], the atoms of E are exactly the connected (equivalently, indecomposable) objects of E. Hence, in view of Theorem 2.7, by replacing ‘𝕋indecomposable’ with ‘𝕋-complete’ everywhere in the criteria above, one obtains syntactic criteria for a geometric (respectively coherent) theory to be classified by an atomic topos; also, one can obtain alternative versions of these criteria in the same spirit as in Remark 3.9.

Concerning atomic toposes, let us notice that if ϕ(x⃗) is a 𝕋-complete formula then ϕ(x⃗) is 𝕋-provably equivalent to a regular formula; indeed, this follows immediately from the fact that any geometric formula is provably equivalent to a disjunction of regular formulae (Lemma D1.3.8 [Johnstone, 2002b]).

We can give the following criterion for a regular theory to be classified by an atomic topos.

3.10. Proposition. Let 𝕋 be a regular theory over a signature Σ. Then 𝕋 is classified by an atomic topos if and only if every regular formula over Σ is either 𝕋-provably equivalent to ⊥ or 𝕋-complete.

Proof. Let ϕ(x⃗) be a regular formula over Σ. If 𝕋 is classified by an atomic topos then, by the discussion above, ϕ is expressible as a disjunction of 𝕋-complete regular formulae; but this implies, by Theorem 3.4, that either ϕ is 𝕋-provably equivalent to ⊥ or it is 𝕋-provably equivalent to one of these formulae and hence 𝕋-complete.

Conversely, if every regular formula over Σ is either 𝕋-provably equivalent to ⊥ or 𝕋complete then, by Lemma 3.2 and the fact that the set of objects of the form y_{𝕋}^{reg}({x⃗.ϕ}) for a regular formula ϕ(x⃗) over Σ form a separating set for the classifying topos Sh(C_{𝕋}^{reg}, J_{𝕋}^{reg}) of 𝕋, we have that Sh(C_{𝕋}^{reg}, J_{𝕋}^{reg}) of 𝕋 has a separating set of atoms and hence, by Theorem 2.7(iii), it is atomic, as required.

In passing, we note an interesting property of theories classified by atomic toposes.

3.11. Theorem. Let 𝕋 be a regular (respectively coherent) theory over a signature Σ which is classified by an atomic (equivalently, Boolean) topos. Then every geometric formula over Σ is 𝕋-provably equivalent to a regular (respectively coherent) formula over Σ.

Proof. Let ϕ(x⃗) be a geometric formula over Σ. Then, the classifying topos of 𝕋 being Boolean, ⊤ ⊢x⃗ ϕ(x⃗) ∨ ¬^{𝕋}ϕ(x⃗) is provable in 𝕋 (where ¬^{𝕋}ϕ(x⃗) denotes the pseudocomplementation of ϕ(x⃗) in Sub_{C_{𝕋}^{geom}}({x⃗.⊤}) as in [Caramello, 2009b]). But, by Theorem 3.4, ⊤(x⃗) is 𝕋-supercompact (respectively 𝕋-compact) and, since by Lemma D1.3.8 [Johnstone, 2002b] ϕ(x⃗) is (𝕋-)provably equivalent to a disjunction of regular formulae, it thus follows that ϕ(x⃗) is 𝕋-provably equivalent to a single regular formula (respectively a finite disjunction of regular formulae), as required.

3.12. Theories of presheaf type In this section we give a characterization of the class of geometric (respectively coherent, regular) theories classified by a presheaf topos. We recall that a theory classified by a presheaf topos is said to be of presheaf type.

Below, for a subcanonical site (C, J), we denote by y : C → Sh(C, J) the factorization through Sh(C, J) ↪ [C^{op}, Set] of the Yoneda embedding.

3.13. Theorem. Let (C, J) be a subcanonical site such that y(C) is closed in Sh(C, J) under retracts. Then Sh(C, J) is equivalent to a presheaf topos if and only if J is rigid.

Proof. The ‘if’ direction follows at once from the Comparison Lemma. Let us then prove the ‘only if’ direction. If E = Sh(C, J) is equivalent to a presheaf topos then, by Lemma C2.2.20 [Johnstone, 2002b], E has a separating set of indecomposable projective objects. Now, suppose A is an indecomposable projective in E. Then, as it is observed in the proof of Lemma C2.2.20 [Johnstone, 2002b], given any epimorphic family {f_{i} : B_{i} → A — i ∈ I}, at least one f_{i} must be a split epimorphism; in particular A is J_{E}-irreducible, where J_{E} is the canonical coverage on E. Hence, by taking as epimorphic family the collection of all the arrows in E from objects of the form y(c) to A, we obtain that A is a retract in E of an object of the form y(c). Thus, by our hypotheses, A is itself, up to isomorphism, of the form y(c) for some c ∈ C. Let us denote by C′ the full subcategory of C on the objects c such that y(c) is indecomposable and projective in E; then the objects in y(C′) form a separating set for E. Thus, for any object B of E the family of all the arrows in E from objects of the form y(c) for c ∈ C′ to B generates a J_{E}-covering sieve. But, J being subcanonical, J = J_{E}|_{C} (by Proposition C2.2.16 [Johnstone, 2002b]) and hence for any object c ∈ C the collection of all arrows in C from objects of C′ to c is J-covering; so, by Proposition 2.6(iii), J is rigid.

3.14. Remark. We note that, under the hypotheses of the theorem, if C is Cauchycomplete (in particular if C is cartesian) then y(C) is closed in E = Sh(C, J) under retracts. Indeed, let i : A ↣ y(c), r : y(c) ↠ A be a retract of A in E, that is, r ∘ i = 1_{A}. Then i ∘ r : y(c) → y(c) is idempotent. Now, since y is full and faithful, i ∘ r = y(e) for some idempotent e : c → c in C. Since C is Cauchy complete then e splits as s ∘ t where t ∘ s = 1. Then y(s) and y(t) form a retract of A and hence, by the uniqueness up to isomorphism of the splitting of an idempotent in a category, it follows that r is isomorphic to y(t) and i is isomorphic to y(s), and in particular A is isomorphic to y(dom(s)).

By Remark 3.14, the regular (respectively coherent, geometric) syntactic sites for regular (respectively coherent, geometric) theories all satisfy the hypotheses of Theorem 3.13. Thus we obtain the following results.

3.15. Corollary. Let 𝕋 be a geometric theory over a signature Σ. Then 𝕋 is of presheaf type if and only if there exists a collection F of geometric formulae-in-context over Σ satisfying the following properties:

(i) for any geometric formula {y⃗.ψ} over Σ, there exist objects {x⃗_{i}.ϕ_{i}} in F as i varies in I and 𝕋-provably functional geometric formulae {x⃗_{i}, y⃗.θ_{i}} from {x⃗_{i}.ϕ_{i}} to {y⃗.ψ} such that ψ ⊢y⃗ ∨_{i∈I}(∃x⃗_{i})θ_{i} is provable in 𝕋;

(ii) for any formula {x⃗.ϕ} in F, for any family {θ_{i} — i ∈ I} of 𝕋-provably functional geometric formulae {x⃗_{i}, x⃗.θ_{i}} from {x⃗_{i}.ϕ_{i}} to {x⃗.ϕ} such that ϕ ⊢x⃗ ∨_{i∈I}(∃x⃗_{i})θ_{i} is provable in 𝕋, there exist i ∈ I and a 𝕋-provably functional geometric formula {x⃗, x⃗_{i}.θ′} from {x⃗.ϕ} to {x⃗_{i}.ϕ_{i}} such that ϕ ⊢x⃗ (∃x⃗_{i})(θ′ ∧ θ_{i}) is provable in 𝕋.

Note that condition (ii) in the corollary says precisely that {x⃗.ϕ} is 𝕋-irreducible; in particular, {x⃗.ϕ} is 𝕋-supercompact, that is, for any family {{x⃗.ϕ_{i}} — i ∈ I} of geometric formulae in the same context which 𝕋-provably imply {x⃗.ϕ} and such that ϕ ⊢x⃗ ∨_{i∈I}ϕ_{i} is provable in 𝕋, there exists i ∈ I such that ϕ_{i} and ϕ are 𝕋-provably equivalent.

The following results are the coherent and regular analogues of this corollary.

3.16. Corollary. Let 𝕋 be a coherent theory over a signature Σ. Then 𝕋 is of presheaf type if and only if there exists a collection F of coherent formulae-in-context over Σ satisfying the following properties:

(i) for any coherent formula {y⃗.ψ} over Σ, there exists a finite number of objects {x⃗_{i}.ϕ_{i}} in F as i varies in I and 𝕋-provably functional coherent formulae {x⃗_{i}, y⃗.θ_{i}} from

{x⃗_{i}.ϕ_{i}} to {y⃗.ψ} such that ψ ⊢y⃗ ∨_{i∈I}(∃x⃗_{i})θ_{i} is provable in 𝕋;

(ii) for any formula {x⃗.ϕ} in F, for any finite family {θ_{i} — i ∈ I} of 𝕋-provably functional coherent formulae {x⃗_{i}, x⃗.θ_{i}} from {x⃗_{i}.ϕ_{i}} to {x⃗.ϕ} such that ϕ ⊢x⃗ ∨_{i∈I}(∃x⃗_{i})θ_{i} is provable in 𝕋, there exist i ∈ I and a 𝕋-provably functional coherent formula {x⃗, x⃗_{i}.θ′} from {x⃗.ϕ} to {x⃗_{i}.ϕ_{i}} such that ϕ ⊢x⃗ (∃x⃗_{i})(θ′ ∧ θ_{i}) is provable in 𝕋.

3.17. Corollary. Let 𝕋 be a regular theory over a signature Σ. Then 𝕋 is of presheaf type if and only if there exists a collection F of regular formulae-in-context over Σ satisfying the following properties:

(i) for any regular formula {y⃗.ψ} over Σ, there exists an object {x⃗.ϕ} in F and a 𝕋provably functional formula {x⃗, y⃗.θ} from {x⃗.ϕ} to {y⃗.ψ} such that ψ ⊢y⃗ (∃x⃗)θ is provable in 𝕋;

(ii) for any formula {y⃗.ψ} in F, for any 𝕋-provably functional regular formulae {x⃗, y⃗.θ} from {x⃗.ϕ} to {y⃗.ψ} such that ψ ⊢y⃗ (∃x⃗)θ is provable in 𝕋, there exist a 𝕋-provably functional regular formula {y⃗, x⃗.θ′} from {y⃗.ψ} to {x⃗.ϕ} such that ψ ⊢y⃗ (∃x⃗)(θ′ ∧ θ_{i}) is provable in 𝕋.

4. Syntactic properties of quotients of theories of presheaf type

Let 𝕋 be a theory of presheaf type over a signature Σ. Recall that a 𝕋-model M in Set is said to be finitely presentable if the representable functor Hom_{𝕋-mod(Set)}(M, −) : 𝕋-mod(Set) → Set preserves filtered colimits. The full subcategory of 𝕋-mod(Set) on the finitely presentable models will be denoted by f.p.𝕋-mod(Set).

A 𝕋-model M in Set is said to be finitely presented if there is a geometric formula {x⃗.ϕ} over Σ and a string of elements (ξ_{1}, …, ξ_{n}) ∈ MA_{1} × … × MA_{n} (where A_{1}, …, A_{n} are the sorts of the variables in x⃗), called the generators of M, such that for any 𝕋-model N in Set and string of elements (b_{1}, …, b_{n}) ∈ MA_{1} × … × MA_{n} such that (b_{1}, …, b_{n}) ∈ [[ϕ]]_{N}, there exists a unique arrow f : M → N in 𝕋-mod(Set) such that (fA_{1} × … × fA_{n})((ξ_{1}, …, ξ_{n})) = (b_{1}, …, b_{n}).

We recall from [Caramello, 2009b] that, given a theory of presheaf type 𝕋, a canonical Morita-equivalence for 𝕋 (in the sense of [Caramello, 2009b]) induces an equivalence of classifying toposes

[f.p.𝕋-mod(Set), Set] ≃ Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom})

sending the universal model M_{𝕋} of 𝕋 in the topos [f.p.𝕋-mod(Set), Set] to the universal model U_{𝕋} of 𝕋 in Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom}). Recall that M_{𝕋} is the 𝕋-model in [f.p.𝕋-Mod(Set), Set] which assigns to a sort A the functor M_{𝕋}A given by (M_{𝕋}A)(M) = MA, to a function symbol f : A_{1} ⋯ A_{n} → B the morphism M_{𝕋}A_{1} × ⋯ × M_{𝕋}A_{n} → M_{𝕋}B given by (M_{𝕋}f)(M) = Mf and to a relation symbol R ↣ A_{1} ⋯ A_{n} the subobject M_{𝕋}R ↣ M_{𝕋}A_{1} × ⋯ × M_{𝕋}A_{n} given by (M_{𝕋}R)(M) = MR (for any M ∈ f.p.𝕋-Mod(Set)), while U_{𝕋} is the image, under the Yoneda embedding y : C_{𝕋} ↪ Sh(C_{𝕋}, J_{𝕋}), of the ‘universal’ model M_{𝕋} of 𝕋 in C_{𝕋}, which assigns to a sort A the object {x^{A}.⊤} where x^{A} is a variable of sort A, to a function symbol f : A_{1} ⋯ A_{n} → B the morphism

\xymatrix{\{x_{1}, …, x_{n}.⊤\} \ar[r]^{[f(x_{1},...,x_{n})=y]} & \{y.⊤\}}

and to a relation symbol R ↣ A_{1} ⋯ A_{n} the subobject

\xymatrix{\{x_{1}, …, x_{n}.R(x_{1}, …, x_{n})\} \ar[r]^{[R(x_{1},...,x_{n})]} & \{x_{1}, …, x_{n}.⊤\}}

as in Lemma D1.4.4(iv) [Johnstone, 2002b].

As a consequence, if M ∈ f.p.𝕋-mod(Set) is a 𝕋-model presented by a formula ϕ(x⃗) over Σ then, denoted by y : f.p.𝕋-mod(Set)^{op} → [f.p.𝕋-mod(Set), Set] the Yoneda embedding, y(M) is equal to [[x⃗.ϕ]]_{M_{𝕋}} and hence corresponds, under the equivalence

[f.p.𝕋-mod(Set), Set] ≃ Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom}),

to the functor y_{𝕋}^{geom}({x⃗.ϕ}) = [[x⃗.ϕ]]_{U_{𝕋}}.

We recall that in [Caramello, 2009c] a bijection is established between the subtoposes of the classifying topos of a geometric theory 𝕋 and the quotients of 𝕋 (i.e., geometric extensions of 𝕋 over its signature), considered up to the obvious notion of syntactic equivalence (i.e. the equivalence which identifies two quotients of 𝕋 precisely when they prove the same geometric sequents over the signature of 𝕋); the subtopos corresponding via this duality to a given quotient of 𝕋 can be identified with its classifying topos (cf. Theorem 3.6 [Caramello, 2009c]).

Now, if 𝕋′ is a quotient of 𝕋 then the subtopos of Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom}) corresponding to it via this duality transfers via the equivalence

[f.p.𝕋-mod(Set), Set] ≃ Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom})

to a subtopos Sh(f.p.𝕋-mod(Set)^{op}, J) ↪ [f.p.𝕋-mod(Set), Set]

of [f.p.𝕋-mod(Set), Set]; the topology J will be called the associated 𝕋-topology of 𝕋′. This gives rise to an equivalence

Sh(f.p.𝕋-mod(Set)^{op}, J) ≃ Sh(C_{𝕋′}^{geom}, J_{𝕋′}^{geom})

of classifying toposes of 𝕋′ which sends l_{J}^{f.p.𝕋-mod(Set)^{op}}(M) to the functor y_{𝕋′}^{geom}({x⃗.ϕ}) = [[x⃗.ϕ]]_{U_{𝕋′}}.

The following result provides a link between ‘geometrical’ properties of J and syntactic properties of 𝕋′.

4.1. Theorem. Let 𝕋 be a theory of presheaf type over a signature Σ, 𝕋′ be a quotient of 𝕋 with associated 𝕋-topology J on f.p.𝕋-mod(Set)^{op} and ϕ(x⃗) be a geometric formula over Σ which presents a 𝕋-model M. Then

(i) ϕ(x⃗) is 𝕋-irreducible; in particular, ϕ(x⃗) is 𝕋-provably equivalent to a regular formula;

(ii) if the site (f.p.𝕋-mod(Set)^{op}, J) is locally connected (for example when f.p.𝕋-mod(Set)^{op} satisfies the right Ore condition and every J-covering sieve is non-empty) then ϕ(x⃗) is 𝕋′-indecomposable;

(iii) if f.p.𝕋-mod(Set)^{op} satisfies the right Ore condition and J is the atomic topology on f.p.𝕋-mod(Set)^{op} then ϕ(x⃗) is 𝕋′-complete;

(iv) if every J-covering sieve on M contains a J-covering sieve generated by a finite family of morphisms (respectively by a single morphism) then ϕ(x⃗) is 𝕋′-compact (respectively 𝕋′-supercompact).

Proof. (i) By Lemma 3.2(iii), ϕ(x⃗) is 𝕋-irreducible if and only if y_{𝕋}^{geom}({x⃗.ϕ}) is an irreducible object of Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom}). But, by the discussion above, this is equivalent to saying that y(M) is irreducible in [f.p.𝕋-mod(Set), Set], and this is is true by Proposition 2.5(iii). The fact that ϕ(x⃗) is 𝕋-provably equivalent to a regular formula then follows from Lemma D1.3.8(ii) [Johnstone, 2002b].

(ii) and (iii) By Lemma 3.2(ii) (respectively Lemma 3.2(i)), ϕ(x⃗) is 𝕋′-indecomposable (respectively 𝕋′-complete) if and only if y_{𝕋′}^{geom}({x⃗.ϕ}) is an indecomposable object (respectively an atom) of Sh(C_{𝕋′}^{geom}, J_{𝕋′}^{geom}); but this is equivalent to saying that l_{J}^{f.p.𝕋-mod(Set)^{op}}(M) is an indecomposable object (respectively an atom) of Sh(f.p.𝕋-mod(Set)^{op}, J), and this is true by Proposition 2.5(i) (respectively Proposition 2.5(ii)).

(iv) By Lemma 3.2(iii), ϕ(x⃗) is 𝕋′-compact (respectively 𝕋′-supercompact) if and only if y_{𝕋′}^{geom}({x⃗.ϕ}) is a compact (respectively supercompact) object of Sh(C_{𝕋′}^{geom}, J_{𝕋′}^{geom}); but this is equivalent to saying that l_{J}^{f.p.𝕋-mod(Set)^{op}}(M) is a compact (respectively supercompact) object of Sh(f.p.𝕋-mod(Set)^{op}, J), and this is true by Proposition 2.6(i) (respectively Proposition 2.6(ii)).

4.2. Remark. The theorem can be profitably applied in the context of cartesian theories. Indeed, if 𝕋 is a cartesian theory then every cartesian formula over Σ presents a 𝕋-model so that we have an equivalence between f.p.𝕋-mod(Set)^{op} and the cartesian syntactic category of 𝕋. Thus the theorem provides syntactic properties of cartesian formulae in particular quotients of 𝕋; for example, for any such formula ϕ(x⃗), part (iii) of the lemma yields that ϕ(x⃗) is 𝕋′-complete where 𝕋′ is the Booleanization of 𝕋 (as defined in [Caramello, 2009a]).

As an application of the notion of irreducible object in a topos, we can prove the following result.

4.3. Theorem. Let 𝕋 be a theory of presheaf type over a signature Σ. Then

(i) Any finitely presentable 𝕋-model in Set is presented by a 𝕋-irreducible geometric formula ϕ(x⃗) over Σ;

(ii) Conversely, any 𝕋-irreducible geometric formula ϕ(x⃗) over Σ presents a 𝕋-model.

In fact, the category f.p.𝕋-mod(Set)^{op} is equivalent to the full subcategory of C_{𝕋}^{geom} on the 𝕋-irreducible formulae.

Proof. We have already observed that we have an equivalence

τ : Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom}) ≃ [f.p.𝕋-mod(Set), Set]

of classifying toposes for 𝕋. Now, if C_{𝕋}^{irr} is the full subcategory of C_{𝕋}^{geom} on the 𝕋-irreducible formulae then, by Theorem 3.13, we have that Sh(C_{𝕋}^{geom}, J_{𝕋}^{geom}) ≃ [(C_{𝕋}^{irr})^{op}, Set] via the Comparison Lemma (cf. the proof of Theorem 2.5). Now, if C̃_{𝕋}^{irr} ↪ C_{𝕋}^{geom} is the Cauchycompletion of C_{𝕋}^{irr} then [(C_{𝕋}^{irr})^{op}, Set] ≃ [(C̃_{𝕋}^{irr})^{op}, Set] and the resulting equivalence

[C̃_{𝕋}^{irr}^{op}, Set] ≃ [f.p.𝕋-mod(Set), Set]

restricts to an equivalence

l : C̃_{𝕋}^{irr}^{op} ≃ f.p.𝕋-mod(Set)

between the subcategories of indecomposable projective objects. Now, given {x⃗.ϕ} ∈ C̃_{𝕋}^{irr}, τ sends the functor y_{𝕋}^{geom}({x⃗.ϕ}) = [[x⃗.ϕ]]_{U_{𝕋}} to y(l({x⃗.ϕ})) = [[x⃗.ϕ]]_{M_{𝕋}}, from which it follows that the model l({x⃗.ϕ}) is finitely presented by {x⃗.ϕ}. Then, by Theorem 4.1(i), ϕ(x⃗) is 𝕋-irreducible. So we conclude that C̃_{𝕋}^{irr} is equal to C_{𝕋}^{irr}, that is, C_{𝕋}^{irr} is Cauchy complete, and hence l gives an equivalence

C̃_{𝕋}^{irr}^{op} ≃ f.p.𝕋-mod(Set).

It is easy to verify that this equivalence coincide with the dualizing functor d of Theorem 3.6 [Caramello, 2009b].

4.4. Remark. As an application of Theorem 4.3 and Remark 2.9, suppose that J is the associated 𝕋-topology of a quotient 𝕋′ of 𝕋. Then, if for any 𝕋-irreducible formula (equivalently, formula presenting a 𝕋-model) ϕ(x⃗), ϕ(x⃗) is 𝕋′-indecomposable (respectively 𝕋′-complete) then the classifying topos Sh(f.p.𝕋-mod(Set)^{op}, J) of 𝕋′ is locally connected (respectively atomic); indeed, as observed above, ϕ(x⃗) is 𝕋′-indecomposable (respectively 𝕋′-atomic) if and only if y_{𝕋′}^{geom}({x⃗.ϕ}) is an indecomposable object (respectively an atom) of the topos Sh(C_{𝕋′}^{geom}, J_{𝕋′}^{geom}), if and only if l_{J}^{f.p.𝕋-mod(Set)^{op}}(M) is an indecomposable object (respectively an atom) of the topos Sh(f.p.𝕋-mod(Set)^{op}, J).

Acknowledgements: I am grateful to Peter Johnstone for useful discussions on the subject matter of this paper, and to the anonymous referee for his suggestions, which have helped improve the readability of this paper.

References

[Artin, Grothendieck and Verdier, 1972] M. Artin, A. Grothendieck and J. L. Verdier, Théorie des topos et cohomologie étale des schémas, Lecture Notes in Math., vols 269, 270 and 305 (Springer-Verlag, 1972).

[Caramello, 2011] O. Caramello, Atomic toposes and countable categoricity, Applied Categorical Structures, doi:10.1007/s10485-010-9244-x.

[Caramello, 2009a] O. Caramello, De Morgan classifying toposes, Advances in Mathematics 222 (2009), 2117-2144.

[Caramello, 2009b] O. Caramello, Universal models and definability, Math. Proc. Camb. Phil. Soc. (2012), 152, 279302, 2011, doi:10.1017/S0305004111000624.

[Caramello, 2009c] O. Caramello, Lattices of theories, arXiv:math.CT/0905.0299.

[Caramello, 2010] O. Caramello, The unification of Mathematics via Topos Theory, arXiv:math.CT/1006.3930v1.

[Johnstone, 2002a] P. T. Johnstone, Sketches of an Elephant: a topos theory compendium. Vol.1, vol. 43 of Oxford Logic Guides (Oxford University Press, 2002).

[Johnstone, 2002b] P. T. Johnstone, Sketches of an Elephant: a topos theory compendium. Vol.2, vol. 44 of Oxford Logic Guides (Oxford University Press, 2002).

[Mac Lane and Moerdijk, 1992] S. Mac Lane and I. Moerdijk, Sheaves in geometry and logic: a first introduction to topos theory (Springer-Verlag, 1992).

[Makkai and Reyes, 1977] M. Makkai and G. E. Reyes, First order categorical logic, Lecture Notes in Math. vol. 611 (Springer-Verlag, 1977).

Department of Pure Mathematics and Mathematical Statistics, University of Cambridge, Centre for Mathematical Sciences, Wilberforce Road, Cambridge, CB3 0WB, United Kingdom

Email: O.Caramello@dpmms.cam.ac.uk

This article may be accessed at http://www.tac.mta.ca/tac/ or by anonymous ftp at

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/26/6/26-06.{dvi,ps,pdf}

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods. Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication. Full text of the journal is freely available in .dvi, Postscript and PDF from the journal’s server at http://www.tac.mta.ca/tac/ and by ftp. It is archived electronically and in printed paper format.

Subscription information Individual subscribers receive abstracts of articles by e-mail as they are published. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh, rrosebrugh@mta.ca.

Information for authors The typesetting language of the journal is TEX, and L^{A}TEX2e strongly encouraged. Articles should be submitted by e-mail directly to a Transmitting Editor. Please obtain detailed information on submission format and style files at http://www.tac.mta.ca/tac/.

Managing editor Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca

TEXnical editor Michael Barr, McGill University: barr@math.mcgill.ca

Assistant TEX editor Gavin Seal, Ecole Polytechnique Fédérale de Lausanne:

gavin seal@fastmail.fm

Transmitting editors

Clemens Berger, Université de Nice-Sophia Antipolis, cberger@math.unice.fr Richard Blute, Université d’ Ottawa: rblute@uottawa.ca Lawrence Breen, Université de Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: ronnie.profbrown(at)btinternet.com

Valeria de Paiva: valeria.depaiva@gmail.com

Ezra Getzler, Northwestern University: getzler(at)northwestern(dot)edu Kathryn Hess, Ecole Polytechnique Fédérale de Lausanne : kathryn.hess@epfl.ch Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk P. T. Johnstone, University of Cambridge: ptj@dpmms.cam.ac.uk Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, Macquarie University: steve.lack@mq.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@buffalo.edu Tom Leinster, University of Glasgow, Tom.Leinster@glasgow.ac.uk Jean-Louis Loday, Université de Strasbourg: loday@math.u-strasbg.fr Ieke Moerdijk, University of Utrecht: moerdijk@math.uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Jiri Rosicky, Masaryk University: rosicky@math.muni.cz Giuseppe Rosolini, Università di Genova: rosolini@disi.unige.it Alex Simpson, University of Edinburgh: Alex.Simpson@ed.ac.uk James Stasheff, University of North Carolina: jds@math.upenn.edu Ross Street, Macquarie University: street@math.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Rutgers University: tierney@math.rutgers.edu Robert F. C. Walters, University of Insubria: robert.walters@uninsubria.it R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca