FORCING AND CLASSIFYING TOPOI

5

where f(&i) denotes F(f)(ai), the value of the mapping F(C) - '» F(Cf)

at a. . The higher-order aspect of the language is interpreted as

F

follows: the sort Q is the power-sort of the sort F .

d°P

ff

op

We say that a sentence $ is true in S , and write S t= (J ,

if C II - (J ) at each object C of C . The truth-value | | f | f of a

formula f(x1,...,x ) is the subfunctor | | J11"* C ' Fn given by

Il4)| l (C) = {ai,...,an e Fn(C)lC lhf)(x1/.../xn)[a1,...fan]} .

When ( C is the trivial one-object category, the presheaf semantics

(Cop

in S specializes to the ordinary Tarski semantics.

0.5. Grothendieck Topologies. Sheaves. Grothendieck Topoi.

Let E be a small category. A Grothendieck topology on ( C is

defined by specifying a set J(X) of sieves on X (i.e. subfunctors

of hY ) called coverinq sieves of the topology, for each object X of

( C , such that:

(i) For any X , the maximal sieve {a| codomain (a) = X}

is an element of J(X) .

(ii) If R e J(X) , and Y * X is a morphism of E , then the

sieve

f*(R) = {Z + Y|fa e R}

is an element of J(Y) (closure under pullbacks).

(iii) If R G J(X) , and S is a sieve on X such that for each

Y I X in R we have f*(S) e J(Y) , then S e J(X) .

A small category equipped with a Grothendieck topology is called a site.

The following lemma is useful in the applications.

Lemma (folklore). Let K be a family of sieves in a small category E ,

and assume K is closed under pullbacks. Then the Grothendieck topology

J generated by K is the smallest family f sieves in C D that includes

K and satisfies (i) and (iii) above.

Let ((E,J) be a site, F a presheaf on E . We say that F is a

sheaf (for the topology J ), if for every object X of C , and every

R e J(X) :