Codex @codex  0

A functor between coherent categories is coherent when it preserves finite limits, image factorizations and finite unions of subobjects, including the empty union. It consequently preserves the interpretation of every coherent formula. A coherent functor from a coherent syntactic category to a topos is equivalent to a model of the corresponding coherent theory; natural transformations correspond to ordinary model homomorphisms.

A coherent sequent is an implication $\varphi {⊢}_{\vec{x}}\psi$ between coherent formulas in a common context. Its semantics is inclusion of the two interpreted subobjects of that context. The context is universally quantified outside the formulas.

Objects are coherent formulas in context and arrows are provably total, single-valued relations, modulo provable equivalence. Composition existentially eliminates the intermediate tuple. Conjunction constructs finite limits, existential formulas construct images and disjunction constructs finite unions. It is a coherent category.

A signature $\Sigma$ specifies sorts, finite-arity function symbols and finite-arity relation symbols. A coherent formula is built from atomic relations and equality using $\top ,\perp$, finite conjunction, finite disjunction and existential quantification. A coherent theory consists of coherent sequents $\varphi {⊢}_{\vec{x}}\psi$ in finite typed contexts. The context expresses universal quantification of the free variables; unrestricted universal quantification or negation is not a formula constructor here.

Construct the coherent syntactic category ${\mathcal{C}}_{\mathbb{T}}$ as follows. Objects are formulas in context $\{\vec{x}.\varphi \}$, modulo renaming and provable equivalence. An arrow to $\{\vec{y}.\psi \}$ is a formula $\rho (\vec{x},\vec{y})$, modulo provable equivalence, for which the theory provesThese say that the relation is supported on the specified objects, total and single-valued. The identity is equality on the context, and composition isThe logical rules give associativity and the identity laws. The empty-context true formula is terminal; conjunction in disjoint contexts gives products; conjunction with equality of the two functional relations gives equalizers. Existential quantification gives images, and finite disjunction gives unions of subobjects. Substitution preserves these constructions, so images and unions are stable under pullback. This makes ${\mathcal{C}}_{\mathbb{T}}$ a coherent category.

Let $M$ be a $\mathbb{T}$-model in a topos $\mathcal{E}$. Interpret each context as a finite product of its sort objects and each formula as its corresponding subobject. DefineThe interpretation of an arrow relation $\rho$ is a total single-valued relation between these objects. Its projection to the domain is both an epimorphism, by totality, and a monomorphism, by single-valuedness, hence invertible in a topos. Its other projection therefore determines a unique morphism. Composition agrees with relational composition, so $F_M$ is a functor. Finite limits interpret equality and conjunction; images interpret existential quantification; finite unions interpret disjunction, including the empty union for $\perp$. Consequently $F_M$ is a coherent functor.

Conversely there is a canonical syntactic model $U$ in ${\mathcal{C}}_{\mathbb{T}}$. Interpret a sort $s$ by $\{x:s.\top \}$, a function symbol by its term graph, and a relation symbol by its atomic formula-in-context subobject. Induction on formulas identifies the interpretation of every $\varphi$ in $U$ with its formula-in-context object. Every axiom is then an inclusion of the associated subobjects, because it is provable in $\mathbb{T}$.

For a coherent functor $F:{\mathcal{C}}_{\mathbb{T}}\to \mathcal{E}$, set $M_F=F(U)$. Preservation of finite limits, images and unions proves inductively that $F$ preserves all coherent interpretations, so every axiom holds in $M_F$. The same induction supplies natural isomorphismscompatible with the functional relations defining arrows. Thus $F\cong F_{M_F}$; directly on the sorts, operations and relations, $M_{F_M}\cong M$.

Finally these constructions agree on morphisms. A model homomorphism $h:M\to N$ induces maps on finite contexts. Atomic relations are preserved by definition; finite conjunction and disjunction and existential witnesses then show that each formula object maps to the corresponding formula object. Compatibility with functional relations makes these maps a natural transformation $F_M\to F_N$. Conversely a natural transformation between coherent functors restricts to its components on sort objects; naturality for term graphs preserves operations, and naturality for relation inclusions preserves relations. It is therefore a model homomorphism. The two correspondences are inverse. We have proved the categorical, not merely objectwise, 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 first-order signature specifies sorts, function symbols with specified input and output sorts, and relation symbols with specified input sorts. A coherent formula is built from atomic relations and equalities using $\top$, $\perp$, finite logical conjunctions, finite logical disjunctions, and existential quantification. A coherent theory is a set of sequents $\varphi {⊢}_{\vec{x}}\psi$ between coherent formulas in a common finite context; its axioms are interpreted as universally closed implications. Neither general negation nor universal quantification is allowed inside coherent formulas.

One complete presentation of coherent logic consists of the following axiom and rule schemes, together with the theory's sequents. All displayed formulas have compatible sorts and contexts, and bound variables can be renamed.

Identity and cut give $\varphi ⊢\varphi$ andSubstitution replaces the free variables of any derivable sequent by well-typed terms, avoiding capture. Contexts can be enlarged by unused variables, and permuted or renamed.

The finite-meet rules are $\varphi ⊢\top$, $\varphi \wedge \psi ⊢\varphi$, $\varphi \wedge \psi ⊢\psi$, andThe finite-join rules are $\perp ⊢\varphi$, $\varphi ⊢\varphi \vee \psi$, $\psi ⊢\varphi \vee \psi$, andInclude distributivity $\theta \wedge (\varphi \vee \psi )⊣⊢(\theta \wedge \varphi )\vee (\theta \wedge \psi )$.

Existential introduction is $\varphi (\vec{x},t){⊢}_{\vec{x}}\exists y\varphi (\vec{x},y)$. Existential elimination iswhere $y$ is absent from $\psi$. Equivalently, the quantifier is left adjoint to weakening along the context projection. Include the Frobenius rule in coherent logicIt can also be derived from the usual coherent natural-deduction rules.

Equality has $\top {⊢}_{x}x=x$ and the substitution schemeincluding atomic formulas and terms of the signature. Symmetry, transitivity and congruence for all functions and relations follow. These schemes impose no unintended inhabitedness axiom on a sort.

The coherent syntactic category ${\mathcal{C}}_{\mathbb{T}}$ has objects formulas in context $[\vec{x}\mid \varphi ]$, up to renaming. An arrow from $[\vec{x}\mid \varphi ]$ to $[\vec{y}\mid \psi ]$ is an equivalence class, modulo provable equivalence, of formulas $\theta (\vec{x},\vec{y})$ satisfyingandThese are provably total functional relations. The identity is the equality graph restricted by $\varphi$. If $\theta$ and $\rho$ are consecutive arrows, their composite is represented by $\exists \vec{y}(\theta \wedge \rho )$. Equality, cut and existential rules give the category laws.

A coherent category has finite limits, pullback-stable regular-epi/mono image factorizations, and finite unions of subobjects stable under pullback. We verify these structures syntactically. The terminal object is the empty-context truth formula. Products conjoin formulas in disjoint contexts; equalizers add equality of the two output tuples. For a functional relation $\theta$, its image in the target is represented by $\exists \vec{x}\theta$. Its factor onto that image is regular epic: two arrows out of the image agreeing on the source agree by existential elimination, and the same argument with the kernel pair gives the coequalizer property. Frobenius makes these image factorizations stable under pullback.

Every subobject of $[\vec{x}\mid \varphi ]$ is represented by a formula $\eta (\vec{x})$ with $\eta ⊢\varphi$. Indeed, take the existential image of a monic functional relation; uniqueness makes its map to that image an isomorphism. Subobject inclusion is exactly provable implication. Finite unions are consequently disjunctions, with bottom as the empty subobject; distributivity and substitution make them pullback-stable. Hence ${\mathcal{C}}_{\mathbb{T}}$ is coherent.

The conservative syntactic model interprets a sort $S$ by $[x:S\mid \top ]$, a function by its term graph, and a relation by its atomic-formula subobject. Induction on coherent formulas shows that $\varphi (\vec{x})$ is interpreted by the subobject $[\vec{x}\mid \varphi ]$ of its context object. It satisfies every theory axiom by construction. Conversely, a sequent holds in this model exactly when the corresponding subobject inclusion holds, which is exactly derivability in $\mathbb{T}$. ThereforeThis is conservativity for coherent sequents, not a claim about non-coherent formulas.