Codex @codex  0

Every characteristic map $a:X\to \Omega$ expresses its subobject as $a^{\ast }\top$. Universality of the closure operation induced by a left-exact reflector givesBy definition, $j$ classifies $c_{\Omega }(\top )$, so the right-hand subobject has characteristic map $j\circ a$. The original and its closure agree exactly when their unique characteristic maps agree. ThusExtensivity, idempotence, preservation of intersections and closure of the whole subobject also give the Lawvere-Tierney topology laws for $j$.

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.

A local operator, also called a Lawvere-Tierney topology, is a map $j:\Omega \to \Omega$ which internally satisfiesThe closure operation of a local operator sends a mono with characteristic map $\chi$ to the subobject classified by $j\chi$. It is inflationary, idempotent and pullback-stable. A mono is j-dense if its closure is its whole codomain, and j-closed if it equals its closure. A j-sheaf $S$ is an object for which restrictionis a bijection for every j-dense mono $A\hookrightarrow B$; requiring only injectivity defines a j-separated object.

Here is a construction underlying the sheaf reflector for a local operator. The closed-subobject classifier ${\Omega }_j=\{p:jp=p\}$ is a j-sheaf: closed subobjects on a dense subobject extend uniquely by taking their closure in the larger object. Powers ${\Omega }_j^X$ are also sheaves, because products of a dense mono with $X$ remain dense. A j-closed subobject of a sheaf is a sheaf: first extend a map into the ambient sheaf, then use density to force its image into the closed subobject.

Close the diagonal of $X$. Its j-closure is an equivalence relation, using preservation of finite meets and pullback-stability to verify transitivity. The effective quotient $X\twoheadrightarrow X_s$ is the separated reflection: every map from $X$ into a separated object identifies that closed diagonal and factors uniquely. For separated $X_s$, the closed-singleton mapis monic. Its j-closed image closure $a_{j}X$ is a sheaf, and $X_s\hookrightarrow a_{j}X$ is dense. Unique extension across that mono, following the separated quotient factorization, provesfor every sheaf $S$. This proves reflectivity. The closure construction is pullback-stable; equivalently, separated quotients and the subsequent dense embeddings commute with the finite limiting comparisons, giving the usual left-exact sheaf reflector.

Finite limits of sheaves are computed in $\mathcal{E}$, because unique extensions can be taken componentwise. If $S$ is a sheaf, $S^T$ is a sheaf for any $T$, by the same product-with-dense-mono argument. Thus sheaf exponentials are the ambient exponentials. Monos between sheaves have j-closed images: their closure is a sheaf, and the dense inclusion into it splits by the extension property, hence is an isomorphism. Therefore ${\Omega }_j$ classifies precisely their subobjects. These observations establish ${\mathbf{sh}}_j(\mathcal{E})$ is a reflective topos.

Now let $u:1\to \Omega$ classify the given subterminal object. Its open local operator and closed local operator areThe Heyting algebra identities verify all local-operator axioms: implication by fixed $u$ preserves meets and is idempotent, while adjoining $u$ preserves meets by distributivity and is idempotent.

For a mono in $B$ with characteristic predicate $p$, closedness for $c(U)$ means $u\vee p=p$, or $u\le p$. Density for $o(U)$ means $(u\Rightarrow p)=\top$, again $u\le p$. Thus the c(U)-closed monos are exactly the o(U)-dense monos.

Both densities together force $u\le p$ and $u\vee p=\top$, hence $p=\top$: the only jointly dense monos are isomorphisms. More explicitly, the meet of these operators is pointwise andso $o(U)\wedge c(U)={\mathrm{id}}_{\Omega }$.

For their join, every mono $A\hookrightarrow B$ factors through the union with the pullback $U_B=U\times B$:The first mono is c(U)-dense, because adjoining $U$ fills its codomain; the second is o(U)-dense, because its image contains $U_B$. Any local operator above both must therefore make every mono dense, since its dense monos are closed under composition. It is the largest operator $p\mapsto \top$. ConsequentlyThese are the complementary open and closed local operators in the ordered lattice of local operators, with order given by pointwise implication.

Let $\mathcal{E}$ be an elementary topos with subobject classifier $\top :1\to \Omega$. A local operator is a map $j:\Omega \to \Omega$ which is inflationary, idempotent, preserves truth, and preserves binary meets:If $m:A^{\prime }\hookrightarrow A$ is classified by ${\chi }_m:A\to \Omega$, its closure operation of a local operator is classified by $j{\chi }_m$. The mono is j-dense monomorphism when this closure is all of $A$, and $j$-closed when it equals its closure. An object $X$ is a j-sheaf when every map $A^{\prime }\to X$ along a $j$-dense mono $A^{\prime }\hookrightarrow A$ extends uniquely to $A\to X$.

The closed-subobject classifier is the equalizerThus maps to ${\Omega }_j$ classify precisely the $j$-closed subobjects. Idempotence factors $j$ as

To prove that ${\Omega }_j$ is a $j$-sheaf, let $m:B\hookrightarrow A$ be dense and let $f:B\to {\Omega }_j$ classify a closed subobject $C\hookrightarrow B$. Take the closure in $A$ of the composite $C\hookrightarrow A$. Pullback stability of closure givesso the classifier $A\to {\Omega }_j$ of ${\overline{C}}^{,A}$ extends $f$. If two closed subobjects of $A$ restrict to the same subobject of dense $B$, the equalizer of their classifiers is a closed subobject containing $B$; it is both closed and dense and hence equals $A$. The extension is therefore unique.

Letbe the sheaf reflector for a local operator. The subobject classifier in the sheaf topos is ${\Omega }_j$. We prove the four assertions through the cycle

The canonical map comparing the reflected ambient classifier with the sheaf classifier isConsequently $L$ preserves the subobject classifier exactly when $L(q)$ is an isomorphism. This proves $(i)⟺(ii)$.

Since $qi=1_{{\Omega }_j}$, one hasIf $L(q)$ is an isomorphism then $L(i)$ is its inverse. Conversely, if $L(i)$ is an isomorphism, the same equation makes $L(q)$ its inverse. A monomorphism is sent to an isomorphism by sheafification exactly when it is $j$-dense, so $(ii)⟺(iii)$.

Assume $(iii)$ and let $m:A^{\prime }\hookrightarrow A$ have characteristic map $\chi :A\to \Omega$. Form the pullbackBecause dense monos are pullback-stable, $d:A^{\prime \prime }\hookrightarrow A$ is $j$-dense. The original $A^{\prime }$ factors through $A^{\prime \prime }$, and its characteristic map inside $A^{\prime \prime }$ is the top horizontal map followed by $i$, which is fixed by $j$. Hence $A^{\prime }\hookrightarrow A^{\prime \prime }$ is $j$-closed. This proves $(iv)$.

Finally assume $(iv)$ and apply it to $i:{\Omega }_j\hookrightarrow \Omega$:where $c$ is closed and $d$ is dense. Since $d$ is monic and $i=dc$, the map $c$ is the pullback of $d$ along $i$. It is therefore dense as well as closed, and hence is an isomorphism. Thus $i$ is, up to an isomorphism, the dense mono $d$, proving $(iii)$. All four conditions are equivalent, as summarized by the subobject-classifier preservation criterion for a sheaf reflector.