学术文献库

We regard a geometric theory classified by a topos as a syntactic presentation for the topos and develop tools for finding such presentations. Extensions of geometric theories, which can add axioms, symbols and sorts, are treated as objects in their own right, to be able to build up complex theories from parts. The role of equivalence extensions, which leave the theory the same up to Morita equivalence, is investigated. Motivated by the question what the big Zariski topos of a non-affine scheme classifies, we show how to construct a syntactic presentation for a topos if syntactic presentations for a covering family of open subtoposes are given. For this, we introduce conditional theory extensions that require part of the data a model is made of only under some condition given in the form of a closed geometric formula. We also give a general definition for systems of interdependent theory extensions, to be able to talk about compatible syntactic presentations not only for the open subtoposes in a given cover but also for their finite intersections. An important concept for finding classified theories of toposes in concrete situations is that of theories of presheaf type. We develop several techniques for extending a theory while preserving the presheaf type property, and give a list of examples of simple extensions which can destroy it. Finally, we determine a syntactic presentation of the big crystalline topos of a scheme. In the case of an affine scheme, this is accomplished by showing that the biggest part of the classified theory is of presheaf type and transforming the site defining the crystalline topos into the canonical presheaf site for this theory, while the remaining axioms induce the Zariski topology. Then we can apply our results on gluing classifying toposes to obtain a classified theory even in the non-affine case.