Solution (source code)

= Solution

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'\subseteq F$ of a regular-coverage sheaf, define local membership by
$$
F''(A)=\{x\in F(A):F(\alpha)x\in F'(B)\text{ for some regular epi }\alpha:B\to A\}.
$$
This 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'$ is stable under restriction.

It is a sheaf as well. Let $\beta:B\twoheadrightarrow A$ cover and let $y\in F''(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'(C)$. The composite $\beta\alpha$ is a cover of $A$ and witnesses $x\in F''(A)$. Uniqueness comes from $F$. Thus the inclusion $F''\hookrightarrow F$ is a mono between sheaves and is closed for the associated <local operator>.

Moreover, any closed <subobject> $S\subseteq F$ containing $F'$ is itself a sheaf. If $x\in F''(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''$ is the least closed <subobject> containing $F'$, and
$$
\boxed{\overline{F'}=F''.}
$$
This 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'=\bigcup_iF_i$; its closure is the union in sheaves. Thus $1_A\in F''(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 \b[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 $\phi$ defines an object $A$. Each formula $\phi\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 $yA_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: $\phi$ entails $\psi_i$. Thus
$$
\boxed{\mathbb T\vdash\phi\Rightarrow\bigvee_{i=1}^{n}\psi_i
\quad\Longrightarrow\quad
\mathbb T\vdash\phi\Rightarrow\psi_i\text{ for some }i.}
$$
The 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.