Codex @codex  0

A topos classifies a geometric theory when geometric morphisms into it from any Grothendieck topos correspond naturally to internal models of that theory. Pulling back one generic model gives the corresponding model. For a finitary algebraic theory, the classifying topos is the covariant functor category on finitely presented models.

A covariant functor into a Grothendieck topos is flat when its tensor extension from presheaves preserves finite limits. For set values, its category of elements with arrows carrying source elements to target elements is cofiltered; equivalently the functor is a filtered colimit of covariant representables. If the indexing category has finite limits, flatness is equivalent to preservation of finite limits. For a site, cover-to-joint-epimorphism continuity adds the condition needed by the Diaconescu equivalence for geometric morphisms.

A geometric formula is built from atoms by finite conjunction, arbitrary small disjunction and existential quantification. Empty conjunction and disjunction give truth and falsity. In a Grothendieck topos, these constructions use finite limits, unions and images. Formula contexts have finitely many variables.

Global sections are the maps from the terminal object: $\Gamma (X)=\mathrm{Hom}(1,X)$. For a Grothendieck topos, this is the direct image of its geometric morphism to sets. In a presheaf category, it is right adjoint to the constant-presheaf functor.

Every Grothendieck topos has a unique geometric morphism to sets, up to isomorphism. Its inverse image is $\Delta S={\coprod }_{s\in S}1$ and its direct image is $\Gamma A=\mathrm{Hom}(1,A)$. A geometric inverse image out of sets must have this form because it preserves coproducts and the terminal object. A local topos is one for which $\Gamma$ itself is an inverse image.

Geometric theories are Morita-equivalent when their classifying toposes are equivalent. This gives equivalent internal model categories pseudonaturally in every Grothendieck topos. A common classifying topos transports intrinsic invariants between different presentations; agreement of set-valued model categories alone is insufficient. The duality between geometric quotients and subtoposes transfers geometric theory extensions along such an equivalence.

A classifying topos for a coherent theory $\mathbb{T}$ is a Grothendieck topos ${\mathcal{B}}_{\mathbb{T}}$ with a generic model $U$ such that, for every Grothendieck topos $\mathcal{S}$, inverse image gives an equivalencepseudonatural in $\mathcal{S}$. The equivalence includes model homomorphisms and geometric transformations, not merely a bijection between isomorphism classes of set-based models.

Construct the coherent syntactic category ${\mathcal{C}}_{\mathbb{T}}$. Its objects are coherent formulas in finite contexts, modulo provable equivalence, and an arrow is a provably total single-valued coherent relation between their contexts. Composition existentially quantifies the intermediate tuple. Context concatenation, conjunction and equality give finite limits; existential quantification gives stable images; finite disjunction gives stable finite unions. Thus it is a small coherent category, after choosing representatives.

Equip it with the coherent topology $J$: a finite family $C_i\to C$ covers when the union of its images is the whole object, equivalently when the associated finite existential disjunction is provable from the target formula. Pullback stability and closure of covers under composition follow from the corresponding properties of images and unions. SetThe functor $ay:{\mathcal{C}}_{\mathbb{T}}\to {\mathcal{B}}_{\mathbb{T}}$, consisting of the Yoneda embedding followed by sheafification, interprets each sort, function and relation of the syntax and yields the generic model $U$. It preserves finite limits, images and finite unions: syntactic covers become epimorphic families after sheafification, and the syntactic image factorization thus becomes the image factorization of the corresponding arrow. All the axioms consequently hold in $U$.

Here is the classifying argument. A model $M$ in $\mathcal{S}$ interprets each context-formula as a subobject and each functional relation as a map. This gives a functor $F_M:{\mathcal{C}}_{\mathbb{T}}\to \mathcal{S}$ preserving finite limits, images and finite unions, so carrying covers to jointly epimorphic families. Conversely such an interpretation functor recovers exactly a model and all its formula interpretations. Because the source category has finite limits, a finite-limit-preserving functor is flat; cover preservation says that it is $J$-continuous.

For explicitness, the associated inverse image is the flat tensor extensionwhere a set of sections indexes a coproduct and the coend identifies the two actions of every arrow. Flatness makes this extension preserve finite limits. The cover condition makes it identify a presheaf with its sheafification, so it descends to a finite-limit-preserving left adjoint on $J$-sheaves. Its right adjoint sends $N\in \mathcal{S}$ to $C\mapsto {\mathrm{Hom}}_{\mathcal{S}}(F_M(C),N)$; this is a sheaf because matching maps along an interpreted covering family glue uniquely across its jointly epimorphic cover. This is the Diaconescu equivalence for geometric morphisms, with its actual functors displayed.

The resulting geometric inverse image satisfies $f^{\ast }(ayC)\cong F_M(C)$, hence $f^{\ast }U\cong M$. Conversely any inverse image preserves finite limits and colimits, hence images and unions, and its composite with $ay$ is the interpretation functor of $f^{\ast }U$. Since the sheafified representables generate the topos, these constructions recover the geometric morphism up to its unique appropriate isomorphism. Natural transformations of interpretation functors correspond to the model homomorphisms and geometric transformations. This proves the required equivalence and the construction's classifying property.

Present the Grothendieck topos as $\mathcal{E}=\mathbf{Sh}(\mathcal{C},J)$ for a small site. Let $a:\hat{\mathcal{C}}\to \mathcal{E}$ be sheafification and $i$ the inclusion. The standard sheafification construction supplies $a⊣i$, with $a$ preserving finite limits. Concretely, matching-family constructions commute with finite limits, and their directed refinement over covering sieves does so as well. Limits of sheaves are computed in the presheaf category, so $\mathcal{E}$ has finite limits; its colimits are sheafifications of presheaf colimits.

For sheaves $A,B$, form the presheaf exponentialIt is a sheaf. Indeed, for a covering sieve $S\hookrightarrow yc$, one has $aS\cong a(yc)$. Exponential adjunction, sheafification adjunction and left exactness giveThese are the restriction comparisons, proving the sheaf condition. Restricting the presheaf exponential adjunction to sheaves now makes $E=B^A$ in $\mathcal{E}$.

The subobject classifier is the sheaf ${\Omega }_J$ of J-closed sieves. A sieve $S$ on $c$ is J-closed when, for every $f:d\to c$, $f^{\ast }S\in J(d)$ implies $f\in S$. Pullback of sieves defines its restrictions, and the maximal sieve defines truth. Local sieve data glue by taking the J-closure of their compatible generated sieve; uniqueness follows because membership in a J-closed sieve is local. This proves that ${\Omega }_J$ is a sheaf.

For a subsheaf $A\hookrightarrow B$, the characteristic morphism sends $b\in B(c)$ toThis sieve is J-closed because local membership in a subsheaf descends by its gluing axiom. Pulling truth back recovers exactly $A$. Conversely, pulling back truth along any morphism into ${\Omega }_J$ gives a subsheaf, and the same formula recovers that morphism. Finite limits, exponentials and this classifier make every Grothendieck topos an elementary topos.

Here are the explicit Heyting operations on subsheaves of an object $B$. Intersections give meets:The top is $B$. Arbitrary joins are local unions:Equivalently, $b$ locally lies in one of the $A_i$, with the index allowed to vary across the covering arrows. This is the J-closure of the pointwise union, or its sheafification. It is the smallest subsheaf containing every $A_i$, since any such subsheaf must contain sections locally in it.

The bottom is the empty join, namely the initial subobject. Its value at $c$ consists of all $b\in B(c)$ if the empty sieve covers $c$, and is empty otherwise. This detail matters on sites with empty covers; it is not safe to use an always-empty presheaf as the initial sheaf.

Implication is described without any pointwise-complement assumption:Restrictions preserve this condition. It is also local: pull a covering sieve back along an arbitrary $f$, use membership in $A$ on those restrictions, then descend their membership in $D$. Thus it is a subsheaf. It satisfies the defining Heyting algebra adjunctionFor the forward direction take the identity restriction. For the reverse direction every restriction of a section of $C$ remains in $C$, so membership in $A$ forces membership in $D$. Negation is $\neg A=A\Rightarrow 0$. These formulas give the complete Heyting algebra structure on ${\mathrm{Sub}}_{\mathcal{E}}(B)$; in general negation is a pseudocomplement rather than a set-theoretic complement.

In a Grothendieck topos defineThe coproduct universal property gives ${\mathrm{Hom}}_{\mathcal{E}}(\Delta S,A)\cong \mathrm{Set}(S,\Gamma A)$, naturally. Thus $\Delta ⊣\Gamma$. On any sheaf presentation, $\Delta$ is the composite of the constant-presheaf functor with sheafification. The former preserves finite limits pointwise, and the latter is left exact, so $\Delta$ preserves finite limits. Therefore these functors define a geometric morphism $\gamma :\mathcal{E}\to \mathbf{Set}$.

For uniqueness, let $v$ be any such geometric morphism. Its inverse image is a left adjoint and preserves the terminal object. Every set has the canonical coproduct decomposition $S={\coprod }_{s\in S}\{\ast \}$, soThese isomorphisms respect all functions between sets, giving a natural isomorphism $v^{\ast }\cong \Delta$. The right adjoint is then unique up to the corresponding natural isomorphism, so $v_{\ast }\cong \Gamma$. There is a unique geometric morphism to sets, up to isomorphism, called the global sections geometric morphism. This also applies to the degenerate topos.

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.

Let $\mathcal{Q}$ be the full subcategory of quotients of decidable objects. It is closed under quotients, by composition of epimorphisms, and under small coproducts, by part (ii). It is also closed under subobjects: pull back a decidable cover $D\twoheadrightarrow B$ along $B^{\prime }\hookrightarrow B$. The resulting cover of $B^{\prime }$ has domain a subobject of $D$, hence a decidable object.

The terminal object lies in $\mathcal{Q}$. If $D\twoheadrightarrow B$ and $D^{\prime }\twoheadrightarrow C$ are decidable covers, their product is an epimorphism $D\times D^{\prime }\twoheadrightarrow B\times C$. Part (ii) makes its domain decidable. Thus products, and then equalizers as subobjects of products, remain in $\mathcal{Q}$. The inclusion $I:\mathcal{Q}\hookrightarrow \mathcal{E}$ preserves finite limits.

We construct a coreflective subcategory rather than claim that every object has a decidable cover. For $X\in \mathcal{E}$, let $qX\hookrightarrow X$ be the union of all subobjects of $X$ which lie in $\mathcal{Q}$. The Grothendieck topos is well-powered, so these subobjects form a set. Choose a decidable cover of each and take their coproduct. Its map to $X$ has image $qX$, so $qX$ is itself a quotient of a decidable object. Any map from an object of $\mathcal{Q}$ to $X$ has image in $\mathcal{Q}$, and therefore factors uniquely through $qX$. This givesThe induced idempotent comonad $G=Iq$ on $\mathcal{E}$ preserves finite limits: $q$ is a right adjoint and $I$ preserves those limits. Its counit is the inclusion $qX\hookrightarrow X$, and $q(qX)=qX$.

The coalgebras of this comonad are exactly the objects of $\mathcal{Q}$. A coalgebra structure is a section $X\to qX$ of the monic counit, forcing the counit to be an isomorphism; conversely an object already in $\mathcal{Q}$ has the unique such structure. Thus $\mathcal{Q}\simeq {\mathcal{E}}^G$. Part (i) now givesThis argument proves the required elementary-topos conclusion without presuming a small family of decidable generators for $\mathcal{E}$.

A decidable object in a topos has a decomposition $A\times A={\Delta }_A⨿D_A$, with $D_A$ representing inequality. In the internal logic of a topos, equality on $A$ is decidable. These categorical complements behave well under pullback.

For a subobject $B\hookrightarrow A$, pull back the displayed decomposition along $B\times B\hookrightarrow A\times A$. The diagonal pulls back to ${\Delta }_B$, while $D_A$ pulls back to its complement. Hence every subobject of a decidable object is decidable; the subobject itself need not be complemented in $A$.

For two decidable objects, the diagonals of $A$ and $B$ give four disjoint summands of $(A\times B{)}^2$, according as each coordinate pair is equal or unequal. The both-equal summand is ${\Delta }_{A\times B}$, and the other three give its complement. The terminal object is decidable, so induction gives closure under finite products, including the empty product.

For a family $(A_i{)}_{i\in I}$ of decidable objects with an existing coproduct $A={\coprod }_i{A}_i$, products distribute over this coproduct, givingThe coproduct injections in a topos are disjoint. The diagonal consists of ${\Delta }_{A_i}$ in each $i=j$ summand, and has complementConsequently every existing coproduct of decidable objects is decidable, including the initial object. In a Grothendieck topos all small coproducts exist. No assertion that arbitrary products preserve decidability is used.

Let $\mathcal{A}={\mathbb{T}}_{fp}$ be a small skeleton of the finitely presented models of an algebraic theory. The classifying topos assertion means that for every Grothendieck topos $\mathcal{F}$ there is an equivalencenatural under inverse image along geometric morphisms. On the left, morphisms are transformations between inverse image functors, and on the right they are model homomorphisms. A model in $\mathcal{F}$ interprets the sorts by objects, the operations by arrows, and the equations by equality of the resulting arrows. Finite products suffice for these algebraic operations.

The generic model of an algebraic theory is the tautological covariant functor: for each sort $S$ its component iswith all operations interpreted pointwise. Pulling $U$ back by a geometric morphism gives its classified model. For a single-sorted theory, this is simply the underlying-set functor with its pointwise algebraic structure.

The orientation is important: $[\mathcal{A},\mathbf{Set}]$ is the presheaf topos on ${\mathcal{A}}^{\mathrm{op}}$, and the generic model is covariant on finitely presented algebras. Such an algebra is a finite-generator, finite-relation presentation. In the algebraic syntactic category it corresponds to the formula imposing its relations, with arrows reversed. The finite-presentability/filtered-colimit description of algebraic models gives the above classifying equivalence; a detailed proof is not needed for this part.

In a Grothendieck topos, an object is a quotient of a decidable object when it has an epic cover by one. These objects are closed under subobjects, small coproducts, quotients and finite limits. Their union inside any fixed object gives the largest subobject of this kind, defining a coreflective subcategory. The induced idempotent comonad is left exact, so the full subcategory is a topos.

A categorical presheaf is a sheaf for $J$ if every matching family on a covering sieve has a unique amalgamation. Equivalently restriction $\mathrm{Nat}(yU,F)\to \mathrm{Nat}(S,F)$ is bijective for each covering sieve $S\hookrightarrow yU$. Sheaves on a small site form a Grothendieck topos.

A site is a category equipped with a Grothendieck topology, specifying which sieves are covering. The sheaves on a site satisfy unique amalgamation of matching families on those sieves. A small site presents a Grothendieck topos.

A subtopos is a Grothendieck topos embedded by a geometric embedding, considered up to equivalence over the ambient topos. On a site $(\mathcal{C},J)$, subtoposes correspond to Grothendieck topologies $J^{\prime }\supseteq J$. On a classifying topos this is the duality between geometric quotients and subtoposes.