8 ANDREJ SCEDROV

0.7. Geometric Morphisms. Geometric Theories. Classifying Topoi.

Let EtV be two Grothendieck topoi. By a geometric morphism

f f*

E •+ V we mean an adjoint pair f = (f*,f*) , where E -* • F , and f*

preserves finite limits (f* is called the inverse image of f).

A geometric formula of a first-order, multi-sorted infinitary

language with equalities is obtainable from atomic formulas by finite

conjunction (including the empty conjunction,T), possibly infinite dis-

junction (including the empty disjunction,X), and existential quantifi-

cation. If M is an interpretation in a Grothendieck topos F , E -* • F

a geometric morphism, and J a geometric formula, then the truth values

of cj ) in M and f*M satisfy |] j| |

fi[

= f*|| $\\ .

A geometric sequent is a sentence of the kind

Vx,.. .Vx (j (x,#,.. ,x ) — ^(x,,... ,x )) (we often write

J (x,,... ,x ) I— ^(x,,...,x )),where J and i( i are geometric formulas

and every variable free in j or \\ occurs in the list x,,...,x . A

geometric theory is a theory in the multi-sorted first-order language with

equalities, with classical logic, axiomatized by geometric sequents. If

f

E • F is a geometric morphism, and M a F-model of a geometric theory

T (i.e. a sheaf interpretation in F satisfying the axioms of T ),

then f*M is an E-model of T . Barr's theorem (cf. e.g. [Jo 1 ,§7.5])

implies that if a geometric sequent is deducible from certain others in

classical logic, then it is deducible from them in intuitionistic logic as

well. Hence, the geometric sequents provable in a geometric theory T

hold in all models of T in all Grothendieck topoi.

If T is a geometric theory, then there exists a Grothendieck topos

E , called the classifying topos of T , and there exists a model M of

T in E , called the universal model of T , such that, for any Grothen-

dieck topos F , the category of geometric morphisms T + E and natural

transformations n: f* • g* is equivalent to the category of models of

T in F and homomorphisms, the identity morphism of E corresponding

to the model M . Thus, M has the universal property that every model

of T in any Grothendieck topos F can be obtained (up to isomorphism)

f

as f*M for a unique (up to natural isomorphism) geometric morphism V + E .