nLab geometric theory

Contents

Context

Topos Theory

topos theory

Background

Toposes

Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory

Theorems

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

  • Let Σ\Sigma be a signature, then the set of all geometric sequents over Σ\Sigma as well as the empty set are geometric theories called the inconsistent theory 𝕋 0 Σ\mathbb{T}^\Sigma_0 resp. the empty theory 𝕋 1 Σ\mathbb{T}^\Sigma_1 over Σ\Sigma. The former admits a more concise axiomatisation as {}\{\top\vdash\bot\}. The most basic examples occur when the signature is empty: 𝕋 0 \mathbb{T}^\emptyset_0 is classified by the initial topos 1\mathbf{1} and 𝕋 1 \mathbb{T}^\emptyset _1 is classified by the terminal topos SetSet (see at classifying topos for details).

  • The empty signature occurring in the preceding example is an extreme case of a propositional signature i.e. one lacking sort symbols. These can at most contain 0-ary relation symbols since function symbols and higher order relation symbols require sorts. Whence theories over such signatures can at most contain sequents in the empty context between formulas consisting of quantifier-free nestings of 0-ary relation symbols and ,\wedge,\bigvee and are therefor called propositional theories - in other words: geometric logic boils down to propositional logic. Propositional theories are classified by localic toposes (see there for further information).

  • 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 𝕂 \mathbb{K} of categories with models the (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(x=0)(n\cdot x = 0) \vdash_{x} (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) xy(z.(xz=1)z.(yz=1))\exists z. ((x+y)z = 1) \vdash_{x y} (\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(x=0)(y.(xy=1)) \top \vdash_{x} (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” – see field) 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

    x n1(nx=0) \top \vdash_{x} \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 the standard successor algebra is geometric. Its signature has one sort symbol NN, one function symbol s:NNs:N\to N and one constant 0:N0:N. The theory axiomaticizes natural number objects by taking advantage of the availability of infinitary disjunctions in geometric logic in order to assert in the third axiom that every natural number is standard i.e. either 0 or obtained from 0 by (repeated) application of the successor function:

    • 0=s(n) n0 = s(n) \vdash_{n} \bot
    • s(n)=s(n) nnn=ns(n) = s(n') \vdash_{n n'} n=n'
    • n in=ssi(0)\top \vdash_{n} \bigvee_{i} n=\underset{i}{\underbrace{s \dots s}}(0)

    The classifying topos is SetSet. But due to the trivial subtopos lattice, theories classified by Set admit no consistent quotient theories; thus the geometric theory of natural numbers is complete! Furthermore, since SetSet is the terminal topos, classifying also the empty theory, one sees that the object/type \mathbb{N} of natural numbers “comes for free” in geometric logic. This observation underlies the ideas for a geometric type theory (for more on this see there or the article by Vickers).

  • 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:

    • (p 1<x<q 1)(p 2<x<q 2)(max(p 1,p 2)<x<min(q 1,q 2))(p_1\lt x\lt q_1) \wedge (p_2\lt x\lt q_2) \vdash (\max(p_1,p_2) \lt x \lt \min(q_1,q_2)) (if max(p 1,p 2)<min(q 1,q 2)\max(p_1,p_2)\lt \min(q_1,q_2)), and (p 1<x<q 1)(p 2<x<q 2)(p_1\lt x\lt q_1) \wedge (p_2\lt x\lt q_2) \vdash \bot (otherwise).
    • (p<x<q)(p<x<q)(p<x<q)(p\lt x\lt q) \vdash (p\lt x\lt q') \vee (p' \lt x\lt q) (if p<p<q<qp\lt p' \lt q' \lt q).
    • (p<x<q) p<p<q<q(p<x<q)(p\lt x\lt q) \vdash \bigvee_{p\lt p'\lt q'\lt q} (p' \lt x\lt q').
    • p<q(p<x<q)\top \vdash \bigvee_{p\lt q} (p\lt x\lt q).

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

  • The theory of flat diagrams1 over a small category 𝒞\mathcal{C} is geometric. For each object ii of 𝒞\mathcal{C} there is a sort σ i\sigma_i, and for each morphism u:iju\colon i \to j a function symbol α u:σ iσ j\alpha_u\colon \sigma_i \to \sigma_j. The axioms are -

    • x:σ iα Id i(x)=x\top \vdash_{x\colon\sigma_i} \alpha_{Id_i}(x) = x

    • x:σ iα v(α u(x))=α vu(x)\top \vdash_{x\colon\sigma_i} \alpha_{v}(\alpha_u(x)) = \alpha_{v u}(x) (u:iju\colon i \to j and v:jkv\colon j \to k)

    • i𝒞 0(x:σ i)\top \vdash \bigvee_{i \in \mathcal{C}_0} (\exists x\colon \sigma_i) \top

    • x:σ i,y:σ j u:ki,v:kj(z:σ k)(x=α u(z)y=α v(z))\top \vdash_{x\colon\sigma_i, y\colon\sigma_j} \bigvee_{u\colon k\to i, v\colon k\to j} (\exists z\colon\sigma_k) (x = \alpha_u(z) \wedge y = \alpha_v(z))

    • α u(x)=α v(x) x:σ i w:ki,uw=vw(z:σ k)x=α w(z)\alpha_u(x) = \alpha_v(x) \vdash_{x\colon\sigma_i} \bigvee_{w\colon k\to i, u w = v w} (\exists z\colon \sigma_k) x = \alpha_w(z) (u,v:iju,v\colon i \to j)

    This theory is classified by the topos of presheaves over 𝒞\mathcal{C}.

    It is commonly more useful to consider the theory of flat presheaves over 𝒞\mathcal{C}, in other words the flat diagrams over 𝒞 op\mathcal{C}^{op}. (Elephant calls these torsors over 𝒞\mathcal{C}, generalizing the established terminology for groups.) This is because the representable presheaves are flat, and so Yoneda’s lemma transforms objects of 𝒞\mathcal{C} covariantly into models of the theory. In fact, the models of the theory are the filtered colimits of representables. For example, a finitary algebraic theory is classified by the topos of covariant functors from the category of finitely presented algebras to SetSet.

  • If (𝒞,J)(\mathcal{C},J) is a small site, by adding a geometric axiom schema to express J-continuity to the theory of flat diagrams, one obtains the theory of J-continuous flat diagrams, which is classified by Sh(𝒞,J)Sh(\mathcal{C},J). This answers in principle the question, given a site representation what geometric theory is classified by a Grothendieck topos? Of course, in practice one would like to have more concise and less unwieldy axiomatizations.

  • For any geometric theory 𝕋\mathbb{T} there exists a geometric theory 𝕋 2\mathbb{T}^\mathbf{2} called the theory of 𝕋 \mathbb{T} -model homomorphisms whose models in a Grothendieck topos \mathcal{E} are precisely the homomorphisms between 𝕋\mathbb{T}-models in \mathcal{E}:

    Mod 𝕋 2()=Mod 𝕋() 2=Mod 𝕋( 2).Mod_{\mathbb{T}^\mathbf{2}}(\mathcal{E})=Mod_{\mathbb{T}}(\mathcal{E})^\mathbf{2}=Mod_\mathbb{T}(\mathcal{E}^\mathbf{2})\quad.
  • 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 categories of models in all Grothendieck topoi up to equivalence (hence a Grothendieck topos is the “extensional categorical 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.

The 2-categorical version of TModT Mod is useful in generalization of the spectrum construction: See at Cole's theory of spectrum.

Properties

References

Review:

Textbook accounts:

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:

which has become a chapter of the following monograph exploring first-order model theory in the context of Grothendieck toposes:

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

Discussion with an eye towards quantum physics:

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)

  1. This is also sometimes called the theory of flat functors on 𝒞\mathcal{C}.

Last revised on May 3, 2024 at 10:06:45. See the history of this page for a list of all contributions to it.