Past exam of the mathematics course of the University of Cambridge / 2012 / iii / Paper 23 / 6

A geometric formula is built from atomic formulas, including equality, using finite conjunctions, arbitrary set-indexed disjunctions and existential quantification in a finite variable context. Truth is the empty conjunction and falsity the empty disjunction. A geometric theory is a set of sequents $\varphi {⊢}_{\vec{x}}\psi$ between such formulas over a many-sorted signature. The context supplies the universal force of an axiom; unrestricted universal quantification, implication and negation are not formula constructors in this fragment.

These choices are exactly suited to inverse image functors of geometric morphisms. Finite-limit preservation handles equality and conjunction; colimit and image preservation handle disjunction and existential quantification. Therefore an inverse image carries an internal model of a geometric theory to another model.

Construct the geometric syntactic category ${\mathcal{C}}_{\mathbb{T}}$ as follows. Objects are formulas in context $\{\vec{x}.\varphi \}$, modulo provable renaming and equivalence. A morphism to $\{\vec{y}.\psi \}$ is an equivalence class of formulas $\theta (\vec{x},\vec{y})$ that are provably total and single-valued:The last notation abbreviates componentwise equality. Identity is equality of the context variables; composition is existential conjunction over the intermediate tuple. The category has finite limits, formed through conjunction and equality.

Give it the geometric syntactic topology $J_{\mathbb{T}}$. A family of arrows represented by ${\theta }_i({\vec{y}}_i,\vec{x})$ into $\{\vec{x}.\varphi \}$ covers whenPullback stability is substitution, and transitivity comes from distributing existential conjunction through the covering disjunctions. Thus the generated sieves define a Grothendieck topology. Empty covers impose the interpretation of falsity as the initial object.

The classifying topos isIts universal model $U_{\mathbb{T}}$ assigns a sort $A$ the sheafified representable of $\{x^A.\top \}$, functions their definable graph morphisms and relations their definable subobjects. The syntactic covering conditions make the axioms valid in this model.

For the universal property, interpreting formulas in a model $M$ in a Grothendieck topos $\mathcal{F}$ gives a finite-limit-preserving, $J_{\mathbb{T}}$-continuous functor ${\mathcal{C}}_{\mathbb{T}}\to \mathcal{F}$: covers go to jointly epimorphic families precisely because the relevant sequents hold. The Diaconescu equivalence for geometric morphisms associates to this functor a geometric morphism $\mathcal{F}\to \mathbf{Set}[\mathbb{T}]$. Conversely, pulling $U_{\mathbb{T}}$ back along a geometric morphism gives a model. The constructions on models and their homomorphisms are inverse up to natural isomorphism, yieldingnaturally in $\mathcal{F}$. This proves the required classifying property, not merely classification of set-valued models.

Yes, with the Horn/Cartesian-fragment convention. A Horn theory uses positive finite-conjunction sequents and has a Cartesian syntactic category ${\mathcal{C}}_{\mathbb{T}}^{\mathrm{cart}}$ with finite limits. Provably uniquely witnessed existential formulas can also be admitted without changing the finite-limit nature of its semantics. Its internal models are precisely finite-limit-preserving functors from that category.

For a category with finite limits, flat functors into a Grothendieck topos are exactly finite-limit-preserving functors. In sets, the reason is concrete: the category of elements of a covariant left-exact functor is cofiltered. Its terminal object supplies nonemptiness, products supply cones over pairs of elements, and equalizers supply equalizing cones over parallel arrows. Conversely a cofiltered category of elements expresses the functor as a filtered colimit of covariant representables; filtered colimits of sets commute with finite limits. The internal version uses the same cone conditions locally.

The presheaf form of the Diaconescu equivalence for geometric morphisms therefore identifies geometric morphisms intowith internal Horn models, naturally in the domain topos. This is the presheaf classifier of a Horn theory.

Equivalently, using a small skeleton of the category $\mathcal{A}$ of finitely presented set-based Horn models, the classifier is $[\mathcal{A},\mathbf{Set}]$, with covariant functors. The duality $\mathcal{A}\simeq ({\mathcal{C}}_{\mathbb{T}}^{\mathrm{cart}}{)}^{\mathrm{op}}$ sends a formula to the model generated by its tuple subject to its finite constraints. The presheaf claim does not extend merely because a general geometric or regular theory has no written disjunctions: arbitrary existential witnesses are not uniquely witnessed Horn data.

Morita equivalence of geometric theories means equivalence of their classifying toposes. Equivalently, their categories of models in every Grothendieck topos are equivalent pseudonaturally with respect to inverse image. Agreement only of their set-based model categories, without this natural internal-model structure, is not the definition.

Suppose $\mathbf{Set}[\mathbb{T}]\simeq \mathbf{Set}[\mathbb{S}]=\mathcal{E}$. A property expressed intrinsically in terms of the topos is the same under either presentation. One can therefore translate a site or logical characterization of that property from $\mathbb{T}$ into one for $\mathbb{S}$. Examples include Booleanity, connectedness, atomicity and the structure of the subtopos lattice. The bridge is the common invariant $\mathcal{E}$, rather than an assumed literal identification of the two signatures.

The duality between geometric quotients and subtoposes makes this precise. A geometric quotient theory ${\mathbb{T}}^{\prime }$ of $\mathbb{T}$ adds geometric axioms over the same signature. Quotients are identified when they prove the same geometric sequents. The theorem givesThe subtopos corresponding to ${\mathbb{T}}^{\prime }$ is its classifying topos. Stronger axioms correspond to smaller subtoposes under inclusion.

The site mechanism explains the correspondence. On ${\mathcal{C}}_{\mathbb{T}}$, an additional sequent requires the associated family of definable images to cover its antecedent. Adding these covering sieves produces a topology $J^{\prime }\supseteq J_{\mathbb{T}}$ and a geometric embeddingConversely, subtoposes correspond to such larger topologies; requiring their extra definable covers gives the corresponding deductively closed quotient theory. Pulling the universal model into the subtopos supplies the universal model of the quotient.

Given a quotient ${\mathbb{T}}^{\prime }$, transport its subtopos along the chosen equivalence of classifying toposes. Apply the duality again to obtain a quotient ${\mathbb{S}}^{\prime }$ of $\mathbb{S}$. Their classifying toposes are equivalent, soThis is an explicit transfer principle for whole families of theory extensions and their order relations. Intrinsic constructions such as open, closed or Boolean subtoposes can likewise be described in each syntax. Different descriptions may look unrelated, but their equality is explained by the common subtopos. No universal translation of individual formulas is asserted without choosing the relevant equivalence and interpretations.