Completeness theorem

First suppose that \(T\) is coherent. By Proposition 6.113, there is a finitary site \((C,\tau)\) with finite limits and an equivalence \(T^{\hyp}\simeq\Shv_\tau(C)^{\hyp}\). The composite \(T^{\hyp}\to T\) is surjective, so it is enough to construct a surjection onto \(\Shv_\tau(C)^{\hyp}\).By Corollary 6.124, there exists a complete Boolean algebra \(\Lambda\) and a surjection \(\Shv(\Lambda) \twoheadrightarrow \Shv_{\tau}(C)\). We claim that this factors as follows: Since \(C\) has finite limits, the given morphism of topoi \(\Shv(\Lambda) \to \Shv_{\tau}(C)\) corresponds to a morphism of logoi \(\Shv_{\tau}(C) \to \Shv(\Lambda)\), which is obtained by left Kan extending some left exact functor \(C \to \Shv(\Lambda)\). We may then consider the following composite: This is still left exact. Since \(\tau\) is finitary, it suffices for descent that finite covering families be carried to effective epimorphisms, and this follows from Lemma 6.125. We therefore obtain a morphism of topoi \(\Shv(\Spec(\Lambda)) \to \Shv_\tau(C)\). Since \(\phi^*\phi_*\simeq\id\) by full faithfulness of \(\phi_*\), its composite with \(\Shv(\Lambda)\to\Shv(\Spec(\Lambda))\) is the original surjection. Right cancellation shows that \(\Shv(\Spec(\Lambda))\to\Shv_\tau(C)\) is itself surjective.For every point \(x\in\Spec(\Lambda)\), the stalk functor gives a point \(\An\to\Shv(\Spec(\Lambda))\). Their coproduct defines a surjection because stalks at all points jointly detect isomorphisms of sheaves on a topological space. The source is hypercomplete, so the composite with \(\Shv(\Spec(\Lambda))\to\Shv_\tau(C)\) factors through the hypercompletion \(\Shv_\tau(C)^{\hyp}\). The factor remains surjective, and composing with \(T^{\hyp}\to T\) proves the theorem for coherent \(T\).Finally, suppose that \(T\) is only locally coherent. Choose a set of coherent objects \((U_i)_{i\in I}\) covering the terminal object. Then \(\prod_{i\in I}T_{/U_i}\to T\) is surjective, and every slice \(T_{/U_i}\) is coherent. Applying the coherent case to each slice and taking the product of the resulting sets gives a surjection \(\An^S\to T\) for a set \(S\).