The notion of geometric theory has many different incarnations. A few are:
A geometric theory is a first order theory whose axioms can be written solely in terms of the connectives (truth), (finite conjunction), (falsity), (possibly infinitary disjunction), and (existential quantification).
The equivalence of these statements involves some serious proofs, including Giraud's theorem characterizing Grothendieck topoi.
In logical terms, a geometric theory fits into a hierarchy of theories that can be interpreted in the internal logic of a hierarchy of types of categories. Since predicates in the internal logic are represented by subobjects, in order to interpret any connective or quantifier in the internal logic, one needs a corresponding operation on subobjects to exist in the category in question, and be well-behaved. For instance:
Finally, theories which also involve infinitary , which is again represented by an infinitary union, can be interpreted in infinitary coherent categories, aka geometric categories. These are geometric theories.
Note that the axioms of one of these theories are actually of the form
where and are formulas involving only the specified connectives and quantifiers, means entailment, and is a context. Such an axiom can also be written as
so that although and are not strictly part of any of the above logics, they can be applied “once at top level.” In an axiom of this form for geometric logic, the formulas and which must be built out of , , , , and are sometimes called positive formulas.
The interpretation of arbitrary uses of and requires a Heyting category. In fact, by the adjoint functor theorem for posets, any geometric category which is well-powered is automatically a Heyting category, but geometric functors are not necessarily Heyting functors. Likewise, a well-powered geometric category automatically has arbitrary intersections of subobjects as well, so we can interpret infinitary in its internal logic, but again these are not preserved by geometric functors.
By the usual syntactic constructions (see internal logic and context), any geometric theory generates a “free geometric category containing a model of that theory,” also known as its syntactic category . This syntactic category has the universal property that for any other geometric category , geometric functors are equivalent to -models in .
The theory of torsion-free abelian groups is also cartesian, being obtained from the theory of abelian groups by the addition of the sequents for all .
The theory of local rings is a coherent theory, being obtained from the theory of commutative rings by adding the sequent , for nontriviality, and
saying that if is invertible, then either or is so.
The theory of fields is also coherent, being obtained from the theory of commutative rings by adding and also
asserting that every element is either zero or invertible. In the constructive logic that holds internal to the categories in question, this is the notion of a “discrete field;” other classically equivalent axiomatizations (called “Heyting fields” or “residue fields”) are not coherent.
The theory of torsion abelian groups is geometric but not coherent; it can be obtained from the theory of abelian groups by adding the sequent
asserting that for each , either or or or …. Similarly, the theory of fields of finite characteristic is geometric but not coherent.
Categories of each “logical” type can also be “completed” with respect to a suitable “exactness” property, without changing their internal logic. Any regular category has an completion into an exact category (see regular and exact completion), any coherent category has a completion into a pretopos, and any geometric category has a completion into an infinitary pretopos.
However, Giraud's theorem says that an infinitary pretopos having a generating set is precisely a Grothendieck topos. Moreover, a functor between Grothendieck topoi is geometric (preserves all the structure of a geometric category) iff it preserves finite limits and small colimits. By the adjoint functor theorem, this implies that it is the inverse image part of a geometric morphism, i.e. an adjunction in which (the “inverse image”) preserves finite limits.
Grothendieck topoi and inverse-image functors are in some sense the “natural home” for models of geometric theories.
Note, though, that geometric morphisms are generally considered as pointing in the direction of the direct image , which is the opposite direction to the geometric functor . (This is because when and are the toposes of sheaves on sober topological spaces (or locales) and respectively, then continuous maps correspond precisely to geometric morphisms .) Also, of course any Grothendieck topos is an elementary topos (at least, as long as one works in foundations for which Set is an elementary topos), and hence its internal logic also includes “higher-order” constructions such as function-objects and power-objects. However, these are not preserved by geometric functors, so they (like and ) are not part of geometric logic. (They are, however, preserved by logical functors, a different sort of morphism between topoi.)
In particular, we can apply the “exact completion” operation to the syntactic category of a geometric theory to obtain an infinitary pretopos . As long as the theory was itself small, will have a generating set, and therefore will be a Grothendieck topos. The universal property of the syntactic category, combined with that of the exact completion, implies that for any Grothendieck topos , geometric morphisms are equivalent to -models in . This topos is called the classifying topos of .
In the other direction, if is any small site, we can write down a “geometric theory of cover-preserving flat functors .” By Diaconescu's theorem classifying geometric morphisms into sheaf topoi, it follows that is a classifying topos for this theory. Therefore, not only does every geometric theory have a [[classifying topos], every Grothendieck topos is the classifying topos of some theory. Very different-looking theories can have equivalent classifying topoi; this of course implies that they have all the same models in all Grothendieck topoi (hence a Grothendieck topos is the “extensional essence” of a geometric theory). We say that two geometric theories with equivalent classifying topoi are Morita equivalent.
Suppose we consider what sorts of “theories” we can define in terms of Grothendieck topoi, that are preserved by inverse image functors. Any such theory should certainly define a 2-functor , where is the 2-category of Grothendieck topoi and geometric morphisms, so for the moment let’s call any such a “theory”. The image of a functor is supposed to be “the category of -models,” and a classifying topos for such a 2-functor will be just a representing object for it.
Of course, this notion of theory is far too general; we only want to consider theories that are constructed in some reasonable way. One theory that should certainly be geometric is the theory of objects, . This 2-functor sends a topos to itself, considered as a mere category, and an inverse image functor to itself, considered as a mere functor. The theory can be shown to have a classifying topos, the object classifier . Similarly, we have a theory of -tuples of objects that should be geometric.
How can we construct more theories that ought to be geometric? We should start from some finite collection of objects (i.e. a model of ), “construct some new objects and morphisms,” and then “impose some axioms on them.” For any theory , let’s call a transformation a geometric construct. This is supposed to be “an object constructed out of the axioms of in a natural way.” More precisely, to every -model in a topos it assigns an object of , in a way that varies naturally with morphisms of -models and inverse image functors.
Now define a simple functional extension of to be the inserter of a pair of geometric constructs . A model of such a theory will consist of a model of , together with an additional morphism between two objects constructed out of the given -model. By iteratively applying such constructions, we can add in any number of new morphisms between “constructed objects.”
Finally, define a simple geometric quotient of to be the inverter of a modification between a pair of geometric constructs . That is, we require that a certain naturally defined morphism between objects constructed out of -models must be an isomorphism. (Applying equalizers, we see that this also includes the ability to set morphisms equal, i.e. to construct equifiers.)
From this point of view, a geometric theory is a theory obtained from some by a finite sequence of simple functional extensions and simple geometric quotients. Of course, once we know that each has a classifying topos, it follows immediately that any geometric theory has a classifying topos, since has inserters and inverters.
The following definition is sort of a “halfway house” between logic and geometry. Start with a first-order signature (this is the logical part). Then we have a 2-functor sending a topos to the category of -structures in . A geometric theory over is defined to consist of the following.
The equivalence of this definition with the others can be found in
It is not sufficient, in the third condition, to restrict to the case when is a singleton, but it is sufficient to consider the case when is a singleton together with all families of coproduct injections .
By framing this notion in the internal language of a topos we can talk of geometric theories over , with models in bounded -toposes (the relative version of “Grothendieck topos”). As a simple example, if we have a sheaf of rings on a topological space we can describe left -modules as models of a geometric theory over , the topos of sheaves on , and this notion is definable in -toposes.
Similarly to the -based case, given a geometric theory over a topos , we can form the -topos that classifies , for which the category of -models in a bounded -topos is naturally equivalent to the category of morphisms of -toposes . In other words
Since a Grothendieck topos is the “extensional essence” of a geometric theory, it makes sense to define a map of theories to be a morphism of -toposes . Equivalently, of course, this is a -model in . Composition with induces a functor, forget along , from -models to -models in any -topos.
Define the gros category? of -models to have as objects pairs where is an -topos and is a -model in . A map is given by a morphism of -toposes and a homomorphism of -models in . The composition of maps should be evident. A map of geometric theories over induces a forgetful functor which leaves unchanged the -topos of residence, which has a left adjoint which may change the topos. For if is a -model in , pulling back along yields a -model, not in but in the pullback. This is a consequence of general facts about finite 2-limits of the 2-category of bounded -toposes.
Standard textbook accounts include
Discussion in the context of computer science is in
Discussion with an eye towards geometric type theory is in