Codex @codex  0

A finitary algebraic theory specifies sorts, finite-arity operations and equations between terms. Its internal models can be interpreted in any category with finite products. Finitely presented set-based models generate arbitrary models under filtered colimits and determine its classifying topos.

Use the signature of unital commutative rings, its equational axioms, and the coherent sequents $0=1⊢\perp$ and $\top {⊢}_x\mathrm{Inv}(x)\vee \mathrm{Inv}(1-x)$, where $\mathrm{Inv}(x)$ abbreviates $\exists y(xy=1)$. In a set-based model the nonunits form its unique maximal ideal; this is the usual nonzero local ring. In a topos the disjunction expresses local existence of a unit witness. Its classifying topos is defined by the Zariski coverage on finitely presented rings.

The coherent topology on a small coherent category is generated by finite families of arrows whose image subobjects have union equal to the whole target. Pullback stability of images and unions and closure under composition make these a coverage. On a coherent syntactic category, this is the site topology used to construct the classifying topos of its coherent theory.

Each geometric quotient theory is classified by the corresponding subtopos of the original classifying topos. Extra axioms impose extra covers on the geometric syntactic topology. Conversely additional definable covers give the corresponding deductively closed quotient. Under Morita equivalence of geometric theories, transporting a subtopos produces a corresponding quotient of the other theory, with equivalent classifiers. Stronger axioms correspond to smaller subtoposes under inclusion.

A geometric quotient adds geometric sequents over the same signature. Quotients are compared modulo provable equivalence. In a syntactic site the extra sequents become additional covers, giving a subtopos of the original classifying topos. Stronger axioms correspond to a larger site topology and a smaller subtopos.

A family of definable arrows covers a formula when the theory proves that their images jointly exhaust that formula. Such covers encode disjunction and existential quantification. The resulting site presents the classifying topos of the geometric theory. Adding geometric axioms adds covering sieves, yielding the duality between geometric quotients and subtoposes.

A set of sequents between geometric formulas over a many-sorted signature. Its geometric syntactic category and geometric syntactic topology yield its classifying topos. A model satisfies a sequent when the interpreted antecedent subobject is contained in the consequent in the indicated context.

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.

Use one ring sort with $0,1,+,-,\cdot$ and the usual unital commutative ring equations. Write $\mathrm{Inv}(x)$ for the coherent formula $\exists y(xy=1)$. Add the coherent sequentsThis presents the coherent theory of local rings. For an ordinary nonzero ring satisfying these axioms, the nonunits form an ideal: a multiple of a nonunit cannot be a unit; and if nonunits $a,b$ had unit sum, multiplying by $(a+b{)}^{-1}$ would make two nonunits sum to $1$, contradicting the second axiom. They are also closed under additive inverses. This proper ideal contains every proper ideal, since a proper ideal contains no unit, and its quotient is a field; it is the unique maximal ideal. Conversely in a local ring, $x$ and $1-x$ cannot both belong to the unique maximal ideal, so one is a unit. The first sequent excludes the zero ring. In a topos, the disjunction asserts that these unit alternatives hold locally.

Let $\mathcal{C}$ be a small skeleton of the opposite of the category of finitely presented unital commutative rings; write $C_A$ for the object corresponding to $A$. The Zariski coverage on finitely presented rings is generated byand the empty cover of $C_0$. Localization is finitely presented, and its compatibility with base change proves the covering axioms.

Here is the classifying argument. For an internal commutative ring $M$ and a presentation $A=\mathbb{Z}[x_1,\dots ,x_n]/(p_1,\dots ,p_r)$, define $F_M(C_A)$ as the subobject of $M^n$ satisfying the polynomial equations $p_i=0$. Ring maps induce maps of these solution objects in the site direction. This is independent of presentation, and it preserves finite limits: finite colimits of finitely presented rings correspond to joining finite generators and equations, whose solution objects are finite limits. Conversely a left-exact functor $F:\mathcal{C}\to \mathcal{E}$ reconstructs a commutative ring $F(C_{\mathbb{Z}[t]})$ using the polynomial maps for addition, multiplication, constants and additive inverse. Presentations by generators and equations then show $F\cong F_M$. Thus flat functors on $\mathcal{C}$ correspond to internal commutative rings.

Under $F_M$, the localization arrow above identifies its domain with the locus where $f_i$ evaluates to a unit; the inverse witness is unique. The family is jointly epimorphic exactly when these unit loci cover the solution object for $A$. The locality axiom implies this for every unit-ideal family: from a finite sum $\sum f_i{g}_i=1$, repeatedly apply the two-summand unit alternative, rescaling a unit partial sum when necessary; some $f_i{g}_i$, hence some $f_i$, is a unit locally. Conversely the cover of $\mathbb{Z}[t]$ by its localizations at $t$ and $1-t$ gives precisely the locality axiom, while the empty cover of the zero ring gives $0=1⊢\perp$. Therefore continuous flat functors are exactly models of the displayed coherent theory. The Diaconescu equivalence for geometric morphisms now identifiesnaturally in $\mathcal{E}$. This proves the asserted classifying topos identification.

Since the site is subcanonical, the generic local ring is the representable sheafIts ring operations are induced by polynomial substitution. Its infinitesimal subobject is likewise representable:Products of representables correspond to tensor products of their rings. For every finitely presented $A$, exponential adjunction and the Yoneda lemma giveEvery element of this ring has a unique expression $a+b\epsilon$, because $1,\epsilon$ form an $A$-basis. This holds even when $A$ has nilpotents or zero divisors. The expression is natural under every ring homomorphism $A\to B$, which sends its two coefficients to their images. The canonical morphism $R\times R\to R^D$, transposed from $(a,b,d)\mapsto a+bd$, is consequently a bijection at every stage $C_A$, with a natural inverse extracting the coefficients. ThereforeThis proves the Kock-Lawvere axiom for the generic local ring. The uniqueness is an internal sheaf assertion tested at all finitely presented rings, including the ring with its generic square-zero element; restricting the test to fields would lose that element and would not prove uniqueness.

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.

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.

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.

For each object $X$, characteristic maps identify $\mathcal{E}(X,\Omega )$ with $\mathrm{Sub}(X)$. These subobject posets carry a natural Heyting algebra structure. Truth and falsity classify $X$ and the empty subobject. Intersections define $\wedge$, unions define $\vee$, and implication is characterized byThese operations commute with pullback, giving arrows on $\Omega$ and the internal Heyting algebra of truth values. Concretely, the order relation on $\Omega$ is the subobject where $p\wedge q=p$; its characteristic map is implication. Negation is $p\Rightarrow \perp$.

If $U\hookrightarrow 1$ has truth value $u:1\to \Omega$, its quasi-closed local operator isThis is double negation relative to the bottom value $u$. In the Heyting algebra interval $[u,1]$, relative implication is inherited and relative negation is $N_u(p)=p\Rightarrow u$. Also $N_u(p)=N_u(p\vee u)$. Therefore the displayed map is the composite of adjoining $u$ and relative double negation. It is inflationary, idempotent, fixes truth and preserves binary meets, so it is a Lawvere-Tierney topology. Its value at bottom is $u$.

The truth values of its sheaf topos are the fixed elements $p=q(U)(p)$. They have bottom $u$, inherited meet and join $q(U)(p\vee r)$. Their relative negation is $N_u(p)$, which is again fixed because $N_u^3=N_u$. The relative double-negation law holds on every fixed element, andThus every subobject in the sheaf topos has a complement: every quasi-closed subtopos is Boolean. This identifies its internal logic, not merely the global truth-value lattice.

Now work in $\mathcal{E}/\Omega$. The arrow $\top :1\hookrightarrow \Omega$ is a subterminal object there; internally it supplies a freely varying generic truth value $u$. Let $a_q$ be sheafification for a local operator for its quasi-closed topology, and let $\pi :\mathcal{E}/\Omega \to \mathcal{E}$ be the slice geometric morphism. The composite $h$ has inverse image $h^{\ast }=a_q{\pi }^{\ast }$.

To prove surjectivity, take any mono $S\hookrightarrow X$ in $\mathcal{E}$, classified by $p:X\to \Omega$. Its pullback along $\pi$ has predicate $p(x)$, independent of the generic $u$. If $h^{\ast }$ sends the mono to an isomorphism, it is $q$-dense in the slice, sofor all $(x,u)$. Pull back this identity along the graph $x\mapsto (x,p(x))$. Substituting $u=p(x)$ gives $q_{p(x)}(p(x))=p(x)$, and therefore $p(x)=1$. Thus the original mono was already invertible.

For parallel arrows $r,s:X\rightrightarrows Y$, equality of their inverse images makes the inverse image of their equalizer invertible. The preceding mono argument makes the equalizer invertible and hence $r=s$. Therefore $h^{\ast }$ is faithful, and the composite is a surjective geometric morphism. A fixed double-negation subtopos can erase information; allowing the generic relative bottom is what detects every original predicate.

For the completeness consequence, let $\mathbb{T}$ be coherent and use its classifying topos with the generic model. Its conservative syntactic interpretation makes an underivable coherent sequent fail as a subobject inclusion. Pulling this model into the Boolean cover constructed above preserves coherent formulas and still refutes that inclusion, because the inverse image is faithful and reflects containment. In the Boolean topos, the difference between antecedent and consequent is a nonzero complemented subobject. Slicing over that difference gives a nondegenerate Boolean topos with a global tuple satisfying the antecedent and the negation of the consequent.

Classical first-order deduction is sound in a Boolean topos. Hence $\mathbb{T}$ together with constants for that tuple, the antecedent and the negated consequent is classically consistent: a proof of contradiction would hold in the nondegenerate sliced model. The ordinary Henkin construction supplies a set model of this consistent theory. Briefly, extend it by witness constants, complete it to a maximal consistent theory, form the term structure modulo provable equality, and prove the truth lemma by induction on formulas. For possibly empty sorts use the standard encoding by sort predicates and functional graph relations, without asserting sort inhabitance; the constants for the chosen tuple assert only the needed witnesses. The resulting set model is a countermodel to the original sequent.

Consequently a coherent sequent valid in every set-valued model of a coherent theory is derivable in coherent logic. The Boolean cover supplies the crucial passage from the generic intuitionistic countermodel to consistency with classical negation; the final set-model step uses ordinary first-order completeness via its Henkin proof, rather than an assumption that every Boolean topos has points.

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.

Adding coherent or geometric axioms to a theory determines a coverage on a site for its classifying topos. The antecedent presentation is covered by presentations where its consequent disjuncts and witnesses hold. Sheafification imposes those axioms on the generic model. An inconsistent antecedent gets an empty cover.

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.