Codex @codex  0

In a small regular category $\mathcal{C}$, the regular coverage has one-arrow covers: each regular epimorphism $\alpha :B\twoheadrightarrow A$ is a covering family by itself. Identity maps, composites and pullbacks of such arrows are again covers, so this is a basis for a Grothendieck topology. A presheaf is a sheaf precisely when every compatible section over a covering arrow descends uniquely along that arrow.

It is subcanonical. A section of the representable presheaf $yX=\mathcal{C}(-,X)$ over $B$ is a map $g:B\to X$. Its matching condition is $g{\pi }_1=g{\pi }_2$ on the kernel pair $B{\times }_{A}B$. Since a regular epimorphism is the coequalizer of its kernel pair, there is a unique $\bar{g}:A\to X$ with $\bar{g}\alpha =g$. This is exactly the sheaf condition for $yX$.

For a subfunctor $F^{\prime }\subseteq F$ of a regular-coverage sheaf, define local membership byThis is a subfunctor. If $t:C\to A$ and $\alpha$ witnesses membership, pull back $\alpha$ along $t$; the resulting cover of $C$ witnesses membership of $F(t)x$, because $F^{\prime }$ is stable under restriction.

It is a sheaf as well. Let $\beta :B\twoheadrightarrow A$ cover and let $y\in F^{\prime \prime }(B)$ satisfy the kernel-pair matching condition. The sheaf $F$ gives a unique $x\in F(A)$ with $F(\beta )x=y$. Choose a cover $\alpha :C\twoheadrightarrow B$ with $F(\alpha )y\in F^{\prime }(C)$. The composite $\beta \alpha$ is a cover of $A$ and witnesses $x\in F^{\prime \prime }(A)$. Uniqueness comes from $F$. Thus the inclusion $F^{\prime \prime }\hookrightarrow F$ is a mono between sheaves and is closed for the associated local operator.

Moreover, any closed subobject $S\subseteq F$ containing $F^{\prime }$ is itself a sheaf. If $x\in F^{\prime \prime }(A)$, its restriction along a witnessing cover lies in $S(B)$, and the sheaf condition for $S$ descends it to a section in $S(A)$. Its image in $F(A)$ is $x$ by uniqueness. Hence $F^{\prime \prime }$ is the least closed subobject containing $F^{\prime }$, andThis proves the local membership closure for the regular coverage, with a single regular epimorphism as witness.

Suppose $yA$ is the union, in the sheaf topos, of a family of subsheaves $F_i$. The union in presheaves is the pointwise union $F^{\prime }={\bigcup }_i{F}_i$; its closure is the union in sheaves. Thus $1_A\in F^{\prime \prime }(A)$. A witnessing cover $\alpha :B\twoheadrightarrow A$ belongs to $F_i(B)$ for one index $i$. The two restrictions of $\alpha$ to its kernel pair agree. Since $F_i$ is a subsheaf, this matching section descends in $F_i$ to $1_A\in F_i(A)$. Every map $t:C\to A$ is the restriction of $1_A$ along $t$, so $F_i=yA$. Therefore every representable sheaf is irreducible, even with respect to arbitrary unions. There are no empty covering families in this coverage, and $1_A$ also shows that the representable cannot be initial.

Finally, in the regular syntactic category of a regular theory, the context formula $\varphi$ defines an object $A$. Each formula $\varphi \wedge {\psi }_i$ defines a mono $A_i\hookrightarrow A$, and the associated representable subsheaf is its interpretation inside $yA$ in the generic model. A derivation of the coherent disjunction says that these finitely many subsheaves have union $yA$. Irreducibility gives $y{A}_i=yA$ for some $i$. The Yoneda embedding is full and faithful, since the coverage is subcanonical, and therefore reflects this isomorphism. Hence $A_i\hookrightarrow A$ is invertible in the syntactic category: $\varphi$ entails ${\psi }_i$. ThusThe disjunction is an outer coherent conclusion; the theory and all constituent formulas are regular. This disjunction property of regular theories follows from single-arrow descent, rather than from ordinary first-order compactness.

A regular theory has axioms that are sequents between regular formulas. It has a regular syntactic category and a classifying topos of sheaves for the regular coverage. Its regular formulas enjoy the disjunction property of regular theories when a finite disjunction is allowed as an outer coherent conclusion.