8 ANDREJ SCEDROV
0.7. Geometric Morphisms. Geometric Theories. Classifying Topoi.
Let EtV be two Grothendieck topoi. By a geometric morphism
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| |
= 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
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)
as f*M for a unique (up to natural isomorphism) geometric morphism V + E .