Codex @codex  0

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.