Topos theory in Logic and Algebraic Geometry

Eliot Hecky

August 2022

Introduction
This text is a report written after my master’s first year internship from May to July 2022 with Olivia
Caramello, whom I warmly thank.
The purpose is here to summarize most of the things I studied in topos theory, keeping it self-contained
and relatively brief. We begin by studying sheaves and Grothendieck toposes, and then their link with
theories in first-order logic. Almost all statements have proofs, the ones being omitted are explicitely
specified.
The aim of this text is not to give an introduction to category theory, which is why the well-known
definitions and results in general category theory are relegated to the end, in the appendix. The last
sections give examples of classifying toposes coming from algebraic geometry. Since only the topos-
theoretic part is relevant here, readers unfamiliar with basic algebraic geometry can read [15] or [14].
By default, every category is assumed locally small (see definition A.1).

Contents
1 Sheaves in topology 2

2 Grothendieck toposes 4
2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
2.2 The link with local operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
2.3 Diaconescu’s equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

3 Subobjects lattices in toposes 13

4 Categorical first-order logic 15

4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
4.2 A soundness theorem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

5 Syntactic sites and classifying toposes 23

5.1 Syntactic categories and a completeness theorem . . . . . . . . . . . . . . . . . . . . . . . 23
5.2 Classifying geometric theories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24

6 Theories of presheaf type 26

7 The Zariski topos 29

8 The crystalline topos 31

A Categorical prerequisites 36
A.1 Glossary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
A.2 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37

1
1 Sheaves in topology
In areas where topology is involved, like algebraic or differential geometry, sheaves are a powerful tool to
study the spaces in play. For example, schemes and manifolds are defined as sheaves - this section’s aim
is to study some of their properties.
Definition 1.1. Let C be a small category. Denote by Psh(C) the category [C op , Set] of contravariants
set-valued functors on C. An object F : C op −→ Set of Psh(C) is a presheaf on C and a natural
transformation F −→ G is a morphism of presheaves. If X is a topological space, write O(X) for the
category of open subsets of X with inclusions as morphisms, and Psh(X) for the category Psh(O(X)).
If F is a presheaf, i : U ⊂ V is an inclusion of open subsets and s ∈ F (V ), write s|U for F (i)(s).
Definition 1.2. Let X be a topological space. A presheaf F on X is a sheaf when for every open subset
V covered by open subsets (Vi )i∈I and for every family (si ∈ F (Vi ))i∈I such that si |Vi ∩Vj = sj |Vi ∩Vj for
all i, j there is a unique s ∈ F (V ) such that s|Vi = si for all i. Write Sh(X) for the full subcategory of
Psh(X) on sheaves.
It will be shown in the next section that Psh(X) and Sh(X) are toposes, which means that they come
with several nice categorical properties.
Proposition 1.3. Let C be a small category. Then Psh(C) has all small limits, exponentials (that is,
every product functor X × − has a right adjoint (−)X ) and has a subobject classifier. In particular,
Psh(C) is cartesian closed. The same is true for Sh(X) where X is a topological space, and will be shown
later, in theorem 2.8.
Proof. Psh(C) is a functor category to Set which has all small limits, so it has all small limits. Precisely,
limits are computed pointwise : if D : J −→ Psh(C) is a diagram of small shape J, (lim D)(c) is the
limit (in Set) of the diagram Dc : J −→ Set, sending i to Dc (i) = D(i)(c) and i −→ j to Dc (i −→ j) =
D(i −→ j)c .
Let P, Q ∈ Psh(C) be presheaves. Define QP (c) = HomPsh(C) (yC (c) × P, Q). This defines a presheaf
QP , which comes with a natural transformation e : QP × P −→ Q, where ec (θ, y) = θc (1c , y). It is
straightforward to see that we indeed get an adjunction : to every φ ∈ HomPsh(C) (R × P, Q), define a
unique corresponding φ0 ∈ HomPsh(C) (R, QP ) as follows. For c ∈ C and u ∈ Rc, let φ0c (u) : yC (c)×P −→ Q
be the natural transformation with components :
HomC (d, c) × P d −→ Qd
(φ0c (u))d :
(f, x) 7−→ φd (R(f )(u), x).
This definition is natural in d, so we get φ0 ∈ HomPsh(C) (R, QP ), and moreover ec (φ0c (u), y) = (φ0c (u))c (1c , y) =
φc (u, y) so that φ = e ◦ (φ0 × 1). The bijective assignment φ −→ φ0 is natural in R : (−)P is right adjoint
to − × P .
If Psh(C) has a subobject classifier Ω, it must classify the representables presheaves :
SubPsh(C) (yC (c)) ∼
= HomPsh(C) (yC (c), Ω).
By the Yoneda lemma, the right-hand side is Ω(c). This shows that Ω must send every object c to the
set of subpresheaves of HomC (−, c). This is how one defines the functor Ω. Then let true : 1 −→ Ω be
the obvious truec : {∗} −→ Ω(c) pointing at yC (c). To show that this is indeed a subobject classifier, let
Q ⊂ P be a subfunctor of a presheaf on C. For c ∈ C and x ∈ P c, set φc (x) = {f | P (f )(x) ∈ Q(dom(f ))}.
This gives a natural transformation φ : P −→ Ω. The diagram
!
Q 1

true

P φ
Ω

2
is then a pullback since φc (x) = yC (c) if and only if x ∈ Qc. This φ is moreover unique : if θ : P −→ Ω
yields the same pullback diagram, then for every f : a −→ c and x ∈ P c, P (f )(x) ∈ Qa if and only if
θa (P (f )(x)) = truea , namely P (f )(θc (x)) = truea , that is f ∈ θc (x). We finally get θc (x) = φc (x) for
every c and x : θ = φ.

When studying sheaves on topological spaces, there is a geometric mirror turning sheaves into spaces
which can shed light on both sides. Let X be a topological space.

Definition 1.4. The category of continuous maps (bundles on X) Y −→ X and commutative triangles
Top/X is denoted Bund(X). The full subcategory on the étale bundles (those Y −→ X which are local
homeomorphisms) is denoted Étale(X).

The end of this section is dedicated to construct a pair of adjoint functors Γ a Λ between Psh(X)
and Bund(X) restricting to an equivalence Sh(X) ' Étale(X).

Definition 1.5. Let p : Y −→ X be a bundle. A cross-section of p on an open U ⊂ X is a (continuous)

map s : U −→ Y such that ps is the inclusion of U in X. Denote by Γp the presheaf sending U to the set
Γp U of all cross-sections of p on U .
Let F be a presheaf on X, x ∈ X and U, V two open neighborhoods of x. If s ∈ F U and t ∈ F V
are such that there exists an open W ⊂ U ∩ V containing x such that s|W = t|W , we say that s
and t have the same germ at x. Define germx (s) as the equivalence class of sections of F under this
relation, and denote Fx = {germ `x (s)} the stalk of F at x. Equivalently, Fx = lim
−−→U 3x
F U . The set
ΛF = {(x, r) : x ∈ X, r ∈ Fx } ∼ = x∈X Fx comes with a projection p : ΛF −→ X of which each s ∈ F U
determines a cross-section ṡ : U −→ ΛF sending x to germx (s). p is made into a bundle by giving ΛF the
topology whose basis is open sets of the form ṡ(U ).

It is straightforward to see that Γp is always a sheaf, and that ΛF is always étale. Both constructions
are functorial, so we get two functors :

Γ : Bund(X)  Psh(X) : Λ

Theorem 1.6. There is an adjunction Λ a Γ, whose unit (called sheafification) ηP : P −→ ΓΛP is an

isomorphism when P is a sheaf, and whose counit Y : ΛΓY −→ Y is an isomorphism when Y is étale.
In particular, every sheaf is a sheaf of cross-sections, and every étale bundle is a bundle of germs.

Proof. Define ηP : P −→ ΓΛP to send an element s ∈ P (U ) to the cross-section ṡ : U −→ ΛP . If P

is a sheaf, then ṡ = ṫ (that is, germx (s) = germx (t) for each x ∈ U ) implies that for each x there is an
open Vx ⊂ U with s|Vx = t|Vx . Since the Vx ’s cover U , we get s = t. To show that ηP is surjective, let
h : U −→ ΛP be a cross-section. Each x ∈ U has an open neighborhood Ux such that hx = germx (sx ) for
some sx ∈ P (Ux ). By continuity of h there is an open neighborhood Vx of x in Ux such that h(Vx ) ⊂ s˙x (Ux ),
that is h = s˙x on Vx . Since P is a sheaf there is an s ∈ P (U ) with s|Vx = sx whence h = ṡ and ηP is
indeed an isomorphism.
Now define Y : ΛΓY −→ Y as follows. Each point of ΛΓY is of the form ṡx with s : U −→ Y a
cross-section and x ∈ X. Define Y (ṡx) = sx, which is independent of the choice of s (two sections having
the same germ implies that they agree on x). If p : Y −→ X is étale, Y has inverse θY sending each
y ∈ Y to ṡ(py) where s is a cross-section on a neighborhood of py.
To show the adjunction Λ a Γ, it suffices to show the triangle identities :
ηΓ
Γ ΓΛΓ Λ

Γ Λη
1 1

Λ
Γ ΛΓΛ Λ

3
If Y is a bundle over X and s ∈ ΓY U , the composite on the left sends s to ṡ ∈ ΓΛΓY U then to s ∈ ΓY U .
Similarly, if P is a presheaf on X, s ∈ P U and x ∈ X, the composite on the right sends germx (s) to
germx (ṡ) then to ṡx = germx (s).

It is a fundamental fact in algebraic geometry that a continuous map f : X −→ Y induces two functors
between Sh(X) and Sh(Y ). The first f ∗ : Sh(Y ) −→ Sh(X) sends a sheaf G on Y to the sheafification
of (f ∗ G)(U ) = −
lim
−→V ⊃f (U )
G(V ) and the second f∗ : Sh(X) −→ Sh(Y ) sends a sheaf F on X to the sheaf
(f∗ F )(V ) = F (f −1 V ). There is an adjunction f ∗ a f∗ and the left adjoint f ∗ preserves finite limits ; this
will constitute an example of a geometric morphism, see example 2.13.

2 Grothendieck toposes
2.1 Introduction
In this section we introduce the concept of Grothendieck toposes, which generalizes the construction of
Sh(X) from Psh(O(X)), replacing O(X) with any small category.

Definition 2.1. Let C be a category and c ∈ C.

– A presieve on c is a collection of arrows with codomain c ;

– A sieve on c is a presieve S on c such that for any f ∈ S and any arrow g composable with f , we
have f ◦ g ∈ S. If C is small, this is equivalently a subpresheaf S  HomC (−, c).

A presieve S generates the sieve S consisting of arrows with codomain c factoring through an arrow in S.

Definition 2.2. Let C be a category. A Grothendieck topology on C is a function J assigning to any c ∈ C

a collection of sieves on c such that :

(i) For any c ∈ C, the maximal sieve Mc = {f | cod(f ) = c} is in J(c) ;

(ii) For any f : d −→ c and S ∈ J(c), the pullback sieve f ∗ S = {g : e −→ d | f ◦ g ∈ S} is in J(d) ;
(iii) For any sieve S on c ∈ C and any T ∈ J(c), if f ∗ S ∈ J(dom(f )) for all f ∈ T then S ∈ J(c).

If J is a topology on C and S is a sieve of J, we say that S is (J-)covering. A site is a pair (C, J) with C
a category and J a Grothendieck topology on C.

Example 2.3. Let C be a category.

(i) The trivial topology on C is given by J(c) = {Mc } : on any given object, only the maximal sieve is
covering ;
(ii) Suppose C satisfies the right Ore condition : every pair of arrows with common codomain fits in a
commutative square. The atomic topology Jat on C has as covering sieves all the non-empty ones.
If C dit not satisfy this condition, the axiom 2.2.(ii) would not be fulfilled ;
(iii) If X is a topological space, define a Grothendieck topology on O(X) for which covering sieves on
an open U ⊂ X are those generated by (small) families (Ui )i∈I which are open coverings of U .

Definition 2.4. Let (C, J) be a small site. Recall that a presheaf on C is an object of the functor category
Psh(C) = [C op , Set]. Mimicking the definition of sheaves on a topological space, a sheaf on (C, J) is a
presheaf P ∈ Psh(C) such that the following condition is satisfied. For any c ∈ C, S ∈ J(c), and any
family (xf ∈ P (dom(f )))f ∈S such that for any arrow g composable with f , P (g)(xf ) = xf ◦g , there exists
a unique amalgamation x ∈ P (c) such that xf = P (f )(x) for all f ∈ S. Equivalently, for each c ∈ C and
S ∈ J(c), the evident diagram
Y Y
P (c) −→ P (dom(f )) ⇒ P (dom(g))
f ∈S f ∈S,dom(f )=cod(g)

4
is an equalizer (in Set).
Such a family (xf ∈ P (dom(f )))f ∈S is called a matching family. In a weaker manner, P is a separated
presheaf if all matching families have at most one amalgamation (that is, if the first arrow in the diagram
is injective).
Define Sh(C, J) to be the full subcategory of Psh(C) on sheaves. A Grothendieck topos is a category
E which is equivalent to some Sh(C, J) (for a small site (C, J)) ; in this case we say that (C, J) is a site
of definition of E.
If C is locally small, a Grothendieck topology J is subcanonical if all representable presheaves HomC (−, c)
are sheaves. In this case, the Yoneda embedding factors through the inclusion Sh(C, J) ,→ Psh(C) into a
full embedding y : C −→ Sh(C, J).

Example 2.5. (i) Set is the topos of sheaves on a point ;

(ii) Any presheaf category is a Grothendieck topos, since Psh(C) = Sh(C, J) where J is the trivial
topology on C ;
(iii) If X is a topological space and J is the topology described in 2.3.(iii), then Sh(O(X), J) = Sh(X) ;

One reason for which Grothendieck toposes are studied is that they enjoy many nice categorical
properties. Some of them are depicted in the next two theorems.

Theorem 2.6. Let (C, J) be a small site. The inclusion i : Sh(C, J) ,→ Psh(C) has a left adjoint called
sheafification which preserves finite limits.

Proof. Let P be a presheaf on C and for R ∈ J(c), let Match(R, P ) be the set of matching families indexed
by R. Define :
P + (c) = −
lim
−→
Match(R, P ).
R∈J(c)

An element of P + (c) is then an equivalence class of matching families, with (xf )f ∈R and (yg )g∈S being
equivalent when there is a covering sieve T ⊂ R ∩ S such that xh = yh for h ∈ T . P + is a presheaf,
with P + (h)((xf )f ∈R ) = (xhg )g∈h∗ R . This definition is functorial in P , and we get a canonical natural
transformation η : P −→ P + given by ηc (x) = {P (f )(x) : f ∈ Mc }.
Notice that η is a monomorphism if and only if P is a separated presheaf, and it is an isomorphism if and
only if P is a sheaf. We will show that P + is always separated, and that if P is separated then P + is a
sheaf.
Let P be a presheaf, we will show that P + is separated. Let x = (xf )f ∈R , y = (yg )g∈S ∈ P + (c) such
that P + (h)(x) = P + (h)(y) for some Q ∈ J(c) and all h ∈ Q. This means that for all h ∈ Q, there is a
covering sieve Th ⊂ h∗ R ∩ h∗ S such that xht = yht for all t ∈ Th . By 2.2.(iii), T = {ht : h ∈ Q, t ∈ Th } is
in J(c) and T ⊂ R ∩ S, so x = y.
Let P be a separated presheaf, we will show that P + is a sheaf. Let (xf ∈ P + (dom(f )))f ∈R be a
matching family for P + , with R ∈ J(c). Each xf is the equivalence class of some (xf,g ∈ P (dom(g)))g∈Sf
matching family for P . This means that for all f : d −→ c in R and h : d0 −→ d, there is a covering sieve
Tf,h ⊂ h∗ (Sf ) ∩ Sf h of d0 such that for all g ∈ Tf,h , xf,hg = xf h,g . By axiom 2.2.(iii), Q = {f g : f ∈ R, g ∈
Sf } is in J(c), and indexes a matching family y = (xf,g )f g∈Q . This definition does not depend on the
factorization f g, because if f g = f 0 g 0 then for any k ∈ Tf,g ∩ Tf 0 ,g0 , P (k)(xf,g ) = xf,gk = xf g,k = xf 0 ,g0 k =
P (k)(xf 0 ,g0 ). Since P is separated, xf,g = xf 0 ,g0 . There is left to prove that y is an amalgamation of
(xf )f ∈R , namely that (yf h )f ∈h∗ Q and xf = (xf,g )g∈Sf are equivalent. But Sf ⊂ f ∗ Q and for any g ∈ Sf ,
yf g = xf,g . This proves that P + is a sheaf.
Now let a = (−)++ be the sheafification functor candidate. We have to show the adjunction claimed
in the theorem.
Let F be a sheaf, and P a presheaf. Any natural transformation φ : P −→ F factors uniquely
through η into ψ : P + −→ F . Indeed, let (xf )f ∈R be a matching family for some R ∈ J(c). Then for

5
any h : d −→ c in R, ηd (xh ) = {P (k)(xh ) : k ∈ Md } and P (h)((xf )f ∈R ) = (xhg )g∈h∗ R . Since h ∈ R,
h∗ R = Md , and since the family is matching, we get the equality :
ηd (xh ) = P (h)((xf )f ∈R ).
If ψ exists, then ψ((xf )f ∈R ) is the unique y ∈ F (c) with :
P (h)(y) = P (h)(ψ((xf )f ∈R )) = ψ(P (h)((xf )f ∈R ) = ψ(ηd (xh )) = φ(xh ).
Since (φ(xh ))h∈R is matching for the sheaf F , this y indeed exists.
ηP ηP +
This means that ηP0 : P − −→ P + −−−→ a(P ) = P ++ defines the unit of the desired adjunction.
Finally, notice that for a presheaf P and a covering sieve R, Match(R, P ) ∼ = HomPsh(C) (R, P ). Since
HomPsh(C) (R, −) preserves limits and since filtered colimits commute with finite limits in Set, (−)+
preserves finite limits, so a does as well.

Definition 2.7. An elementary topos is a category which has finite limits, is cartesian closed and has a
subobject classifier.
Theorem 2.8. Any Grothendieck topos is an elementary topos and has small (co)limits.
Proof. Let (C, J) be a (small) site. (Small, but in particular) finite limits in Sh(C, J) are computed
pointwise like in Psh(C), because the inclusion i : Sh(C, J) ,→ Psh(C) has a left adjoint so it preserves
limits. In the same manner, since sheafification has a right adjoint it preserves colimits, so computing
colimits in Psh(C) then sheafifying them is a way to compute (small) colimits in Sh(C, J).
If exponentials exist in Sh(C, J) then for any sheaves F and G, and any presheaf P , we have (naturally
in P ) :
HomPsh(C) (P, i(GF )) ∼
= HomSh(C,J) (a(P ), GF )
∼
= HomSh(C,J) (a(P ) × F, G)
∼
= HomSh(C,J) (a(P × i(F )), G)
∼
= HomPsh(C) (P × i(F ), i(G))
∼
= HomPsh(C) (P, i(G)i(F ) ).
This means that if they exist, exponentials in Sh(C, J) are to be computed in Psh(C). There is left
to show that if F and G are sheaves then GF is a sheaf (and in fact, only G needs to be a sheaf).
Recall from proposition 1.3 that GF (c) = HomPsh(C) (yC (c) × F, G). Let τ, σ ∈ GF (c) be two such
natural transformations and S ∈ J(c) such that GF (f )(τ ) = GF (f )(σ) for all f : c0 −→ c in S. This
implies that τ (f, x) = σ(f, x) for all x ∈ F (c0 ). Let k : c0 −→ c be any arrow and g ∈ k ∗ S (that is,
kg ∈ S). Then GF (g)(τ (k, x)) = τ (kg, xg) = σ(kg, xg) = GF (g)(σ(k, x)). Since k ∗ S ∈ J(c0 ) and G is
separated, we get τ = σ so GF is separated as well. Now let S ∈ J(c) and suppose we are given a natural
transformation τf : yC (d) × F −→ G for every f : d −→ c in S, forming a matching family. Let us
construct τ 0 : yC × F −→ G+ such that for each f ∈ S, the diagram
τf
yC (d) × F G

yC (f )×1 ηG

yC (c) × F G+
τ0

commutes. If τ 0 exists, we get an amalgamation (ηG )−1 ◦ τ 0 (ηG is an isomorphism since G is a sheaf),
which is what we want. Let b be an object of C, k : b −→ c and x ∈ F (b). Set :
τb0 (k, x) = {τkh (1, F (h)(x)) : h ∈ k ∗ S}.

6
This family is matching for G for the k ∗ S ∈ J(b), since for any suitable m we have G(m)(τkh (1, F (h)(x))) =
τkh (m, F (hm)(x)) = τkhm (1, F (hm)(x)) : τ 0 : yC (c) × F −→ G+ is well defined.
To show that the square indeed commutes, let f : d −→ c in S ; so that f ∗ S is the maximal sieve Md
on d. For k : b −→ d and x ∈ F (b), we have on one side :

(τ 0 ◦ (yC (f ) × 1))(k, x) = τ 0 (f k, x) = {τf kh (1, F (h)(x)) : h ∈ (f k)∗ S = Mb }

and on the other side :

ηG τf (k, x) = ηG (τf k (1, x)) = {τf kh (1, F (h)(x)) : h ∈ Mb }.

Now there is left to show that Sh(C, J) has a subobject classifier. Say that a sieve S on an object c is
J-closed if the arrows f : d −→ c such that f ∗ S ∈ J(d) are all in S. Now define the subobject classifier
(Ω ∈ Sh(C, J), true : 1Sh(C,J)  Ω) as :

Ω(c) = {J-closed sieves on c}

Ω(f ) = f ∗ (−)
true(∗)(c) = Mc .

It is straightforward to prove that Ω is indeed a sheaf. To show that it is a subobject classifier, for F a
sheaf and A ⊂ F a subsheaf define the characteristic morphism χA : F −→ Ω as :

(χA )c (x) = {f : d −→ c | F (f )(x) ∈ A(d)}.

The corresponding square

A 1

true

F χA Ω

is then a pullback. Indeed it is pointwise a pullback since for all c in C and x ∈ F (c), x ∈ A(c) if and
only if (χA )c (x) = Mc . This also shows the uniqueness of χA since for any f : d −→ c, f ∈ (χA )c (x) if
and only if idd ∈ f ∗ (χA )c (x) = (χA )d (F (f )(x)), if and only if F (f )(x) ∈ A(d).

Definition 2.9. Let (C, J) be a small site. A subcategory D of C is J-dense if

(i) every object c ∈ C has a covering sieve R ∈ J(c) generated by morphisms whose domains are in D
(or equivalently, the sieve generated by all morphisms of codomain c is J-covering) ;
(ii) for any f : c −→ d in C with d ∈ D, there is R ∈ J(c) generated by morphisms g : b −→ c with f g
in D (or equivalently, the family of those morphisms generates a J-covering sieve).

Given any subcategory D of C, define the restriction J|D on D by letting J|D (d) be the collection of sieves
R|D = R ∩ Morphisms(D) with R ∈ J(d).

Lemma 2.10. Let (C, J) be a small site and D a subcategory satisfying the second condition of the
definition above. Then

(i) a sieve S is J|D -covering if and only if the generated sieve S in C is J-covering ;
(ii) for any sheaf A on (C, J), the restriction of A to D is a J|D -sheaf.

In particular, if D is a J-dense subcategory of C then the restriction Psh(C) −→ Psh(D) restricts to a

functor Sh(C, J) −→ Sh(D, J|D ).

7
Proof. (i) Since S|D = S ∩ Morphisms(D) = S, the if part is obvious. Conversely, if S = R|D for some
R ∈ J(d), then for any f : c −→ d in R the sieve f ∗ S contains all morphisms g : b −→ c with f g in
D so it is J-covering, and thus S ∈ J(d).
(ii) Let S ∈ J|D (d) and (sf ∈ A(dom(f )))f ∈S be a matching family. By the first part of the lemma, it is
enough to show that this family extends to a matching family for S, that is if there is a commutative
diagram
g1
b c1

g2 f1 ∈S

c2 f2 ∈S
d

then A(g1 )(sf1 ) = A(g2 )(sf2 ). Since b can be covered by morphisms h : a −→ b such that g1 h and
g2 h are in D, the images of the A(gi )(sfi ) under A(h) are both sf1 g1 h . Since A is a sheaf, they are
equal.

Theorem 2.11 (Comparison lemma). Let (C, J) be a small site and D a dense subcategory of C. Then
the restriction Sh(C, J) −→ Sh(D, J|D ) is an equivalence of categories.

Proof. Let B ∈ Psh(D). For an object c ∈ C, let A(c) be the limit of the composite
B
(D/c)op −→ Dop −→ Set.

We clearly get a presheaf A ∈ Psh(C), and the assignment τ : B 7→ A is clearly a functor Psh(D) −→
Psh(C).
If A is a sheaf on (C, J), then for any matching family (sf ∈ A|D (dom(f )))f ∈D/c the same argument as
in lemma 2.10.(ii) ensures that it extends to a matching family for the sieve generated by all morphisms
in D to c, hence there is a unique s ∈ A(c) with A(f )(s) = sf for all f .
Conversely, if B is a sheaf on (D, J|D ) and we are given an element (sf ∈ B(dom(f )))f ∈D/d of τ (B)(d),
then for each f : e −→ d the morphisms g : e0 −→ e for which f g is in D generate a J|D -covering sieve.
Thus, sf is uniquely determined by the sf g for all such g, the latter being determined by sidd (since idd
is the terminal object in D/d).
It just remains to show that if B is a sheaf on (D, J|D ) then τ (B) is a sheaf on (C, J). We prove that
for each c ∈ C and S ∈ J(c), the natural transformations S −→ τ (B) factor uniquely through S  yC (c).
Let α : S −→ τ (B) be such a natural transformation : we have to find an element of τ (B)(c). By
definition this is a matching family (xf ∈ B(d))f :d−→c,d∈D . For such f , the sieve (f ∗ R)|D is J|D -covering
on d and α defines a matching family of elements of B for this covering sieve. Since B is a sheaf, this
gives an element xf as required.

As for any other structure in mathematics, let us define a notion of morphism between Grothendieck
toposes. The usual notion of a functor does not carry enough structure for Topos to be an interesting
category :

Definition 2.12. Let E and F be Grothendieck toposes. A geometric morphism f : E −→ F is a pair

of adjoint functors f ∗ a f∗ such that the left adjoint f ∗ : F −→ E preserves finite limits. If moreover
f ∗ has a left adjoint, then f is an essential geometric morphism. A point of a topos E is a geometric
morphism Set −→ E. A geometric transformation η : f −→ g between geometric morphisms is a natural
transformation f ∗ −→ g ∗ . Denote by Geom(E, F) the category of geometric morphisms E −→ F and
geometric transformations between them.

8
Example 2.13. (i) Let f : X −→ Y be a continuous map of topological spaces. Then the inverse
and direct image functors introduced in the end of the first section yield a geometric morphism
f : Sh(X) −→ Sh(Y ). If Y is Hausdorff (or more generally, sober) then the corresponding map
HomTop (X, Y ) −→ Geom(Sh(X), Sh(Y )) is a bijection (see [12], p.348). In particular, under this
assumption, the points of the topos Sh(Y ) are in bijection with the points of the space Y .
(ii) Let f : C −→ D be a functor. It induces an essential geometric morphism f : [C, Set] −→ [D, Set],
where f ∗ = − ◦ f . The left and right adjoints of f ∗ are given by its Kan extensions. If C and D
have finite limits and they are preserved by f , then the left extension f! : Psh(C) −→ Psh(D) also
preserves finite limits, and is thus the left adjoint of a geometric morphism Psh(D) −→ Psh(C).
(iii) There are non-trivial toposes without any points. In the light of the next sections, these are the
toposes arising from consistent geometric theories which have no models in Set. It is discussed in
[2], but an example found by Deligne is given in [1], p.243 : let K be a compact space and µ a
measure on K. Endow the ordered set of measurable subsets of K modulo subsets of measure zero
with the Grothendieck topology given by countable open covers (modulo subsets of measure zero).
If µ is not trivial, the corresponding topos is not empty, but its points are given by those x ∈ K
such that µ({x}) 6= 0. Take K = [0, 1] with the Lebesgue measure to find a pointless topos.

2.2 The link with local operators

There is another description of Grothendieck toposes in terms of Lawvere-Tierney topologies on presheaf
toposes. This equivalence shortens some proofs and definitions, and we shall give it here.

Definition 2.14. Let E be an elementary topos. A local operator, or Lawvere-Tierney topology on E is

an arrow j : Ω −→ Ω such that these three diagrams commute :
∧
1 Ω Ω×Ω Ω

true j
true j j×j j

∧
Ω j
Ω Ω j
Ω Ω×Ω Ω

∧ : Ω × Ω −→ Ω being the meet operation in the internal Heyting algebra structure of Ω, that is the
classifying arrow of the monomorphism (true, true) : 1  Ω × Ω (see remark 3.10).
A closure operator on E is a family of functions cX : SubE (X) −→ SubE (X) indexed by X ∈ E such
that m ≤ c(m) and c(c(m)) = c(m) for all m. c is called universal if it preserves pullbacks.

Example 2.15. In Heyting algebras, the intuitionistic identities x ≤ ¬¬x, ¬¬¬¬x = ¬¬x and ¬¬(x∧y) =
¬¬x ∧ ¬¬y always hold (see definition 3.6) : ¬¬ is a universal closure operator.

Theorem 2.16. If E is an elementary topos, there is a bijection between Lawvere-Tierney topologies on

E and universal closure operators.

Proof. Send a closure operator c to jc : Ω −→ Ω the classifying morphism of c(true : 1 −→ Ω). It is a

Lawvere-Tierney topology : the first diagram commutes by the universal property of the pullback (with the
arrows true : 1 −→ Ω and 1 −→ 1), the second by universality of c and the fact that c(c(true)) = c(true).

9
For the third one, notice that by universality of c, every vertical face in this diagram is a pullback :

1 1
(true,true)
true

m×m m Ω×Ω ∧ Ω

c(true)×c(true) jc ×jc jc
c(true)

Ω×Ω ∧ Ω

Conversely, send a local operator j : Ω −→ Ω to cj which takes a subobject m  b with classifying

arrow χm : b −→ Ω to the subobject m0 with classifying arrow jχm (cj (m)  b is the pullback of true
along jχm ). Since j ◦ true = true, we can use the universal property of the pullback to get a morphism
m −→ cj (m). The identity j 2 = j proves directly that cj (cj (m)) = cj (m), and the square defining j can
be used to show that cj preserves pullbacks. Finally, use the same arguments to get cjc (m) = m for all
m and j = jcj .

Definition 2.17. Let E be an elementary topos and c a universal closure operator on E. A monomorphism
m : Y 0  Y is c-dense if c(m) = idY . An object X is a c-sheaf if for any c-dense monomorphism
m : Y 0  Y the arrows Y 0 −→ X all factor uniquely through m ; that is

HomE (m, X) : HomE (Y, X) −→ HomE (Y 0 , X)

is bijective. Write shc (E) (or shj (E) if j and c correspond under the equivalence of theorem 2.16) for the
full subcategory of E on c-sheaves.

Theorem 2.18. Let C be a small category. The Grothendieck topologies on C correspond bijectively to
the Lawvere-Tierney topologies on Psh(C).

Proof. It was shown in proposition 1.3 that the subobject classifier in Psh(C) is given by Ω(c) being
the set of subpresheaves of yC (c), that is sieves on c. Given a Lawvere-Tierney topology j on Psh(C),
the subobject J  Ω whose classifying arrow is j verifies S ∈ J(c) if and only if jc (S) = Mc . Since
j ◦ true = true, Mc ∈ J(c). Since j is a natural transformation, each arrow f : c0 −→ c induces
jc0 (f ∗ S) = f ∗ jc (S) ; in particular S ∈ J(c) implies f ∗ S ∈ J(c0 ). For the transitivity, if S ∈ J(c)
and T is a sieve on c such that g ∗ T ∈ J(dom(g)) for all g ∈ S then for such g : d −→ c we have
g ∗ jc (T ) = jd (g ∗ T ) = Md . Since idd ∈ g ∗ jc (T ) for all g ∈ S, S ⊂ jc (T ) and Mc = jc (S) ⊂ jc jc (T ). This
shows that jc (T ) = Mc , that is T ∈ J(c).
Conversely, given a Grothendieck topology J on C one can define j : Ω −→ Ω by saying that jc (S) is
the set of arrows g : d −→ c such that g ∗ S ∈ J(dom(g)). The naturality of j is obvious, as well as the
fact that jc (Mc ) = Mc , which means that j ◦ true = true. Since S ⊂ T implies jc (S) ⊂ jc (T ), we get
jc (S ∩ T ) = jc (S) ∩ jc (T ). Finally, it is clear that S ⊂ jc (S) so jc (S) ⊂ jc jc (S), and if g ∈ jc jc (S) then
g ∗ jc (S) ∈ J(dom(g)). Since for each h ∈ jc (S) one has h∗ S = Mc ∈ J(dom(h)), the transitivity axiom
implies that g ∈ jc (S).
It is straightforward to check that these two assignments are inverse bijections.

Theorem 2.19. Let C be a small category. If a Lawvere-Tierney topology j on Psh(C) and a Grothendieck
topology J on C correspond under the bijection of theorem 2.18, then the j-sheaves are exactly the J-sheaves
: shj (Psh(C)) = Sh(C, J).

10
Proof. Let P ∈ shj (Psh(C)). For each object c and S ∈ J(c), one has

HomPsh(C) (S, P ) ∼
= HomPsh(C) (yC (c), P ) ∼
= P (c)

because by definition S  yC (c) is a j-dense monomorphism. This clearly shows that P is a J-sheaf.
Conversely, if P is a J-sheaf and A  E is a j-dense monomorphism in Psh(C), we have to show that
all natural transformations σ : A −→ P extend uniquely to E −→ P . By the construction in theorem
2.18, we have for every e ∈ E(c) that e ∈ cj (A)(c) if and only if χA (e) ∈ J(c). By the construction of
χA in theorem 2.8, this is the case exactly when {f : d −→ c | E(f )(e) ∈ A(d)} ∈ J(c). Since we already
have a matching family (σd (E(f )(e)) for this covering sieve, there is an amalgamation p ∈ P (c) which
can define τc (e) = p as a natural extension of σ to E.

Example 2.20. Let E be an elementary topos. The ¬¬ closure from example 2.15 defines a subtopos
sh¬¬ (E). This topos is always a boolean category, and this fact can be used to prove that the continuum
hypothesis is not provable in ZFC. If A is a set strictly larger than N, let P be the poset of maps
p : Fp −→ 2 (with Fp a finite subset of A × N), where q ≤ p if Fp ⊂ Fq and q|Fp = p. Then it can be
shown that in the internal logic of the Cohen topos sh¬¬ (Psh(P )) (which is boolean), the axiom of choice
holds but not the continuum hypothesis (for the set A).

2.3 Diaconescu’s equivalence

A fundamental theorem of Diaconescu gives a nice description of geometric morphisms with target a given
topos Sh(C, J) as certain functors coming out of C. Let C be a small category.
R
Definition 2.21. For a presheaf P ∈ Psh(C), the category of elements P has objects pairs (c, x) with
c ∈ C and x ∈ P c and arrows (c,Rx) −→ (d, y) for each f : c −→ d such that P (f )(y) = x. There is a
canonical projection functor πP : P −→ C.

Proposition 2.22. Let E be a locally small and cocomplete category. Then for any functor A : C −→ E,
the functor :
E −→ Psh(C)
RA :
e 7−→ HomE (A(−), e)
has a left adjoint − ⊗C A : Psh(C) −→ E.

Proof. The desired left adjoint sends P ∈ Psh(C) to P ⊗C A = colim(A ◦ πP ). A morphism of presheaves
τ : P −→ RA (e) is a family of maps (τc : P c −→ HomE (Ac, e))c∈C natural in c. We view this data as a
family of arrows (τc (x) : Ac −→ e)(c,x)∈R P , and the naturality of τ is viewed as the commutativity of

Ac AπP (c, x)
τc (x)

Au AπP u e
τc0 (y)
Ac0 AπP (c0 , y)

for each u : c0 −→ c. This means that the arrows τc (x) form a cocone over the diagram AπP . By the
universal property of colimits, cocones with target e are in bijection with arrows colim(AπP ) −→ e, which
means that HomPsh(C) (P, RA e) ∼ = HomE (colim(AπP ), e). This bijection is natural in P and e, which
concludes the proof.

11
Definition 2.23. Let E be a Grothendieck topos. A functor A : C −→ E is flat if − ⊗C A preserves
finite limits. Let J be a Grothendieck topology on C. A is J-continuous if it sends J-covering sieves to
epimorphic families. Let Flat(C, E) be the full subcategory of [C, E] on flat functors, and FlatJ (C, E) be
the full subcategory of Flat(C, E) on J-continuous flat functors.

Theorem 2.24 (Weak Diaconescu’s equivalence). Let C be a small category and E a Grothendieck topos.
Then there is an equivalence of categories :

Geom(E, Psh(C)) ' Flat(C, E)

sending a geometric morphism f : E −→ Psh(C) to the flat functor f ∗ ◦ yC and a flat functor A : C −→ E
to the geometric morphism − ⊗C A a RA .

Proof. Begin by noticing that by the Yoneda lemma, RyC (E)(c) = HomPsh(C) (yC (c), E) ∼ = E(c), which
means that RyC ∼ = idPsh(C) and by the uniqueness of the left adjoint, P ∼ = P ⊗C yC : any presheaf is a
colimit of representable presheaves. Furthermore, f ∗ and − ⊗C (f ∗ ◦ yC ) agree on representables and both
commute with colimits, whence they are isomorphic ; in particular f ∗ ◦ yC is indeed flat. Proposition
R 2.22
shows that − ⊗C A a RA is a geometric morphism when A is flat. Notice that the category yC (c) has
id : c −→ c as a terminal object ; the colimit of AπyC (c) is its value on this terminal object :

[(− ⊗C A) ◦ yC ](c) ∼
= AπyC (c) (c, idc ) = Ac,

whence the equivalence.

Definition 2.25. A functor A : C −→ E from a small category C into a topos E is filtering if :

(i) the family of maps (Ac −→ 1)c∈C is epimorphic ;

(ii) for any two objects c and d, the family of maps

(Au, Av) : Ab −→ Ac × Ad
u v
indexed by the spans c ←− − b −→ d is epimorphic ;
(iii) for any two parallel arrows u, v : c −→ d, letting eu,v be the equalizer in E of Au and Av, the family
of maps Ab −→ eu,v factoring the Aw for w : b −→ c equalizing u and v (uw = vw) is epimorphic.

Lemma 2.26. Let C be a small category with finite limits and E a Grothendieck topos. Then a functor
C −→ E is flat if and only if it preserves finite limits.

Proof. For conciseness purposes, we admit the fact that a functor A : C −→ E is flat if and only if it is
filtering (see [12], theorem VII.9.1, pages 399 to 409. We only need here the if part, which is proven by
showing that − ⊗C A preserves the terminal object as well as pullbacks). Suppose A is flat. Since yC
preserves limits, the composite (− ⊗C A) ◦ yC : C −→ E preserves finite limits. It was shown in theorem
2.24 that this functor is naturally isomorphic to A, whence A preserves finite limits as well. Conversely,
suppose that A preserves finite limits. We show that it is filtering (see definition 2.25). The first condition
is fulfilled since A(1) −→ 1 is an isomorphism. For the second condition, notice that for two objects c
πc πd
and d, the span c ←− − c × d −→ d gives an isomorphism (Aπc , Aπd ) : A(c × d) −→ Ac × Ad. The third
condition is evident as A preserves equalizers.

Lemma 2.27. Let (C, J) be a small site, E a Grothendieck topos and f : E −→ Psh(C) a geometric
morphism. The following are equivalent :

(i) f factors through Sh(C, J)  Psh(C) ;

(ii) f ∗ ◦ yC maps J-covering sieves to colimits ;
(iii) f ∗ ◦ yC is J-continuous.

12
Proof. (i) ⇒ (ii) : let S be a J-covering sieve on an object c : the monomorphism u : S  yC (c) is J-dense,
so HomPsh(C) (u, f∗ F ) is an isomorphism for all F ∈ E (see theorem 2.19). By the adjunction f ∗ a f∗ ,
the map HomE (f ∗ u, F ) is also an isomorphism for all F ∈ E ; by the Yoneda lemma, f ∗ S  f ∗ yC (c) is
then an isomorphism. Writing the sieve as a colimit of representable presheaves S ∼ = lim
−−→d−→c∈S
yC (d) and
applying the colimit-preserving functor f ∗ , we get an isomorphism :

lim
−−→
f ∗ yC (d) ∼
= f ∗ yC (c).
d−→c∈S

(ii) ⇒ (iii) : this is immediate since a colimiting cocone is obviously an epimorphic family.
(iii) ⇒ (i) : it suffices to show that f ∗ sends dense monomorphisms B ⊂ P to isomorphisms. As in
the first part of the proof, write P as a colimit of representables lim
−−→i∈I
yC (ci ). For each i, define Bi as the
pullback of B  P along the cocone leg yC (ci ) −→ P . Since pullbacks preserve colimits, B ∼ = lim
−−→i∈I
Bi ,
and Bi  yC (ci ) is a dense monomorphism. This means that Bi is a J-covering sieve on ci . For each
arrow u : d −→ ci in this sieve Bi , draw the triangle

f ∗ yC (u)
f ∗ yC (d) f ∗ yC (ci )

f ∗ (Bi )

Since f ∗ ◦ yC is J-continuous, the arrows f ∗ yC (u) are an epimorphic family, so the lower-right arrows
are as well, and they form an isomorphism. Moreover, f ∗ preserves colimits so f ∗ (B)  f ∗ (P ) is an
isomorphism.

Theorem 2.28 (Strong Diaconescu’s equivalence). The equivalence of theorem 2.24 restricts to an equiv-
alence :
Geom(E, Sh(C, J)) ' FlatJ (C, E).

Proof. Geometric morphisms E −→ Sh(C, J) are exactly the geometric morphisms f : E −→ Psh(C)
which factor through Sh(C, J)  Psh(C), and by lemma 2.27 they are exactly those for which f ∗ ◦ yC is
J-continuous.

3 Subobjects lattices in toposes

Toposes are often described as good mathematical universes in which one can do usual mathematics,
replacing sets with the objects of the topos. Every topos has an internal language in which one can study
first-order logic intrinsically. In general, this logic is not classical but intuitionistic : the law of excluded
middle need not hold. This will appear in this section as toposes are Heyting categories, ant not always
boolean. Other classes of categories are introduced, and they serve as natural settings in which one can
interpret the fragments of logic which will be introduced in the next section.

Definition 3.1. Let C be a category with pullbacks. Since the pullback of a monomorphism is itself
monomorphic, any arrow f : c −→ d induces a functor on the subobject posets

f ∗ : SubC (d) −→ SubC (c),

sending a subobject s to the pullback f ∗ s  c of s  d along f .

Definition 3.2. A cartesian category is a category which has all finite limits ; a cartesian functor
is a functor between cartesian categories which preserves finite limits. Write Cart(C, D) for the (full
sub)category on cartesian functors between two cartesian categories C and D.

13
Definition 3.3. Let C be a cartesian category. We say that C has images if for any morphism f : c −→ d
there is a subobject Im(f ) of d which is the least (in SubC (d)) through which f factors. In the factorization
f : c −→ Im(f ) −→ d, the arrow c(f ) : c −→ Im(f ) is called a cover. If C has images and they are stable
under pullback (see definition 3.1), we say that C is regular. A regular functor is a cartesian functor
between regular categories which preserves covers ; write their category Reg(C, D).

Proposition 3.4. If f : c −→ d is an arrow in a regular category C, the pullback functor f ∗ has a left
adjoint ∃f .

Proof. The left adjoint assigns to m : b  c the image Im(f m)  d. The adjunction is immediate : given
a subobject s  d, Im(f m) ≤ s if and only if m ≤ f ∗ s by the universal property of the pullback.

Definition 3.5. A coherent category is a regular category in which subobject posets have finite unions
which are stable under pullback. Subobject posets in coherent categories have a structure of a distributive
lattice, so we call them subobject lattices. A coherent functor between coherent categories is a regular
functor which preserves finite unions. Write Coh(C, D) for the category of coherent functors between C
and D.

Definition 3.6. A Heyting algebra is a lattice L (a poset with finite products and finite coproducts) such
that every functor − ∧ a has a right adjoint a ⇒ − ; namely there is an operation ⇒: Lop × L −→ L
satisfying the universal property that (x ∧ a) ≤ b if and only if x ≤ (a ⇒ b). A Heyting category is a
coherent category such that every pullback functor f ∗ has a right adjoint ∀f .

Proposition 3.7. Let C be a Heyting category and b, c  d be two subobjects. Then there exists a largest
subobject (b ⇒ c)  d such that (b ⇒ c) ∩ b ≤ c. This defines an operation ⇒: SubC (d) × SubC (d) −→
SubC (d) which is preserved by pullback functors. In particular, the subobject lattices in a Heyting category
are Heyting algebras.

Proof. Write m : b  d and let (b ⇒ c) = ∀m (b ∩ c) (the intersection b ∩ c  b being the pullback of

c  d along m). The property is given by the adjunction m∗ a ∀m .

When c  d is a subobject in a Heyting category, write ¬c = c ⇒ 0. Notice that in general c ∪ ¬c

is different from d, which explains why the law of excluded middle does not hold in the logic of Heyting
categories. It however holds in boolean categories which carry classical logic :

Definition 3.8. A boolean category is a coherent category in which every subobject c  d is comple-
mented : there exists a unique subobject b  d such that b ∪ c = 1 and b ∩ c = 0.

Definition 3.9. A category C is well-powered if for every object c, the poset SubC (c) is essentially small.
A geometric category is a well-powered regular category in which subobject posets have small (hence
arbitrary) unions which are stable under pullbacks. A geometric functor between geometric categories is
a regular functor which preserves unions ; write Geo(C, D) for their category.

Remark 3.10. The relations between the different classes of categories which have been defined so far

14
are summarized in this diagram :

Cartesian

Regular

Coherent Geometric

Heyting Grothendieck topos

Boolean Elementary topos

Proof. To see that a boolean category is Heyting, let c ⇒ d = ¬c ∪ d. A geometric category is Heyting
by the adjoint functor theorem for posets, which states that if G : D −→ C is a functor between posets
such that D has and G preserves all (small) unions, then G has a right adjoint.
If E is an elementary topos, Ω is an internal Heyting algebra, by letting :

– 0 : 1 −→ Ω be the classifying arrow of 0  1 ;

– 1 : 1 −→ Ω be true : 1  Ω ;
– ∧ : Ω × Ω −→ Ω be the classifying arrow of (true, true) : 1  Ω × Ω ;
– ∨ : Ω×Ω −→ Ω be the classifying arrow of π1∗ (true)∪π2∗ (true) where πi is the projection Ω×Ω −→ Ω
and πi∗ (true) is the pullback of true along it ;
– ⇒: Ω × Ω −→ Ω be the classifying arrow of the equalizer of ∧ and π1 .

Given a subobject lattice SubE (c), the Heyting algebra structure on it is induced by the internal Heyting
algebra structure on Ω. For example, given a  c and b  c (with classifying arrows χa and χb ),
construct a ∧ b  c as the pullback of true along the composite
(χa ,χb ) ∧
c −−−−−→ Ω × Ω −→ Ω.

4 Categorical first-order logic

4.1 Introduction
This section will show how Grothendieck toposes constitute an ideal setting to study first-order theories
in logic. Most of the examples will come from algebraic geometry and will prove to be relevant in the next
section, but of course many interesting results can be proved outside of algebraic geometry with these
tools. We begin with some general first-order logic.

Definition 4.1. A signature Σ is a triple (S, F, R) of sets, where :

(i) S is the set of sorts of Σ ;

(ii) F is the set of function symbols of Σ, each function symbol having a type, consisting of a non-empty
list of sorts. We write f : A1 · · · An −→ B when a symbol f has type (A1 , . . . , An , B) ;
(iii) R is the set of relation symbols of Σ, each relation symbol having a type, consisting of a (possibly
empty) list of sorts. We write R  A1 · · · An when a symbol R has type (A1 , . . . , An ).

15
If A is a sort, we suppose that there are as many variables of sort A as we may wish to use. Terms over
Σ (and their sorts) are defined to be elements of the smallest set such that the following are terms (if a
term t has sort A, we write t : A) :

(i) x : A when x is a variable of sort A ;

(ii) f (t1 , . . . , tn ) : B when f : A1 · · · An −→ B is a function symbol and each ti : Ai is a term of sort Ai .

Definition 4.2. We define the set of formulae over a signature Σ recursively (if φ is a formula, we also
define the set FV(φ) of free variables of φ) :

(i) R(t1 , . . . , tn ) is a formula when R  A1 · · · An is a relation symbol and each ti : Ai is a term, and
the free variables are those occurring in some ti ;
(ii) s = t is a formula when s and t are terms of the same sort, and the free variables are those occurring
in s or t ;
(iii) > is a formula without any free variable ;
(iv) φ ∧ ψ is a formula when φ and ψ are, and FV(φ ∧ ψ) = FV(φ) ∪ FV(ψ) ;
(v) ⊥ is a formula without any free variable ;
(vi) φ ∨ ψ is a formula when φ and ψ are, and FV(φ ∨ ψ) = FV(φ) ∪ FV(ψ) ;
(vii) φ ⇒ ψ is a formula when φ and ψ are, and FV(φ ⇒ ψ) = FV(φ) ∪ FV(ψ) ;
(viii) ¬φ is a formula when φ is, and FV(¬φ) = FV(φ) ;
(ix) (∃x : A)φ is a formula when φ is and x is a variable of sort A, and FV((∃x : A)φ) = FV(φ) \ {x} ;
(x) W(∀x : A)φ is a formula when φ is and x isS a variable of sort A, and FV((∀x : A)φ) = FV(φ) W \ {x} ;
(xi) Vi∈I φi is a formula when each φi is and Si∈I FV(φi ) is finite, and this set is then FV(Vi∈I φi ) ;
(xii) i∈I φi is a formula when each φi is and i∈I FV(φi ) is finite, and this set is then FV( i∈I φi ).

A variable occurring in a formula without being free is called a bound variable.

Alas, it is too restrictive to consider the twelve types of formulae at once, whence it is convenient to
restrict ourselves to certain types of formulae.

Definition 4.3. In this table we define restrictions of logic by only allowing for a given fragment (columns)
certain types of formulae (lines).
∞-First-order
First-order
Geometric
Coherent
Regular
Atomic
Horn

R(t1 , . . . , tn ) X X X X X X X
s=t X X X X X X X
> X X X X X X
φ∧ψ X X X X X X
⊥ X X X X
φ∨ψ X X X X
φ⇒ψ X X
¬φ X X
(∃x : A)φ X X X X X
(∀x : A)φ X X
W
φi X X
i∈I
V
φi X
i∈I

16
 There is an eighth class of formulae called cartesian which will be defined later. It sits between Horn
and Regular formulae, only allowing existential quantification in certain cases.

When working in categories other than Set, the formulae must come with some additional syntactic
data :

Definition 4.4. A context is a (possibly empty) finite sequence ~x = (x1 , . . . , xn ) of distinct variables of a
given signature. If Ai is the sort of xi , the type of ~x is the sequence (A1 , . . . , An ). If ~x and ~y are contexts
and z is a variable, ~x, z is the context (x1 , . . . , xn , z) and ~x, ~y is the context (x1 , . . . , xn , y1 , . . . , ym ). If all
free variables of a formula φ appear in a context ~x, we say that ~x is a suitable context for φ and that the
pair ~x.φ is a formula-in-context. The canonical context of a formula is the sequence of its free variables,
in order of appearance.
Two formulae are α-equivalent if one can rename the bound variables of one to get the other. Modulo
α-equivalence, we can always assume that formulae have no conflict between their bound and free variables.
For example, R(x) ∨ (∀x : A)S(x, y) has one bound and one free x, but is α-equivalent to R(x) ∨ (∀z :
A)S(z, y).
If ~x is a suitable context for φ and ~s is a sequence of terms of the same length and type as ~x, let
φ[~s/~x] be the (α-equivalence class) obtained by replacing each free xi by si in φ (after some potentially
necessary renaming of the bound variables of φ).

We are now able to define theories, in a same manner as is done usually in classical first-order logic :

Definition 4.5. A sequent is an expression φ `~x ψ where ~x is a context suitable for both formulae φ and
ψ. Intuitively, ψ is meant to be a logical consequence of φ in the context ~x. Some classical first-order
logic lessons use φ  ψ, which we will not do here.
If both φ and ψ are atomic/Horn/regular/coherent/first-order/geometric/infinitary first-order, we say
that φ `~x ψ is an atomic/.../infinitary first-order sequent.
A theory is a set of sequents (of course over the same signature) called the axioms of the theory. If
all axioms of a theory T are atomic/.../infinitary first-order, we say that T is an atomic/.../infinitary
first-order theory.

Remark 4.6. A theory is usually defined to be a set of sequents or formulae which is closed under logical
consequence, while a set of axioms generating such a theory is called an axiomatization. This will not
make any difference in practice, besides, logical consequence has not been defined yet.

Example 4.7. (i) A theory whose signature has no sorts is a propositional theory, and its study is
basically reduced down to propositional logic ;
(ii) A theory whose signature has no relation symbol and whose axioms are all of the form > `~x s = t
is an algebraic theory (and automatically Horn) ;
(iii) A particularly relevant example is the theory of local rings. Start with the (algebraic) theory of
rings, defined over the signature with one sort A, two constants 0 and 1, two binary function symbols
+ and × and a unary function symbol −, with the following axioms :

> `x 0 + x = x
> `x,y x + y = y + x
> `x,y,z (x + y) + z = x + (y + z)
> `x x + (−x) = 0
> `x 1 × x = x
> `x,y x × y = y × x
> `x,y,z (x × y) × z = x × (y × z)
> `x,y,z x × (y + z) = (x × y) + (x × z).

17
 Add to the algebraic theory of rings the coherent axioms of locality :
n
_
x1 + · · · + xn = 1 `x1 ,...,xn ∃y(xi × y = 1) (n ∈ N)
i=1

We can notice two things here. The first is that the symbol − is superfluous, because the fourth
axiom can be replaced by > `x ∃y(x + y = 0). We do not wish to do this, because then the theory
of rings would not be algebraic nor Horn anymore, it would only be regular. The second one is
that local rings are usually defined by the property of having a unique maximal ideal ; which is not
expressible in (even infinitary) first-order logic. We are saved by the fact that being a local ring is
equivalent to asking that for every element x, either x or 1 − x is invertible. We cannot express
locality in regular logic, so the theory of local rings is at best coherent. Notice that it would be
enough to only keep n = 0 and n = 2, since n = 1 is always true and the cases n > 2 follow by
induction.

Now is time to inject first-order theory into category theory by interpreting formulae and theories
inside of nice enough categories.

Definition 4.8. Let C be a category with finite products and Σ a signature. A Σ-structure M in C
consists of :

(i) For each sort A, an object M A ∈ C (defining for each finite sequence of sorts (A1 , . . . , An ) the object
M (A1 , . . . , An ) = M A1 × · · · × M An ) ;
(ii) For each function symbol f : A1 · · · An −→ B, an arrow M f : M (A1 , . . . , An ) −→ M B ;
(iii) For each relation symbol R  A1 · · · An , a subobject M R  M (A1 , . . . , An ).

Of course we want these structures to form a category, so we define a Σ-structure homomorphism h :

M −→ N to be a collection of arrows hA : M A −→ N A indexed by the sorts of Σ such that :

– For each function symbol f : A1 · · · An −→ B, the induced diagram

Mf
M (A1 , . . . , An ) MB

hA1 ×···×hAn hB

Nf
N (A1 , . . . , An ) NB

commutes ;
– For each relation symbol R  A1 · · · An , there is an arrow M R −→ N R such that the diagram

MR M (A1 , . . . , An )

hA1 ×···×hAn

NR N (A1 , . . . , An )

commutes.

Notice that Σ-Str is 2-functorial : if a functor C −→ D preserves finite products and monomorphisms
(for example, if it preserves finite limits), it induces a functor Σ-Str(C) −→ Σ-Str(D), and any natural
transformation T −→ T 0 between two such functors induces a natural transformation Σ-Str(T ) −→
Σ-Str(T 0 ).

18
 We can now interpret terms and later formulae on a given signature Σ in Σ-structures :
Definition 4.9. Let C be a category with finite products and M ∈ Σ-Str(C). We recursively interpret a
term-in-context ~x.t (with xi : Ai and t : B) in M as a morphism J~[Link] : M (A1 , . . . , An ) −→ M B :
– If t is a variable xi , let J~[Link] = πi be the i-th product projection ;
– If t = f (t1 : C1 , . . . , tm : Cm ), let J~[Link] be the composition :
(J~
x.t1 KM ,...,J~
[Link] KM ) Mf
M (A1 , . . . , An ) −−−−−−−−−−−−−→ M (C1 , . . . , Cm ) −−→ M B.

If this does not introduce confusion, the ambient structure can be omitted (J~[Link]) as well as the context
if we wish to use the canonical one (JtK).
Lemma 4.10 (Substitution lemma for terms). Let ~y .t be a term-in-context, with yi : Bi and t : C. Let
~s be a sequence of terms of same length and type as ~y , and ~x a context suitable for all the si ’s. Then
J~x.t[~s/~y ]KM is the composition :
(J~
x.s1 KM ,...,J~
[Link] KM ) y .tKM
M (A1 , . . . , An ) −−−−−−−−−−−−−→ M (B1 , . . . , Bm ) −−−−→ M C.
J~

Proof. This is true when t is a variable yi by the universal property of products, and when t = f (t1 :
D1 , . . . , ts : Ds ) by associativity of composition.

Lemma 4.11 (Naturality lemma for terms). Let h : M −→ N be a Σ-structure homomorphism and ~x.t
be a term-in-context (with xi : Ai and t : B). Then the diagram
[Link]
J~
M (A1 , . . . , An ) MB

hA1 ×···×hAn hB

[Link]
J~
N (A1 , . . . , An ) NB

commutes.
Proof. This is similar to the previous lemma : it is obviously true when t is a variable xi and also
true when t = f (t1 : C1 , . . . , tm : Cm ) by the commutativity of the first diagram defining Σ-structure
homomorphisms.

As in tarskian first-order logic in Set, terms are easy to interpret, but in general, formulae will require
certain properties on the category to be interpretable :
Definition 4.12. Let C be a cartesian category and M ∈ Σ-Str(C). A formula-in-context ~x.φ is recursively
interpreted as a subobject of M (A1 , . . . An ) (if xi : Ai ) :
(i) If φ = R(t1 : B1 , . . . , tm : Bm ), J~x.φKM is the pullback :

J~x.φK MR
y

(J~
x.t1 K,...,J~
[Link] K)
M (A1 , . . . , An ) M (B1 , . . . , Bm )

(ii) If φ = (s = t) where s and t are of sort B, J~x.φKM is the equalizer :

[Link]
J~
J~x.φK M (A1 , . . . , An ) MB
[Link]
J~

19
 (iii) If φ = >, J~x.φKM is the top of SubC (M (A1 , . . . , An )) ;
(iv) If φ = (ψ ∧ χ), J~x.φKM is the pullback

J~x.φK J~x.ψK
y

J~x.χK M (A1 , . . . , An )

(v) If φ = ⊥ and C is coherent, J~x.φKM is the bottom of SubC (M (A1 , . . . , An )) ;

(vi) If φ = (ψ ∨ χ) and C is coherent, J~x.φKM is the union of J~x.ψK and J~x.χK ;
(vii) If φ = (ψ ⇒ χ) and C is Heyting, J~x.φKM is J~x.ψK ⇒ J~x.χK in SubC (M (A1 , . . . , An )) ;
(viii) If φ = ¬ψ and C is Heyting, J~x.φKM is ¬J~x.ψK in SubC (M (A1 , . . . , An )) ;
(ix) If φ = (∃y : B)ψ and C is regular, J~x.φKM is the image of the composition
π
J~x, y.ψK  M (A1 , . . . , An , B) −→ M (A1 , . . . , An )

(x) If φ = (∀y : B)ψ and C is Heyting, J~x.φKM is ∀π (J~x, y.ψK) with π : M (A1 , . . . , An , B) −→
M (A1 ,W. . . , An ) the projection ;
(xi) If φ = Vi∈I ψi and C is geometric, J~x.φKM is the union of the J~x.ψi K in SubC (M (A1 , . . . , An )) ;
(xii) If φ = i∈I ψi and SubC (M (A1 , . . . , An )) has arbitrary intersections, J~x.φKM is the intersection of
the J~x.ψi K.
The proofs of the analogues of lemmas 4.10 and 4.11 for formulae are akin and omitted :
Lemma 4.13 (Substitution lemma for formulae). Let ~y .φ be a formula-in-context interpretable in C (with
yi : Bi ) and ~s be a sequence of terms of same length and type as ~y . Let ~x be a context suitable for all the
si ’s (with xi : Ai ). Then for any M ∈ Σ-Str(C), there is an arrow J~x.φ[~s/~y ]KM −→ J~y .φKM such that

J~x.φ[~s/~y ]K J~y .φK

(J~
x.s1 K,...,J~
[Link] K)
M (A1 , . . . , An ) M (B1 , . . . , Bm )

is a pullback.
Lemma 4.14 (Naturality lemma for formulae). Let ~x.φ be a geometric formula-in-context interpretable
in C (with xi : Ai ) and h : M −→ N be a Σ-structure homomorphism. Then there is an arrow J~x.φKM −→
J~x.φKN such that
J~x.φKM M (A1 , . . . , An )

hA1 ×···×hAn

J~x.φKN N (A1 , . . . , An )
commutes.
Definition 4.15. Let M ∈ Σ-Str(C). A sequent σ = (φ `~x ψ) interpretable in C is satisfied in M when
J~x.φKM ≤ J~x.ψKM in SubC (M (A1 , . . . , An )), namely when the interpretation of ~x.φ is a subobject of the
interpretation of ~x.ψ. In this case, we write M  σ. If all the axioms of a theory T are satisfied in M , we
say that M is a T-model and write M  T.
Let T-Mod(C) be the full subcategory of Σ-Str(C) on T-models.

20
Lemma 4.16. Let T : C −→ D be a cartesian/regular/coherent/Heyting/geometric functor between
such categories. For every M ∈ Σ-Str(C) and every sequent σ interpretable in C such that M  σ,
Σ-Str(T )(M )  σ. The converse is true if T is conservative. In particular, if T is a regular/.../geometric
theory and T is a functor of the same kind, Σ-Str(T ) restricts to a functor T-Mod(T ) : T-Mod(C) −→
T-Mod(D).

Proof. T preserves the interpretations of formulae because it is of the appropriate kind. For example, if
T is coherent and φ = (ψ ∨ χ), T (JφKM ) = T (JψKM ∪ JχKM ) = T (JψKM ) ∪ T (JχKM ) since T preserves finite
unions ; whence T (JφKM ) = JφKΣ-Str(T )(M ) . T is always at least cartesian, so it always preserves order in
subobject lattices.
Notice that M  (φ `~x ψ) if and only if J~x.φ ∧ ψKM  J~x.φKM is an isomorphism. If Σ-Str(T )(M ) 
(φ `~x ψ), then T (J~x.φ ∧ ψKM ) = J~x.φ ∧ ψKΣ-Str(T )(M )  J~x.φKΣ-Str(T )(M ) = T (J~x.φKM ) is an isomorphism.
If T is conservative, this in turn implies that M  (φ `~x ψ).

4.2 A soundness theorem

The following definition introduces a deduction system providing rules for inferring the validity of sequents
from other sequents. The section ends with a soundness theorem, stating that these rules can only prove
sequents that are satisfied in all models of a given theory.

Definition 4.17. Rules are written in the form Γσ , Γ being a (possibly empty) list of sequents and σ the
sequent that can be inferred from the validity of the sequents in Γ. Obviously, the rules involving certain
symbols only concern the fragments of logic which include this symbol.

– The structural rules include the identity axiom

φ `~x φ

the substitution rule

φ `~x ψ
φ[~s/~x] `~y ψ[~s/~x]
where ~y includes all the variables of ~s, and the cut rule
(φ `~x ψ) (ψ `~x χ)
φ `~x χ
– The equality rules include the equality axiom

> `x x = x

and the replacement axiom

(~x = ~y ) ∧ φ `~z φ[~y /~x]

where ~z contains the variables of ~x and ~y and the free variables of φ ;

– The finite conjunction rules include the axioms

φ `~x > φ ∧ ψ `~x φ φ ∧ ψ `~x ψ

and the rule

(φ `~x ψ) (φ `~x χ)
φ `~x ψ ∧ χ
– The finite disjunction rules are the analogous

21
 ⊥ `~x φ φ `~x φ ∨ ψ ψ `~x φ ∨ ψ
and
(φ `~x χ) (ψ `~x χ)
φ ∨ ψ `~x χ
– The implication rules are the double rule
φ ∧ ψ `~x χ
ψ `~x φ ⇒ χ
yielding a rule for negation by setting χ = ⊥ and ¬φ = (φ ⇒ ⊥) ;
– The existential quantification rules are the double rule
φ `~x,y ψ
∃yφ `~x ψ
(under the assumption that the sequents are well-formed, namely y is not free in ψ) ;
– The universal quantification rules are the double rule
φ `~x,y ψ
φ `~x ∀yψ
– The infinitary conjunction and disjunction rules are the infinitary analogues of the finite conjunction
and disjunction rules ;
– The two remaining mixed axioms for coherent logic are the distributive axiom
φ ∧ (ψ ∨ χ) `~x (φ ∧ ψ) ∨ (φ ∧ χ)
(and its infinitary analogue for geometric logic) and the Frobenius axiom
φ ∧ ∃yψ `~x ∃y(φ ∧ ψ)
where y is not in ~x.
A sequent σ is provable in a theory T (or T-provable) if there is a derivation from the axioms of T to σ
in the appropriate fragment of logic.
Theorem 4.18 (Soundness theorem). Let T be a Horn (resp. regular, coherent, first-order, geometric)
theory and M be a model of T in a cartesian (resp. regular, coherent, Heyting, geometric) category. If σ
is a sequent which is provable in T then M  σ.
Proof. By induction on the height of the derivation tree leading to σ, it is enough to show that each rule
in definition 4.17 is sound, that is if M satisfies the sequents above the line then it satisfies the sequent
below it. This is in most cases trivial. For example, the rule
(φ `~x ψ) (φ `~x χ)
φ `~x ψ ∧ χ
is sound because if M satisfies the two sequents above the line, then J~x.φKM ≤ J~x.ψKM and J~x.φKM ≤
J~x.χKM in SubC (M (A1 , . . . , An )) and of course the universal property of the pullback yields J~x.φKM ≤
J~x.ψKM ∩ J~x.χKM = J~x.(ψ ∧ χ)KM .

Remark 4.19. Notice that the law of excluded middle > `~x φ∨¬φ does not appear in definition 4.17, since
adding it would make the soundness theorem false. Indeed, as said in the previous section, Grothendieck
toposes are Heyting categories and not boolean categories, which means that subobjects are not always
complemented. This is why one has to prove theorems intuitionistically in order for them to hold in every
topos.

22
5 Syntactic sites and classifying toposes
5.1 Syntactic categories and a completeness theorem
According to the soundness theorem, any sequent that is provable in a given theory T is true in T. A
converse of this, known as a completeness theorem, shall be proven using syntactic categories : any sequent
which is true in T is indeed provable.
Definition 5.1. Let T be a cartesian (resp. regular, coherent, first-order, geometric) theory over Σ. The
syntactic category CTcart (resp. CTreg , CTcoh , CTfo , CT ) has as objects the α-equivalence classes (see definition
4.4) of cartesian (resp. regular, ...) formulae-in-context {~x.φ} and as arrows {~x.φ} −→ {~y .ψ} (where ~x
and ~y are chosen disjoint) the T-provable equivalence classes [θ] of cartesian (resp. regular, ...) formulae
θ(~x, ~y ) which are T-provably functional, that is such that the sequents

φ `~x ∃~y θ
θ `~x,~y φ ∧ ψ
θ ∧ θ[~z/~y ] `~x,~y,~z ~y = ~z

are T-provable. The composite [γ] ◦ [θ] of composable arrows [θ] : {~x.φ} −→ {~y .ψ} and [γ] : {~y .ψ} −→
{~z.χ} is the class [∃~y (θ∧γ)] and the identity arrow of {~x.φ} is the class [φ∧~x0 = ~x] : {~x.φ} −→ {~x0 .φ[~x0 /~x]}.
Lemma 5.2. Let T be a cartesian (resp. regular, ...) theory.
(i) A morphism [θ] : {~x.φ} −→ {~y .ψ} is an isomorphism if and only if θ is T-provably functional from
{~y .ψ} to {~x.φ}.
(ii) [θ] is a monomorphism if and only if the sequent

θ ∧ θ[~x0 /~x] ` ~x = ~x0

is provable in T.
(iii) Any subobject of {~x.φ} is (isomorphic to one) of the form
x0 =~
[ψ∧~ x]
{~x0 .ψ[~x0 /~x]} −−−−−−→ {~x.φ},

with ~x.ψ a formula such that ψ `~x φ is provable in T. For two such subobjects [ψ] and [χ], we have
[ψ] ≤ [χ] (in SubCT ({~x.φ})) if and only if ψ `~x χ is provable in T.
Proof. (i) If [θ] is T-provably functional in the other direction, then [θ] : {~y .ψ} −→ {~x.φ} is clearly
the required inverse. Conversely, if [γ] is the inverse of [θ] then γ is T-provably equivalent to θ so
[γ] = [θ].
(ii) Form the kernel pair {~x, ~x0 .θ ∧ θ[~x0 /~x]} of [θ] and notice that the sequent is T-provable if and only
if the diagonal map {~x.φ} −→ {~x, ~x0 .θ ∧ θ[~x0 /~x]} is an isomorphism, which is the case if and only if
[θ] is a monomorphism.
(iii) Such a morphism is always monic by (ii). If [θ] : {~y .ψ} −→ {~x.φ} is a monomorphism, then again
(ii) ensures that ~x.∃~y θ is cartesian relative to T, and (i) shows that [θ] is an isomorphism over {~x.φ}
from {~y .ψ} to {~x.∃~y θ} (and indeed, φ ` ∃~y θ is provable in T by functionality). Moreover, if [ψ]
and [χ] are two such subobjects, then the only possible morphism over {~x.φ} from [ψ] to [χ] is
[ψ ∧ ~x = ~x0 ] : {~x.ψ[~x0 /~x]} −→ {~x.χ}, which is a morphism exactly when ψ ` χ is provable in T.

This identification between subobjects in a syntactic category and provability of sequents enables us
to directly prove :
Theorem 5.3. (i) If T is a cartesian theory, then CTcart is a cartesian category ;

23
 (ii) If T is a regular theory, then CTreg is a regular category ;
(iii) If T is a coherent theory, then CTcoh is a coherent category ;
(iv) If T is a first-order theory, then CTfo is a Heyting category ;
(v) If T is a geometric theory, then CT is a geometric category.

Now let us prove the completeness theorem which comes from the rich structure of syntactic categories.

Definition 5.4. Let T be a cartesian (resp. regular, coherent, first-order, geometric) theory over Σ. The
universal model MT is the Σ-structure in CT where :

– for each sort A, MT A is the object {x : A.>} ;

– for each function symbol f : A1 · · · An −→ B, MT f is the morphism
[f (x1 ,...,xn )=y]
{x1 : A1 , . . . , xn : An .>} −−−−−−−−−−→ {y : B.>} ;

– for each relation symbol R  A1 · · · An , MT R is the subobject

[R(x1 ,...,xn )]
{x1 : A1 , . . . , xn : An .R(x1 , . . . , xn )} −−−−−−−−→ {x1 : A1 , . . . , xn : An .>}.

Theorem 5.5. Let T be a cartesian (resp. regular, ...) theory over Σ. Then for any cartesian (resp.
regular, ...) formula-in-context ~x.φ, its interpretation in MT is the subobject J~x.φKMT = [φ] : {~x.φ} 
{~x.>}. Moreover, a cartesian (resp. regular, ...) sequent over Σ is satisfied in MT if and only if it is
provable in T.

Proof. The first part is an easy induction on the shape of φ. If σ is a sequent which is provable in T then
by soundness it is satisfied in MT , and if φ ` ψ is satisfied in MT then [φ] ≤ [ψ] and by lemma 5.2.(iii),
the sequent is provable in T.

Corollary 5.6 (Completeness theorem). Let T be a cartesian (resp. regular, ...) theory. Then any
sequent which is satisfied in all models of T in cartesian (resp. regular, ...) categories is provable in T.

5.2 Classifying geometric theories

Another strong result that can be proven with syntactic categories will be theorem 5.12, for which we
shall prove a lemma here.

Lemma 5.7. Let T be a cartesian (resp. regular, coherent, geometric) theory. Then, for any cartesian
(resp. regular, coherent, geometric) category D, the functor from Cart(CTcart , D) (resp. Reg(CTreg , D),
Coh(CTcoh , D), Geo(CT , D)) to T-Mod(D) which sends F to F (MT ) is an equivalence of categories.

Proof. By lemma 4.16, this functor is well-defined. Given a T-model M in D, define FM : CT −→ D

by letting FM ({~x.φ}) = J~x.φKM and FM ([θ]) be the morphism whose graph is J~x, ~y .θKM . This defines
a functor which is cartesian (resp. regular, coherent, geometric). The functoriality of the assignment
M 7→ FM is a consequence of lemma 4.14. Clearly, FM (MT ) ∼ = M naturally in M . Conversely, if we are
given a cartesian (resp. regular, coherent, geometric) functor F : CT −→ D with F (MT ) ∼ = M , then for
every ~x.φ there is an isomorphism F ({~x.φ}) ∼
= J~x.φKM , yielding a natural isomorphism F ∼
= FM , naturally
in F .

Let us also define Grothendieck topologies on some of the syntactic categories, since their corresponding
toposes will be useful later.

Definition 5.8. In a regular category, a covering family is a family of arrows with common codomain c
whose union of images is the maximal subobject of c (that is, idc ).

24
 – Let C be a regular category. The regular topology JCreg is the topology whose covering sieves are
those which contain a cover.
– Let C be a coherent category. The coherent topology JCcoh is the topology whose covering sieves are
those which contain a finite covering family.
– Let C be a geometric category. The geometric topology JC is the topology whose covering sieves are
those which contain a small covering family.

One can notice that all these topologies are subcanonical (see definition 2.4).

Proposition 5.9. Let C and D be regular (resp. coherent, geometric) categories. A cartesian functor
is regular (resp. coherent, geometric) if and only if it sends JCreg - (resp. JCcoh -, JC -) covering sieves to
covering families.

A useful tool in algebraic topology is the notion of classifying spaces. It turns out that a similar
construction is possible for (geometric) theories, and it is of great value when studying said theories.

Definition 5.10. Let T be a geometric theory. A classifying topos for T is a Grothendieck topos Set[T]
such that for every Grothendieck topos E we have an equivalence :

Geom(E, Set[T]) ' T-Mod(E)

natural in E in the sense that for every geometric morphism f : F −→ E, the induced diagram
'
Geom(E, Set[T]) T-Mod(E)

−◦f f∗

'
Geom(F, Set[T]) T-Mod(F)

commutes up to isomorphism. Clearly this implies the uniqueness, up to (canonical) isomorphism, of a

classifying topos for a given theory.

Remark 5.11. In the diagram of definition 5.10, set E = Set[T] to see that there is a universal T-model
U in Set[T] (the image of idSet[T] under the equivalence) such that every T-model in a Grothendieck topos
F appears as the pullback of U along a (unique up to isomorphism) geometric morphism f : F −→ Set[T]
(the image in Geom(F, Set[T]) of the model under the equivalence).

Several examples will be discussed later. One could legitimately ask why this definition is restricted
to geometric theories. Nothing keeps us from defining classifying toposes of non-geometric theories, but
the two following theorems give a convincing answer.

Theorem 5.12. (i) For any cartesian theory T, Psh(CTcart ) classifies T.

(ii) For any regular theory T, Sh(CTreg , JCreg
T
) classifies T.
coh coh
(iii) For any coherent theory T, Sh(CT , JCT ) classifies T.
(iv) For any geometric theory T, Sh(CT , JCT ) classifies T.

Proof. Let E be a Grothendieck topos and T a geometric theory. By Diaconescu’s equivalence, we have
Geom(E, Sh(CT , JT )) ' FlatJT (CT , E) ; and by lemma 2.26 this category is in turn equivalent to cartesian
JT -continuous functors CT −→ E. Proposition 5.9 shows that this is equivalent to Geo(CT , E), and lemma
5.7 concludes : Geom(E, Sh(CT , JT )) ' T-Mod(E). All these equivalences are natural in E, and the same
proof works when T is cartesian, regular or coherent.

Theorem 5.13. Every Grothendieck topos classifies a geometric theory.

25
Proof. Let (C, J) be a small site and E any Grothendieck topos. By Diaconescu’s theorem, Geom(E, Sh(C, J)) '
FlatJ (C, E) naturally in E. A good candidate for a theory classified by Sh(C, J) would then be a ”theory
TCJ of flat and J-continuous functors on C”.
The signature consists of one sort pcq for each object c ∈ C and one function symbol pf q : pcq −→ pdq
for each arrow f : c −→ d in C. The axioms are the following :

- Functoriality :

> `x:pcq pidc q(x) = x for every c ∈ C

> `x:pdom(g)q pf ◦ gq(x) = pf q(pgq(x)) for every composable f and g

- Filteringness (equivalent to flatness) :

_
> `[] (∃x : pcq)>
c∈C
_
> `x:pcq,y:pdq (∃z : peq)(pf q(z) = x ∧ pgq(z) = y) for every c, d ∈ C
f g
c←
−e→
−d
_
pf q(x) = pgq(x) `x:pcq (∃z : pdom(h)q) phq(z) = x for every parallel f, g : c −→ d
f h=gh

- J-continuity :
_
> `x:pcq (∃y : pdi q) pfi q(y) = x for every J-cover (fi : di −→ c)i∈I
i∈I

It is straightforward to check that TCJ -Mod(E) ' FlatJ (C, E), whence Sh(C, J) is a classyfing topos for
TCJ .

6 Theories of presheaf type

Theories classified by presheaf toposes are especially nice to work with, as this topos then has a canonical
site of definition which is simpler than the syntactic site. Knowing this and a remarkable duality theorem,
computations to switch between theories and topologies will become easy. From now on, theories will all
be assumed geometric.

Definition 6.1. A (geometric) theory T is of presheaf type if it is classified by a presheaf topos.

Example 6.2. Because of theorem 5.12, every cartesian theory is of presheaf type.

Definition 6.3. Let T be a theory. A model M ∈ T-Mod(Set) is finitely presentable if HomT-Mod(Set) (M, −) :
T-Mod(Set) −→ Set preserves filtered colimits (see definition A.7). In general, such an object is also
called compact. It is equivalent to ask that every epimorphic family with codomain M contains a finite
epimorphic subfamily.
A model M is presented by a geometric formula-in-context ~x.φ if the functor HomT-Mod(Set) (M, −) is
isomorphic to J~x.φK− : N 7→ J~x.φKN . Since φ is geometric, this implies that M is finitely presented.
Explicitely, an element of J~x.φKN is given by elements ai ∈ AiN such that φ holds for a1 , . . . , an . Thus,
M is presented by φ if and only if there are ai ∈ AiM , called the generators of M , such that φ holds for
a1 , . . . , an and such that for any N ∈ T -Mod(Set) and any bi ∈ AiN for which φ holds, there is a unique
f : M −→ N sending ai to bi for every 1 ≤ i ≤ n.

Theorem 6.4. Any theory of presheaf type T is classified by the presheaf topos [f.p. T-Mod(Set), Set].

26
Proof. Let T be classified by Set[T] ' [C, Set] with C a small category. By theorem A.19.(iv), we
can replace C by its Cauchy completion C. ˆ By Diaconescu’s equivalence, we have Flat(Cˆop , Set) '
Geom(Set, [C, Set]) ' T-Mod(Set). One can check that the compact objects of Flat(Cˆop , Set) are
ˆ
exactly the retracts of the representable presheaves, and since Cˆ is Cauchy-complete this states that
Cˆ ' (Flat(Cˆop , Set))fp , hence Set[T] ' [f.p. T-Mod(Set), Set].

Definition 6.5. Let (C, J) be a site. A J-irreducible object is an object whose only J-covering sieve is
the maximal one. J is said to be rigid if for every object c, the collection of arrows from J-irreducible
objects to c generates a J-covering sieve.

Theorem 6.6. Let (C, J) be a small subcanonical site such that yC (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.

Idea of proof. Only the if part is really important here. If J is rigid, the comparison lemma (theorem
2.11) applied to the trivial topology shows that Sh(C, J) ' Psh(C irr ). The only if part can be found in
[6], theorem 6.1.7, p.202.

Definition 6.7. If T is a theory, a formula-in-context ~x.φ is T-irreducible if {~x.φ} is JT -irreducible in CT .

Proposition 6.8. Let T be a theory of presheaf type. Then a model of T in Set is finitely presentable if
and only if it is presented by a T-irreducible geometric formula.

Proof. Since T is of presheaf type, there is a canonical equivalence

τ : Sh(CT , JT ) ' [f.p. T-Mod(Set), Set].

By theorems 6.6 and A.19.(iv), there is an equivalence Sh(CT , JT ) ' Psh(CTirr ) ' Psh(C
d irr
T ). The resulting
equivalence Psh(C
d irr ) ' [f.p. T-Mod(Set), Set] restricts to an equivalence
T
op
l:C
d irr ' f.p. T-Mod(Set).
T

Given {~x.φ} ∈ C irr

T , τ sends yCT ({~
x.φ}) = J~x.φKU (see remark 5.11 for the definition of U ) to yCT (l({~x.φ})) =
d
J~x.φKN (N being the universal model in [f.p. T-Mod(Set), Set], given by N A(M ) = M A, N f (M ) = M f
and N R(M ) = M R, which moreover verifies J~x.φKN (M ) = J~x.φKM ). So l({~x.φ}) is presented by ~x.φ.
Since all representables in presheaf toposes are irreducible, ~x.φ is T-irreducible. So C irr irr
T ' CT . l is then
d
irr op
an equivalence (CT ) ' f.p. T-Mod(Set), as required : this equivalence sends objects and morphisms of
CT to the models and homomorphisms that they represent.

Typically, theories of presheaf type are those with few enough axioms for such a big category as a
presheaf topos to be classifying it. We can expect that adding axioms amounts to removing sheaves from
a classifying topos, and this is indeed the case, known as the duality theorem.

Definition 6.9. Let T be a theory. A quotient of T is a theory T0 such that each axiom of T is provable
in T0 . Two theories T and S are syntactically equivalent (denoted T ≡s S) if every (geometric) sequent is
provable in T exactly when it is provable in S.

Theorem 6.10 (Duality theorem). Let T be a theory. There is a bijection between quotients of T modulo
syntactic equivalence and subtoposes of Set[T], sending a quotient T0 to its classifying topos.

Ideas of the proof. Let T0 be a quotient of T obtained by adding (geometric) axioms of the form φ `~x ψ.
Given a Grothendieck topos E and M ∈ T-Mod(E), the functor FM : CT −→ E sends the monomorphism
x0 =~
[φ∧ψ∧~ x]
{~x0 .φ ∧ ψ} −−−−−−−−→ {~x.φ} to an epimorphism if and only if J~x.φKM ≤ J~x.ψKM , which is equivalent to
M  (φ `~x ψ). Thus, the JT -continuous flat functors CT −→ E which send each of these monomorphisms

27
to epimorphisms correspond to the T0 -models in E. Let JTT0 be the smallest Grothendieck topology on
CT containing the JT -covering sieves and the sieves containing such a monomorphism. By Diaconescu’s
equivalence, Sh(CT , JTT0 ) classifies T0 , and is also a subtopos of Set[T].
To show that this assignment does not depend on the syntactic equivalence class of the quotient, let
T1 and T2 be two syntactically equivalent quotients of T. Since they have the same models in every
Grothendieck topos E, we get an equivalence

Geom(E, Sh(CT , JTT1 )) ' FlatJT1 (CT , E) ' T1 -Mod(E)

= T2 -Mod(E) ' FlatJT2 (CT , E) ' Geom(E, Sh(CT , JTT2 ))

natural in E. It follows from a Yoneda-like lemma that Sh(CT , JTT1 ) and Sh(CT , JTT2 ) are equivalent over
Psh(CT ), hence they represent the same local operators and JTT1 = JTT2 .
Let Sh(CT , J)  Sh(CT , JT ) be a subtopos and TJ the quotient of T with additional axioms the
(geometric) sequents ψ `~y ∃~xθ, where [θ] : {~x.φ} −→ {~y .ψ} is a monomorphism generating a J-covering
sieve. One can show that the natural equivalence T-Mod(E) ' FlatJT (CT , E) restricts to an equivalence
TJ -Mod(E) ' FlatJ (CT , E), thus Sh(CT , J) classifies TJ .
T
It is clear that for any topology J on CT we have J = JTTJ , so we are left to show that T0 ≡s TJT0
T
for any quotient T0 of T. Notice that given a Grothendieck topos E, the T0 -models in E and the TJT0 -
models in E both correspond to the JTT0 -continuous flat functors CT0 −→ E. Now let UTT0 be the image of
aJ T0 ◦ yCT ∈ FlatJ T0 (CT , Sh(CT , JTT0 )) under the equivalence with T0 -Mod(Sh(CT , JTT0 )). This model is both
T T
T T
a T0 - and a TJT0 -universal model, and one can deduce that T0 ≡s TJT0 as required.

Definition 6.11. According to this theorem, the (syntactic equivalence classes of) quotients of a theory T
correspond to the topologies on Psh(CT ) which contain JT . If T0 is a quotient of a theory T, the topology
JTT0 on Psh(CT ) as in the theorem is called the associated T-topology of T0 . In the light of theorem 6.4,
when T is of presheaf type this is equivalently a topology on f.p. T-Mod(Set)op .

To make the computation T0 7→ JTT0 convenient in the setting where T is of presheaf type, we shall
state a theorem making this topology more explicit when T0 is presented in the right form.

Definition 6.12. Let T be a theory. Let ~x.φ and ~y .ψ be formulae representing models Mφ , Mψ ∈
f.p. T-Mod(Set). Let θ be provably functional {~y .ψ} −→ {~x.φ}. Then for any N ∈ T -Mod(Set),
JθKN ⊂ JψKN × JψKN is the graph of a map JψKN −→ JφKN . If ~a ∈ JψKMψ is the tuple of generators of
Mψ , then there is a unique ~b ∈ JφKMψ such that (~a, ~b) ∈ JθKMψ . Since ~x.φ presents Mφ , there is a unique
homomorphism sθ : Mφ −→ Mψ sending the generators of Mφ to ~b. Call this sθ the arrow presented by θ.

Theorem 6.13. Let T be a theory of presheaf type. Let ~xi .φi (i ∈ I) be formulae presenting models
Mi ∈ f.p. T-Mod(Set). For each i ∈ I, let ~yij .ψij and θij (j ∈ Ji ) be formulae where each ψij presents a
model Mij ∈ f.p. T-Mod(Set) and each θij is T-provably functional from ψij to φi . Then the quotient T0
obtained from T by adding the axioms _ j j
φi `~xi ∃~yi θi
j∈Ji

for i ∈ I has as its associated T-topology the topology on f.p. T-Mod(Set)op generated by the sieves Si ,
where each Si is the dual of the cosieve on Mi generated by the arrows sji : Mi −→ Mij presented by θij .

Ideas of the proof. Let J be the induced T-topology of T0 on f.p. T-Mod(Set)op and J 0 the topology
generated by the sieves Si . Also write σi for the axiom displayed in the theorem. We have to show that
J = J 0.
Let F : f.p. T-Mod(Set)op −→ E be a flat functor into a Grothendieck topos E, and MF the T-model
in E naturally corresponding to F via Diaconescu’s equivalence and the fact that [f.p. T-Mod(Set), Set]

28
classifies T. One easily shows that F (Mi ) = J~xi .φi KMF and that the graph of F (sji ) is J~yij , ~xi .θij KMF . From
this and the equivalence
T0 -Mod(E) ' FlatJ (f.p. T-Mod(Set)op , E)
we can show that any functor F ∈ FlatJ (f.p. T-Mod(Set)op , E) sends each Si to an epimorphic family.
Apply this and lemma 2.27 to the geometric morphism

Sh(f.p. T-Mod(Set)op , J)  [f.p. T-Mod(Set), Set]

to see that the sheafification aJ : [f.p. T-Mod(Set), Set] −→ Sh(f.p. T-Mod(Set)op , J) sends each monomor-
phism Si  Homf.p. T-Mod(Set) (Mi , −) to an isomorphism, hence J 0 ⊂ J.
To see that J = J 0 it is in fact enough now to show that for any Grothendieck topos E,

FlatJ 0 (f.p. T-Mod(Set)op , E) ⊂ FlatJ (f.p. T-Mod(Set)op , E).

Since J 0 contains the Si ’s, the T-model corresponding to F ∈ FlatJ 0 (f.p. T-Mod(Set)op , E) is already a
T0 -model. Since T0 -Mod(E) ' FlatJ (f.p. T-Mod(Set)op , E), F is J-continuous.

Because it is noteworthy, we state a last theorem to underline the simplicity of presheaf type theories
:
Theorem 6.14. Let T be a theory of presheaf type and A a full subcategory of f.p. T-Mod(Set). Then
the A-completion TA of T (the theory of geometric sequents valid in all models in A) is of presheaf type,
classified by [A, Set].
Proof. The inclusion A  f.p. T-Mod(Set) induces a canonical geometric inclusion

i : [A, Set]  Set[T].

The quotient of T corresponding to this subtopos is exactly the collection of sequents which hold in every
model in A.

7 The Zariski topos

From this section onwards, we take a look at examples of classifying toposes in algebraic geometry. The
first example is the Zariski topos, which is one of the most natural toposes to consider when dealing with
schemes.
Definition 7.1. Let k be a (commutative, unitary) ring. A finitely presented k-algebra is a k-algebra of
the form k[X1 , . . . , Xn ]/(f1 , . . . , fm ).SA morphism of schemes f : T −→ S is locally of finite presentation
if there is an affine open cover T = i∈I Ui with Ui = Spec Ai and affine open subsets Vi = Spec Ki ⊂ S
for i ∈ I such that for all i, f (Ui ) ⊂ Vi and the induced ring homomorphisms Ki −→ Ai make every Ai
into a finitely presented Ki -algebra.
Definition 7.2. Let S be a scheme. The (big) Zariski site is the category ZAR∗ (S) with objects the
affine schemes Spec A −→ S locally of finite presentation over S and scheme morphisms over S, and with
a sieve R on T = Spec A being in JZAR∗ (T ) if there are a1 , . . . , ak ∈ A with sum 1 and such that all the
duals of localizations (A −→ A[a−1
i ])
op are in R.

The resulting topos SZAR = Sh(ZAR∗ (S), JZAR∗ ) is the big Zariski topos of S.
Remark 7.3. In general, the Zariski site ZAR(S) has all schemes locally of finite presentation Sover S,
and a sieve is JZAR -covering if it contains immersions of open subsets Ui  T such that T = i∈I Ui .
The comparison lemma (theorem 2.11) shows that the resulting topos is equivalent when only taking
affine schemes (Sh(ZAR(S), JZAR ) ' Sh(ZAR∗ (S), JZAR |ZAR∗ (S) )), and the Grothendieck topology JZAR
restricted to ZAR∗ (S) is in fact the same as JZAR∗ defined above.

29
 When S is an affine scheme, there is a simple syntactic presentation for SZAR (that is, a theory
classified by SZAR ) which shall be given here. In the general case, it appears that the simplest theory we
know to be classified by SZAR is quite intricate and can be found in [9], theorem 3.7.6, p.33.
Until the end of this section, let K be a ring and S = Spec K.
Lemma 7.4. There is an equivalence of categories ZAR∗ (S) ' (K−Alg)op
fp .

Proof. Since Spec gives an equivalence between the affine schemes and the opposite of the category of
rings, the claim follows from the observation that Spec A −→ Spec K is locally of finite presentation if
and only if A is a a finitely presented K-algebra.

Lemma 7.5. JZAR∗ is generated (on (K−Alg)op

fp ) by the families of duals of localizations :

op
K[X1 , . . . , Xn ]/(X1 + · · · + Xn − 1) −→ K[X1 , . . . , Xn , Xi−1 ]/(X1 + · · · + Xn − 1)

for 1 ≤ i ≤ n.
Proof. Any family of duals of localizations (A −→ A[a−1 op with
Pn
i ]) i=1 ai = 1 as in definition 7.2 is the
pullback in ZAR∗ (S) of this universal family along the suitable K[X1 , . . . , Xn ]/(X1 + · · · + Xn − 1) −→ A
sending Xi to ai .

Definition 7.6. The theory K of K-algebras is the theory of rings (see example 4.7.(iii)) with one new
constant symbol cλ : A for every λ ∈ K, with the axioms

> `[] c0 = 0 > `[] c1 = 1

> `[] cλ + cµ = cλ+µ > `[] cλ × cµ = cλµ

for every λ, µ ∈ K. The quotient of this theory obtained by adding the locality axiom (see example
4.7.(iii)) is the theory loc−K of local K-algebras.
Lemma 7.7. The finitely presentable models in K -Mod(Set) are exactly the finitely presented K-algebras.
Proof. It is easy to see that K[X] is finitely presentable. Since any A = K[X1 , . . . , Xn ]/(f1 , . . . , fm ) can
be constructed from K[X] by finite colimits, the finitely presented algebras are all finitely presentable
K-models. This comes from the fact that K[X1 , . . . , Xn ] = K[X]⊗n and A is then the coequalizer of
Xi 7→ fi and Xi 7→ 0.
Let A ∈ f.p.K -Mod(Set). The set I of finitely generated sub-K-algebras (that is, quotients of poly-
nomial rings K[X1 , . . . , Xk ]) of A if clearly a filtered category, and the inclusions to A form a cocone in
K -Mod(Set). We get a canonical homomorphism colimB∈I B −→ A. It is surjective since every a ∈ A is
in the image of K[X] −→ A mapping X to a, and injective since two elements a1 ∈ A1 and a2 ∈ A2 can
be mapped into a common finitely generated subalgebra of A. Since A is finitely presentable, there is an
image of idA under the isomorphism

HomK -Mod(Set) (A, A) ∼

= HomK -Mod(Set) (A, colimB∈I B) ∼
= colimB∈I HomK -Mod(Set) (A, B)

which has to be a section of some inclusion B ⊂ A with B ∈ I, hence A ∈ I and A is finitely generated.
Let q : K[X1 , . . . , Xn ] −→ A be a surjective K-algebra homomorphism, which exists since we just
showed that A is finitely generated. Again, the set J of finitely generated ideals of K[X1 , . . . , Xn ] contained
in the kernel of q is a filtered category. In the same manner, we get a homomorphism

colimj∈J K[X1 , . . . , Xn ]/j −→ A

which is an isomorphism as well. Again, since A is finitely presentable, take the image of idA under the
isomorphism
HomK -Mod(Set) (A, A) ∼
= colimj∈J HomK -Mod(Set) (A, K[X1 , . . . , Xn ]/j)

30
to see that there is a finitely presented K-algebra B = K[X1 , . . . , Xn ]/j and a section s : A −→ B of the
quotient qB : B −→ A. Notice that for any B 0 = K[X1 , . . . , Xn ]/l with l ⊃ j in J we have qB 0 rs = idA . To
see that A is finitely presented, we just need to see that there is a B 0 isomorphic to A, that is such that
rsqB 0 = idB 0 . Since B is finitely presented, it is in f.p.K -Mod(Set) and as before, there is an isomorphism

coliml∈J HomK -Mod(Set) (B, K[X1 , . . . , Xn ]/l) ∼

= HomK -Mod(Set) (B, A).

Since sqB and idB are equal in the right hand side, they are in the left hand side. So there is B 0 with
rsqB = r. Thus, rsqB 0 r = rsqB = r and since r is surjective, rsqB 0 = idB 0 , so B 0 ∼
= A and A is indeed
finitely presented.

Remark 7.8. Since it is algebraic, the theory of K-algebras is of presheaf type (see theorem 5.12). Also,
the finitely presentable models of K are exactly the finitely presented K-algebras. Hence, [f.p.K -Mod(Set), Set] '
Psh(ZAR∗ (Spec K)).
Theorem 7.9. The Zariski topos SZAR of an affine scheme S = Spec K classifies the theory of local
K-algebras.
Proof. According to the above remark, it is enough to prove that JZAR∗ is the induced K-topology on
f.p.K -Mod(Set) of the theory loc−K. Fortunately, the locality axioms are of the required form
_
φn `~xn ∃~yni θni
1≤i≤n

as in theorem 6.13, with :

φn = (x1 + · · · + xn = 1)
ψni = (x01 + · · · + x0n = 1) ∧ (x0i × y = 1)
θni = ψni ∧ (x1 = x01 ) ∧ . . . ∧ (xn = x0n ).

Since the model Mφn = K[X1 , . . . , Xn ]/(X1 + · · · + Xn − 1) is presented by φn and the model Mψni =
K[X1 , . . . , Xn , Xi−1 ]/(X1 + · · · + Xn − 1) is presented by ψni , it is enough to show that θni presents the
corresponding localization homomorphism Mφn −→ Mψni . Set x0i to be Xi and y to be Xi−1 in the
presentation ψni of Mψni to see that θni is the unique morphism Mφn −→ Mψni sending Xi to Xi , that is
the localization.

Remark 7.10. In particular, let K = Z to notice that the (usual) local rings are exactly the points of the
Zariski topos (Spec Z)ZAR .

8 The crystalline topos

In this section we present another topos used in algebraic geometry, playing a key role in crystalline
cohomology. The interest is that the crystalline topos involves more data, which makes a syntactic
presentation harder to find than for the Zariski topos. In rings of characteristic p > 0, it is not possible
to divide by p hence the polynomial derivative is never surjective. To overcome this, there is a notion of
divided powers structure which will allow us to divide by p. Once again, only the affine case is treated,
the general result can be found in [9], theorem 5.8.3, p.75.
Definition 8.1. Let A be a ring and I ⊂ A an ideal. A divided powers structure (or PD-structure) γ on
I is a family (γn )n∈N of maps I −→ I such that for all n, m ≥ 0, a ∈ A and x, y ∈ I :
(i) γ0 (x) = 1 and γ1 (x) = x ;
(ii) γn (x)γm (x) = (n+m)!
n!m! γn+m (x) ;

31
(iii) γn (ax) = an γP
n (x) ;
(iv) γn (x + y) = ni=0 γi (x)γn−i (y) ;
(nm)!
(v) γn (γm (x)) = n!(m!) n γnm (x).

The numbers (n+m)! (nm)!

n!m! and n!(m!)n are always integers. Typically, γn (x) should be thought of as a legitimate
way to write xn /n!. The data (A, I, γ) is called a divided powers ring (or PD-ring). A divided powers
homomorphism (A, I, γ) −→ (B, J, δ) is a ring homomorphism A −→ B sending I into J and commuting
with the PD-structures. This defines the category PDRing of PD-rings. (A, I, γ)-algebras are defined as
the coslice category (A, I, γ)/PDRing.
The ideal I is PD-generated by a subset S ⊂ I if it is generated as an ideal by the γn (s) for s ∈ S and
n ≥ 1.
The polynomial ring A[X] has a natural PD-structure (I[X], γ 0 ) such that (A, I, γ)-algebra homomor-
phisms (A[X], I[X], γ 0 ) −→ (B, J, δ) correspond to the elements of B. Similarly, define the PD-polynomial
algebra AhXi as the A-module freely generated by the γn (X) for n ≥ 0, with the PD-ideal generated by
I and the γn (X) for n ≥ 1. The (A, I, γ)-algebra homomorphisms AhXi −→ (B, J, δ) correspond to the
elements of J.
Definition 8.2. We turn definition 8.1 into actual geometric theories.
(i) Let R be the theory of rings (see example 4.7) ;
(ii) Let I be the theory of rings with a new relation symbol I  A and the axioms

> ` I(0)
I(x) ∧ I(y) `x,y I(x + y)
I(x) `λ,x I(λ × x)

(iii) Let nil be the additional axiom I(x) `x n∈N xn = 0 ;

W
(iv) Let PDI be the theory of rings with a new sort SI and new functions symbols i : SI −→ A, 0 : SI ,
+ : SI × SI −→ SI , × : A × SI −→ SI and γn : SI −→ SI for n ≥ 0, the axioms stating that i is an
A-module homomorphism, and the axioms

i(x) = i(y) `x,y:SI x = y

> `x γ0 (x) = 1
> `x γ1 (x) = x
(n + m)!
> `x,y i(γn (x))γm (x) = γn+m (x)
n!m!
> `λ,x γn (λ × x) = λn × γn (x)
Xn
> `x,y γn (x + y) = i(γi (x)) × γn−i (y)
i=0
(nm)!
> `x,y γn (γm (x)) = γnm (x)
n!(m!)n
(v) Define PD by extending the theory R + I with the extension PDI and the axiom

∃x : SI , i(x) = y a`y I(y)

to state that the inclusion i is the inclusion of the ideal I (we get two theories R + I + PD and
R + PDI which are syntactically equivalent, so they are in particular Morita-equivalent) ;
(vi) Let K be a ring a R a K-algebra. Let (K, R)−Alg be the disjoint union of the theories of K-algebras
and R-algebras, with a new function symbol f : A −→ B (A being the sort of the K-algebras and
B the sort of the R-algebras) and axioms stating that f is a K-algebra homomorphism ;

32
 (vii) Let surj be the additional axiom > `y:B ∃x : A, f (x) = y and (K, R)−Quot = (K, R)−Alg + surj ;
(viii) If I ⊂ K is an ideal, let II be the extension of the theory of K-algebras by I (see (ii)) and the axiom
> `λ I(cλ ) (see definition 7.6) for every λ ∈ I ;
(ix) If (K, I, δ) is a PD-ring, let PDδ be the extension of II by PD (see (v)) and the axioms i(x) =
cλ `x:SI i(γn (x)) = cδn (λ) for λ ∈ I.
Lemma 8.3. Let (A, I, γ) be a PD-ring. If I is PD-generated by nilpotent elements, then it is a nilpotent
ideal.
Proof. It is enough to show that if a ∈ I is nilpotent, then every γn (a) is nilpotent. Let m ≥ 1 be such
that am = 0.
Compute on the canonical PD-structure on Q[X] :
1 (kn − m)!
γn (X)k = k
X kn = γkn−m (X)X m .
(n!) (n!)k
(kn−m)!
Notice that (n!)k
is an integer when k is large enough, hence this stays true in ZhXi ⊂ Q[X]. After
applying the unique PD-morphism ZhXi −→ A sending X to a (see definition 8.1), we get γn (a)k =
(kn−m)!
(n!)k
γkn−m (a)am = 0.

Definition 8.4. A PD-scheme is a triple (S, I, γ) where S is a scheme, I ⊂ OS is a quasi-coherent sheaf

of ideals (every I(U ) is a sub-OS (U )-module of OS (U ), the restriction maps of I are compatible with
those of OS and for each x ∈ S there is an open neighborhood U in which there is an exact sequence
OS⊕I |U −→ OS⊕J |U −→ I|U −→ 0) and γ is a PD-structure on I, that is such that every (OS (U ), I(U ), γ)
is a PD-ring. Equivalently, this is a model of PD in Sh(S).
It is a theorem of basic algebraic geometry that the quasi-coherent sheaves of ideals I ⊂ OS correspond
bijectively with closed immersions i : U −→ S, by I = Ker(i] ). Thus, given a PD-scheme (S, I, γ) there
is a natural closed immersion V (I) −→ S whose comorphism has kernel I.
A morphism of PD-schemes (S, I, γ) −→ (S 0 , I 0 , γ 0 ) is a morphism of schemes f : S −→ S 0 such that
f ] : f ∗ OS 0 −→ OS is a PD-model homomorphism. Explicitely, it means that (f −1 I 0 )OS ⊂ I and that
every (OS 0 (U 0 ), I 0 (U 0 ), γ 0 ) −→ (OS (f −1 U 0 ), I(f −1 U 0 ), γ) with U 0 open in S 0 is a PD-homomorphism. In
particular, such a morphism induces a morphism between the closed immersions V (I) −→ V (I 0 ).
0
AS morphism of PD-schemes
0
S S −→ S is locally of finite PD-presentation if there are affine open covers
S = Spec Ai and S = Spec Kj such that for every i there is a map Spec Ai −→ Spec Kji whose
induced Kji −→ Ai is of the form (K, I, γ) −→ KhX1 , . . . , Xn i[Y1 , . . . , Ym ]/(r1 , . . . , rk ).
A PD-thickening is a PD-scheme (S, I, γ) such that the PD-model (OS , I, γ) in Sh(S) satisfies the
axiom nil.
If (S, I, γ) is a PD-scheme and X −→ V (I) is a morphism of schemes, a PD-thickening over S
and X is a PD-thickening (T, J, δ) together with a PD-morphism (T, J, δ) −→ (S, I, γ) and a morphism
of schemes V (J) −→ X over S. A morphism of PD-thickenings over S and X is a PD-morphism
(T, J, δ) −→ (T 0 , J 0 , δ 0 ) over (S, I, γ) such that V (J) −→ V (J 0 ) is a morphism over X :

V (J) T

V (J 0 ) T0

X V (I) S

The (big) crystalline site Cris(X/S) is the category of PD-thickenings over X and S for which T −→ S
is locally of finite PD-presentation, and their morphisms, with the same topology as in definition 7.2 : a

33
sieve S
on (T, J, δ) is in the topology if it contains the inclusions (Ti , J|Ti , δ|Ti )  (T, J, δ) of an open cover
T = Ti . As in definition 7.2 and remark 7.3, thanks to the comparison lemma (theorem 2.11) we can
restrict to the affine schemes without changing the resulting topos, which we call (X/S)Cris .
Proposition 8.5. Let T be a theory of presheaf type and A a sort of the signature of T. Then the theory
T0 obtained by adding a constant symbol c : A is also of presheaf type, and the finitely presentable models
of T0 are exactly the finitely presentable models of T.
Ideas of proof. Let MT be the universal model in the classifying topos Set[T]. Then one can show that
T0 is classified by Set[T]/JAKMT . If Set[T] = Psh(C), then the equivalence
Z
Psh(C)/X ' Psh( X)
C

taken at X = JAKMT shows that T0 is of presheaf type. Notice that there is an equivalence T0 -Mod(Set) '
R T -Mod(Set)
JAK− over T -Mod(Set). The functor JAK− preserves filtered colimits, and one can deduce that
R T -Mod(Set)
the projection functor π : JAK− −→ T -Mod(Set) preserves and reflects compact objects.

Lemma 8.6. Let (K, I, γ) be a PD-ring. The finitely presentable models of the theory T0 of K-algebras
+II + PDγ are exactly the PD-rings over K of the finite PD-presentation form :

KhX1 , . . . , Xn i[Y1 , . . . , Ym ]/(r1 , . . . , rk ).

Proof. The theory T0 is syntactically equivalent to a Horn theory, up to adding constants. But the
finitely presentable models of a Horn theory are all presented by a Horn formula (see proposition 6.8).
Here, ~x : SIn , ~y : Am .> presents KhX1 , . . . , Xn i[Y1 , . . . , Ym ]. Since PDγ asks the interpretation of the
symbol i to be injective, any atomic formula is provably equivalent to one of the form r = 0 where r is
a term representing an element of KhX1 , . . . , Xn i[Y1 , . . . , Ym ]. A Horn formula is just a conjunction of
atomic formulae, which concludes.

Lemma 8.7. Let (K, I, γ) be a PD-ring with I finitely PD-generated, and R be a finitely presented K/I-
algebra. Let T = (K, R)−Quot + PDγ + nil. Then T is of presheaf type and its finitely presentable models
are the (A, J, δ, B = A/J) where (A, J, δ) is of finite PD-presentation over (K, I, γ).
Sketch of proof. Let T0 be the cartesian theory of K-algebras + II + PDγ . By lemma 8.6, the objects of
f.p.T0 -Mod(Set) are the PD-rings of finite presentation over (K, I, γ). Since every T0 -model in Set gives
exactly one T0 -model (with T0 = (K, K/I)−Quot + PDγ + nil), the forgetful functor f.p.T0 -Mod(Set) −→
f.p.T0 -Mod(Set) is an equivalence of categories. Since R is a finitely presented K/I-algebra, proposition
8.5 ensures that (K, R)−Quot + PDγ is of presheaf type, with finitely presentable models those of finite
PD-presentation over K.
Now let M = (A, J, δ, B = A/J) be a finitely presentable ((K, R)−Quot + PDγ )-model in Set. Since
I is finitely PD-generated and A is of finite PD-presentation over K, J is also finitely PD-generated. Let
(a1 , . . . , an ) be a family of generators of J. Let Jnil be the induced ((K, R)−Quot + PDγ )-topology of T.
Then the covering sieve Si given by theorem 6.13 is the cosieve of all M −→ M 0 sending ai to a nilpotent
element. It is generated by the family M −→ (A/Jn , J/Jn , γ, B) where Jn is the ideal PD-generated by
ani . Each of these models are still finitely generated, and their ideal J/Jn are each PD-generated by the
images of the PD-generators of J. This gives a cover of M by models where the PD-ideal is PD-generated
by nilpotent elements, and thanks to lemma 8.3, these ideals are nilpotent. This shows that Jnil is a rigid
topology, hence by theorem 6.6 T is of presheaf type.

Lemma 8.8. Let (K, I, γ) be a PD-ring and R a K/I-algebra. Let T = (K, R)−Quot + PDγ + nil.
The topology on T-Mod(Set)op seen as a full subcategory of Cris(Spec R/ Spec K) has cosieves on ob-
jects (A, J, δ, B = A/J) those which contain the canonical localization arrows (A, J, δ, B = A/J) −→
(A[a−1 −1
i ], Jai , δai , B[ai ]) with (a1 , . . . , an ) = A.

34
Proof. A cosieve on (A, J, δ, B = A/J) is covering if it generates a covering sieve in Cris(Spec R/ Spec K).
Such a sieve contains an open cover of Spec A if and only if it contains a cover by principal open subsets
D(ai ), if and only if (a1 , . . . , an ) = A.

Theorem 8.9. Let (K, I, γ) be a PD-ring with I finitely PD-generated, and R a finitely presented K/I-
algebra. Then the crystalline topos

(X/S)Cris = Sh(Cris(Spec R/ Spec K))

classifies the theory

(K, R)−Quot + PDγ + nil + loc
where loc is the axiom of locality (see example 4.7.(iii)).

Proof. Let T = (K, R)−Quot+PDγ +nil. Then Cris(Spec R/ Spec K)op is the subcategory of T-Mod(Set)
where A is of finite PD-presentation over K. By lemma 8.7, this is f.p. T-Mod(Set). Hence, the presheaf
topos
Psh(Cris(Spec R/ Spec K))
classifies T. Thanks to lemma 8.8, it is for the exact same reason as in theorem 7.9 that the induced
topology of T + loc on Cris(Spec R/ Spec K) is the topology defining (X/S)Cris .

35
A Categorical prerequisites
A.1 Glossary
Definition A.1. A category is small if its objects and morphisms form sets. A category is essentially
small if it is equivalent to a small category. A category is locally small if between any two objects there
is a set of morphisms.

Definition A.2. A functor F : C −→ D is full (resp. faithful) if given two objects c and d, the induced
map HomC (c, d) −→ HomC (F c, F d) is surjective (resp. injective). An embedding is a faithful functor that
is injective on objects ; every fully faithful functor is equivalent to a fully faithful functor that is injective
on objects. Given a category C, the full subcategory of C on the objects O ⊂ Objects(C) is the category
with objects O and all the morphisms from C between them.

Definition A.3. In a category, a family of morphisms with same codomain (fi : Xi −→ X)i is epimorphic
if for any two morphisms g, h : X −→ Y such that gfi = hfi for all i, we have g = h.

Definition A.4. A functor F is conservative if for any morphism f , F (f ) being an isomorphism implies
that f was already an isomorphism.

Definition A.5. A category is complete (resp. cocomplete) if it has all small limits (resp. all small
colimits).

Definition A.6. Two functors L : C −→ D and R : D −→ C are adjoint (denoted L a R, L is

the left adjoint and R is the right adjoint) if the functors HomD (L(−), −) and HomC (−, R(−)) are
naturally isomorphic. Under the isomorphism HomD (L(c), L(c)) ∼
= HomC (c, R(L(c))), the image of idL(c)
is called the unit of the adjunction and is denoted ηc : c −→ RLc. Dually, under the isomorphism
HomC (R(d), R(d)) ∼= HomD (L(R(d)), d), the image of idR(d) is called the counit and is denoted d :
LRd −→ d. These constructions give natural transformations η : idC −→ RL and  : LR −→ idD .

Definition A.7. A category C is filtered if every finite diagram has a cocone. Equivalently, if :

– there is an object of C ;
– for every objects c1 and c2 there are morphisms to a common object c1 −→ c3 and c2 −→ c3 ;
– for every pair of parallel arrows f, g : c1 −→ c2 there is an arrow h : c2 −→ c3 coequalizing f and g
(hf = hg).

Definition A.8. A cartesian closed category is a category with finite products and exponentials (that is,
each functor − × X has a right adjoint (−)X ).

Definition A.9. In a category C, a subobject of an object X is an equivalence class of monomorphisms

A  X, where A and B are equivalent when they are isomorphic in C/X. Since there is at most one
morphism in C/X between two such monomorphisms, the category of subobjects SubC (X) is a (a priori
large) poset.

Definition A.10. In a category C with finite limits, a subobject classifier is a monomorphism true : 1  Ω
from the terminal object such that for every monomorphism A  X in C there is a unique characteristic
morphism χA : X −→ Ω such that the corresponding square is a pullback :

!
A 1
y
true

X χA Ω

36
Definition A.11. The kernel pair of an arrow f : X −→ Y in a category with pullbacks is the pullback
of f along itself :
X ×Y X X
y
f

Y f
Y

The corresponding diagonal arrow is the arrow ∆ : X −→ X ×Y X given by the universal property of
pullbacks applied to the arrows idX and idX . It is easy to check that ∆ is an isomorphism if and only if
f is a monomorphism.

Definition A.12. In a category, an object A is a retract of B if there are morphisms i : A −→ B and

r : B −→ A such that ri = idA . A morphism e is idempotent if e ◦ e = e. Clearly, if r is a retraction of a
morphism i, then ir is idempotent. A split idempotent is an idempotent of this form.
Let C be a small category. Its Cauchy completion Cˆ is the full subcategory of Psh(C) on the retracts
of representable presheaves. A category is Cauchy-complete if every idempotent splits.

A.2 Results
Lemma A.13 (Yoneda’s lemma). Let C be a locally small category and yC : C −→ Psh(C) = [C op , Set] the
functor sending an object c to HomC (−, c). This is the image under the adjunction HomCAT (C op ×C, Set) '
HomCAT (C, [C op , Set]) of the functor HomC . Then for a presheaf X ∈ Psh(C), there is a canonical
isomorphism :
HomPsh(C) (yC (c), X) ∼
= X(c).

Proof. A natural transformation η ∈ HomC (−, c) −→ X is uniquely determined by the value ξ = ηc (idc ) ∈
X(c). Indeed, for any object b in C, the naturality of η implies that ηb must send an element f ∈ HomC (b, c)
to X(f )(ξ) ∈ X(b).

Corollary A.14. The Yoneda embedding yC is full and faithful, since it induces the following isomor-
phism for objects c and d :

HomPsh(C) (HomC (−, c), HomC (−, d)) ∼

= (HomC (−, d))(c) = HomC (c, d).

In particular, if yC (c) ∼
= yC (d) then this natural isomorphism comes from an isomorphism c ∼
= d.

Proposition A.15. Two functors L : C −→ D and and R : D −→ C are adjoint if and only if there exist
natural transformations η : idC −→ RL and  : LR −→ idD such that the following two triangles commute
:
Lη
L LRL R

L ηR
idL idR

R
L RLR R

Proof. Given f : Lc −→ d, the corresponding morphism f ] : c −→ Rd is the composite R(f ) ◦ ηc . In

the other way, given g : c −→ Rd the corresponding morphism g [ : Lc −→ d is given by d ◦ L(g). The

37
isomorphism f 7→ f ] follows from :
ηc R(f )
f ][ = (c −→ RLc −−−→ Rd)[
L(ηc ) LR(f )
d 
= Lc −−−→ LRLc −−−−→ LRd −→ d
L(ηc ) Lc  f
= Lc −−−→ LRLc −−→ Lc −→ d
f
= Lc −→ d.
The naturality of this isomorphism comes from the naturality of η and .

Theorem A.16. Let L : C −→ D : R be functors with L a R. Then L preserves all colimits and R
preserves all limits.
Proof. We only show this for R, as the fact for L is dual. Let Y be an object of D and X : J −→ C be a
diagram whose limit exists in C. Since the Hom functors preserve limits in the second argument, we have
:
HomD (Y, R(lim Xj )) ∼
= HomC (LY, lim Xj )
j∈J j∈J
∼
= lim HomC (LY, Xj )
j∈J
∼
= lim HomD (Y, RXj )
j∈J
∼
= HomD (Y, lim RXj ),
j∈J

naturally in Y . The Yoneda lemma concludes that R(limj∈J Xj ) ∼

= limj∈J RXj .
Converses to this theorem are called adjoint functor theorems, stating that under assumptions on the
categories or the functors involved, them preserving (co)limits suffices to ensure that they have adjoints.
A proof of the adjoint functor theorem used in remark 3.10 would be too long for its relevance.
Theorem A.17 (Finite limits commute with filtered colimits in Set). Let I be a finite category and J a
small filtered category. Then for any functor F : I × J −→ Set, the canonical arrow
κ : colimj∈J lim F (i, j) −→ lim colimj∈J F (i, j)
i∈I i∈I

is an isomorphism.
Proof. Notice that a
colimj∈J F (i, j) = F (i, j)/R,
j∈J

R being the equivalence relation where x ∈ F (i, j) and x0 ∈ F (i, j 0 ) are equivalent when there are
u : j −→ k and u0 : j 0 −→ k with F (i, u)(x) = F (i, u0 )(x0 ). Any finite family of such equivalence classes
((xm , jm )) (with xm ∈ F (i, jm )) can be rewritten as ((ym , k)) with a common k, since J is filtered. For
the same reason, if two items (y, k) and (y 0 , k) of this list are equivalent then there is w : k −→ k 0 such
that F (i, w)(y) = F (i, w)(y 0 ).
For any functor G : I −→ Set, limi∈I G(i) = Hom[I,Set] (∗, G) is the set of cones on G. Letting
G(i) = colimj∈J F (i, j), since I is finite every cone is a finite family of elements of colimj∈J F (i, j)
satisfying a finite number of equations. According to the remarks above, each cone τ is thus a family
(τi = (yi , k 0 ))i∈I for some common k 0 where the yi constitute a cone y : ∗ −→ F (−, k 0 ). Since the
equivalence class of y is an element of colimj∈J limi∈I F (i, j), we get a map
lim colimj∈J F (i, j) −→ colimj∈J lim F (i, j)
i∈I i∈I
0
τ 7−→ (y, k )

38
which can be checked to be the inverse of κ.

Proposition A.18. The following conditions are equivalent for an idempotent e : c −→ c :

(i) e splits as i ◦ r ;
(ii) the equalizer i of e and idc exists ;
(iii) the coequalizer r of e and idc exists.

Theorem A.19. Let C be a small category and Cˆ its Cauchy completion. Then

(i) Cˆ is small and C is a full subcategory of Cˆ ;

(ii) Cˆ is Cauchy-complete ;
(iii) the inclusion C  Cˆ is an equivalence if and only if C is Cauchy-complete ;
(iv) there is an equivalence Psh(C) ' Psh(C). ˆ

Proof. Ĉ is small because Psh(C) is well-powered, and C is a full subcategory because yC is full and
faithful. Every idempotent in Cˆ splits because it splits in Psh(C) and the composite of two retractions is
a retraction.
A retract of a representable presheaf yC (c) induces an idempotent on yC (c) and by the Yoneda lemma
an idempotent on c. If C is Cauchy-complete, this idempotent splits and already produces a retraction of
yC (c). So if C is Cauchy-complete then C ' Ĉ.
To prove the equivalence between the presheaf categories, it is enough to show that a presheaf F ∈
Psh(C) extends uniquely to a presheaf F̂ ∈ Psh(C). ˆ Since by proposition A.18 the category Set is already
Cauchy-complete, F̂ has to map the splitting of an idempotent e to the splitting of F e. If i : R  yC (c) : r
and j : S  yC (d) are retractions, every morphism f : R −→ S is equal to sjf ri. Since F̂ (i) and F̂ (s)
are already defined and since F̂ (jf r) has to be F (jf r), this determines uniquely the presheaf F̂ .

39
Bibliography
[1] Michael Artin, Alexandre Grothendieck, Jean-Louis Verdier, Théorie des topos et cohomologie
étale des schémas (SGA4), Springer-Verlag, 1972.

[2] Michael Barr, Toposes without points, Springer-Verlag, 1971.

[3] Ingo Blechschmidt, Using the internal language of toposes in algebraic geometry, [Link]
org/abs/2111.03685, 2017.

[4] Francis Borceux, Dominique Dejean, Cauchy completion in category theory, Cahiers de topologie
et géométrie différentielle catégoriques (tome 27), 1986.

[5] Olivia Caramello, Site characterizations for geometric invariants of toposes, [Link]
abs/1112.2542, 2011.

[6] Olivia Caramello, Theories, Sites, Toposes, Oxford University Press, 2018.

[7] Monique Hakim, Topos annelés et schémas relatifs, Springer-Verlag, 1972.

[8] Matthias Hutzler, Internal language and classified theories of toposes in algebraic geometry, 2018.

[9] Matthias Hutzler Syntactic presentations for glued toposes and for crystalline toposes, https://
[Link]/abs/2206.11244, 2022.

[10] Peter T. Johnstone, Sketches of an Elephant : A Topos Theory Compendium, Volume 2, Oxford
Logic Guides, 2002.

[11] Saunders Mac Lane, Categories for the Working Mathematician, Springer-Verlag, 1971.

[12] Saunders Mac Lane, Ieke Moerdijk, Sheaves in Geometry and Logic, Springer-Verlag, 1992.

[13] Conor Mahany, Elementary Topos Theory and Intuitionistic Logic, [Link]
~may/REU2012/REUPapers/[Link], 2012.
[14] The Stacks Project authors, The Stacks Project, [Link]

[15] Ravi Vakil, The Rising Sea, [Link] 2017.

[16] Gavin C. Wraith, Generic Galois theory of local rings (from the symposium Applications of
Sheaves), Springer-Verlag 1977.

40