nLab
geometric theory

Context

Topos Theory

Could not include topos theory - contents

Contents

Idea

The notion of geometric theory has many different incarnations. A few are:

The equivalence of these statements involves some serious proofs, including Giraud's theorem characterizing Grothendieck topoi.

Logical definition

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:

Note that the axioms of one of these theories are actually of the form

φ xψ \varphi \vdash_{\vec{x}} \psi

where φ\varphi and ψ\psi are formulas involving only the specified connectives and quantifiers, \vdash means entailment, and x\vec{x} is a context. Such an axiom can also be written as

x.(φψ) \forall \vec{x}. (\varphi \Rightarrow \psi)

so that although \Rightarrow and \forall 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 φ\varphi and ψ\psi which must be built out of \top, \wedge, \bot, \bigvee, and \exists are sometimes called positive or geometric formulas.

The interpretation of arbitrary uses of \Rightarrow and \forall 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 \bigwedge 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 TT generates a “free geometric category containing a model of that theory,” also known as its syntactic category G TG_T. This syntactic category G TG_T has the universal property that for any other geometric category GG', geometric functors G TGG_T \to G' are equivalent to TT-models in GG'.

Examples

  • Any finitary algebraic theory is, in particular, a cartesian theory, and hence geometric. This includes monoids, groups, abelian groups, rings, commutative rings, etc.

  • The theory of (strict) categories is not finitary-algebraic, but it is cartesian, and hence geometric; this generalises to (finitary) essentially algebraic theories.

  • The theory of torsion-free abelian groups is also cartesian, being obtained from the theory of abelian groups by the addition of the sequents (nx=0)(x=0)(n\cdot x = 0) \vdash (x = 0) for all nn\in \mathbb{N}.

  • The theory of local rings is a coherent theory, being obtained from the theory of commutative rings by adding the sequent (0=1) (0 = 1) \vdash \bot , for nontriviality, and

    z.((x+y)z=1)(z.(xz=1)z.(yz=1))\exists z. ((x+y)z = 1) \vdash (\exists z.(x z = 1) \vee \exists z.(y z = 1))

    saying that if x+yx+y is invertible, then either xx or yy is so.

  • The theory of fields is also coherent, being obtained from the theory of commutative rings by adding (0=1) (0 = 1) \vdash \bot and also

    (x=0)(y.(xy=1)) \top \vdash (x=0) \vee (\exists y.(x y = 1))

    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

    n1(nx=0) \top \vdash \bigvee_{n\ge 1} (n \cdot x = 0)

    asserting that for each xx, either x=0x=0 or x+x=0x+x=0 or x+x+x=0x+x+x=0 or …. Similarly, the theory of fields of finite characteristic is geometric but not coherent.

  • The theory of a real number is geometric. This is a propositional theory, having no sorts, and having one relation symbol “p<x<qp\lt x\lt q” for each pair of rational numbers p<qp\lt q. Its axioms are:

    • If max(p 1,p 2)<min(q 1,q 2)\max(p_1,p_2) \lt \min(q_1,q_2), then if p 1<x<q 1p_1\lt x\lt q_1 and p 2<x<q 2p_2\lt x\lt q_2, then max(p 1,p 2)<x<min(q 1,q 2)\max(p_1,p_2)\lt x\lt \min(q_1,q_2). Otherwise, if p 1<x<q 1p_1\lt x\lt q_1 and p 2<x<q 2p_2\lt x\lt q_2 then \bot.
    • If p<p<q<qp\lt p' \lt q' \lt q, then if p<x<qp\lt x\lt q, then either p<x<qp\lt x\lt q' or p<x<qp' \lt x\lt q.
    • If p<x<qp\lt x\lt q, then p<p<q<q(p<x<q)\bigvee_{p\lt p'\lt q'\lt q} (p' \lt x\lt q').
    • Always p<q(p<x<q)\bigvee_{p\lt q} (p\lt x\lt q).

    The classifying topos of this theory is the topos of sheaves on the real numbers.

  • A geometric theory whose classifying topos is a presheaf topos is called a theory of presheaf type.

Other characterizations

In terms of sheaf topoi

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 f *f *f^* \dashv f_* in which f *f^* (the “inverse image”) preserves finite limits.

Thus:

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 f *f_*, which is the opposite direction to the geometric functor f *f^*. (This is because when EE and FF are the toposes of sheaves on sober topological spaces (or locales) XX and YY respectively, then continuous maps XYX \to Y correspond precisely to geometric morphisms EFE \to F.) 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 \forall and \Rightarrow) 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 G TG_T of a geometric theory to obtain an infinitary pretopos Set[T]Set[T]. As long as the theory TT was itself small, Set[T]Set[T] 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 EE, geometric morphisms ESet[T]E\to Set[T] are equivalent to TT-models in EE. This topos Set[T]Set[T] is called the classifying topos of TT.

In the other direction, if CC is any small site, we can write down a “geometric theory of cover-preserving flat functors C opSetC^{op}\to Set.” By Diaconescu's theorem classifying geometric morphisms into sheaf topoi, it follows that Sh(C)Sh(C) 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.

Functorial definition

We can approach the same idea by starting instead from the notions of Grothendieck topos and geometric morphism. The following approach is described in B4.2 of the Elephant.

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 T:GrTop opCatT\colon GrTop^{op}\to Cat, where GrTopGrTop is the 2-category of Grothendieck topoi and geometric morphisms, so for the moment let’s call any such TT a “theory”. The image T(E)T(E) of a functor EE is supposed to be “the category of TT-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, OO. This 2-functor sends a topos EE to itself, considered as a mere category, and an inverse image functor to itself, considered as a mere functor. The theory OO can be shown to have a classifying topos, the object classifier Set[O]Set[O]. Similarly, we have a theory O nO_n of nn-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 O nO_n), “construct some new objects and morphisms,” and then “impose some axioms on them.” For any theory TT, let’s call a transformation TOT\to O a geometric construct. This is supposed to be “an object constructed out of the axioms of TT in a natural way.” More precisely, to every TT-model in a topos EE it assigns an object of EE, in a way that varies naturally with morphisms of TT-models and inverse image functors.

Now define a simple functional extension of TT to be the inserter of a pair of geometric constructs TOT\;\rightrightarrows\; O. A model of such a theory will consist of a model of TT, together with an additional morphism between two objects constructed out of the given TT-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 TT to be the inverter of a modification between a pair of geometric constructs TOT\;\rightrightarrows\; O. That is, we require that a certain naturally defined morphism between objects constructed out of TT-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 GrTop opCatGrTop^{op}\to Cat obtained from some O nO_n by a finite sequence of simple functional extensions and simple geometric quotients. Of course, once we know that each O nO_n has a classifying topos, it follows immediately that any geometric theory has a classifying topos, since GrTopGrTop has inserters and inverters.

Hybrid definition

The following definition is sort of a “halfway house” between logic and geometry. Start with a first-order signature Σ\Sigma (this is the logical part). Then we have a 2-functor ΣStr:GrTop opCat\Sigma Str\colon GrTop^{op}\to Cat sending a topos EE to the category ΣStr(E)\Sigma Str(E) of Σ\Sigma-structures in EE. A geometric theory over Σ\Sigma is defined to consist of the following.

  • For each Grothendieck topos EE, we have a replete full subcategory T(E)T(E) of ΣStr(E)\Sigma Str(E), such that
  • For each geometric morphism f:EFf\colon E\to F, if MT(F)M\in T(F) then f *MT(E)f^*M\in T(E) (i.e. TT is a subfunctor of ΣStr\Sigma Str), and moreover
  • For any set-indexed jointly surjective family (f i:E iE) iI(f_i \colon E_i \to E)_{i\in I} of geometric morphisms, and any MΣStr(E)M \in \Sigma Str(E), if f i *MT(E i)f_i^* M \in T(E_i) for all ii, then MT(E)M\in T(E).

The equivalence of this definition with the others can be found in

  • Olivia Caramello, “A characterization theorem for geometric logic”, arXiv:0912.1404.

It is not sufficient, in the third condition, to restrict to the case when II is a singleton, but it is sufficient to consider the case when II is a singleton together with all families of coproduct injections (E i iE i) iI(E_i \to \coprod_i E_i)_{i\in I}.

Localization

By framing this notion in the internal language of a topos SS we can talk of geometric theories over SS, with models in bounded SS-toposes (the relative version of “Grothendieck topos”). As a simple example, if we have a sheaf AA of rings on a topological space XX we can describe left AA-modules as models of a geometric theory over Sh(X)Sh(X), the topos of sheaves on XX, and this notion is definable in Sh(X)Sh(X)-toposes.

Similarly to the SetSet-based case, given a geometric theory TT over a topos SS, we can form the SS-topos S[T]SS[T] \to S that classifies TT, for which the category of TT-models in a bounded SS-topos EE is naturally equivalent to the category of morphisms of SS-toposes ES[T]E \to S[T]. In other words

TMod(E)Top S(E,S[T])T Mod(E) \simeq Top_S(E,S[T])

Morphisms of theories

Since the classifying topos encodes the “extensional essence” of a geometric theory, it makes sense to define a map of theories TTT \to T' to be a morphism of SS-toposes h:S[T]S[T]h: S[T'] \to S[T]. Equivalently, of course, this is a TT-model in S[T]S[T']. Composition with hh induces a functor, forget along hh, from TT'-models to TT-models in any SS-topos.

Gros categories of models

Define the gros category? TModT Mod of TT-models to have as objects pairs (E,A)(E,A) where EE is an SS-topos and AA is a TT-model in EE. A map (f,g):(E,A)(F,B)(f,g): (E,A) \to (F,B) is given by a morphism f:FEf: F \to E of SS-toposes and a homomorphism g:f *(A)Bg: f^*(A) \to B of TT-models in FF. The composition of maps should be evident. A map h:TTh: T \to T' of geometric theories over SS induces a forgetful functor TModTModT' Mod \to T Mod which leaves unchanged the SS-topos of residence, which has a left adjoint TModTModT Mod \to T' Mod which may change the topos. For if a:ES[T]a: E \to S[T] is a TT-model in EE, pulling aa back along hh yields a TT'-model, not in EE but in the pullback. This is a consequence of general facts about finite 2-limits of the 2-category of bounded SS-toposes.

Properties

References

Standard references are

A textbook account of (finitary) geometric logic can be found in

A systematic introduction to topos theory and geometric logic can be found in the following draft by O. Caramello:

For additional background on (finitary) geometric formulas consider:

  • Karel Stokkermans, Bill Lawvere, and Steve Vickers: Catlist discussion March 1999 . (link)

  • H.J. Keisler: Theory of models with generalized atomic formulas , JSL 25 (1960), pp.1-26.

Discussion in the context of computer science is in

Discussion with an eye towards geometric type theory is in

Stone duality for geometric theories is discussed in:

A nice short exposition together with an unorthodox proposal to expand geometric logic with fix point operators can be found here:

  • Andreas Blass, Topoi and Computation, Bull. European Assoc.Theoret. Comp.Sci. 36 (1988) pp.57-65. (draft)

Revised on September 28, 2014 02:28:45 by Colin Zwanziger (108.32.26.99)