I'm trying to understand the proof of the Barr-Diaconescu theorem about Boolean covers for Grothendieck sites. Precisely, the versions you can find in Jardine's book "Local Homotopy Theory" or in Mac Lane - Moerdijk "Sheaves in Geometry and Logic", which are essentially the same. That is,

Theorem. For every Grothendieck topos $\mathcal{E}$ there exists a complete Boolean algebra $\mathcal{B}$ and a topos morphism $p: \mathbf{Sh}(\mathcal{B}) \longrightarrow \mathcal{E}$ such that the inverse image functor $p^* : \mathcal{E} \longrightarrow \mathbf{Sh}(\mathcal{B}) $ is faithful.

Particularly, I'm having troubles with something that must be definitively elementary. In both books the first step goes like this: you take a Grothendieck site $\mathcal{X}$ such that $\mathcal{E} = \mathbf{Sh}(\mathcal{X})$ and you consider the poset of strings of arrows $\mathbf{String}({\mathcal{X}})$ of $\mathcal{X}$, where a string is a sequence of composable arrows in $\mathcal{X}$,

$$ s = \left( U_n \stackrel{\alpha_n}{\longrightarrow} U_{n-1} \stackrel{\alpha_{n-1}}{\longrightarrow} \dots \stackrel{\alpha_1}{\longrightarrow} U_0 \right) $$

These strings carry a natural partial order, both books say (and here, perhaps, begins my problem):

For two strings $s$ and $t$ we write $t \leq s$ if $t$ prolongs $s$ to the left.

That is, for a string $s$ like the one above, $t$ must be of the form

$$ t = \left( U_{n+m} \longrightarrow \dots \longrightarrow U_{n+1} \longrightarrow U_n \stackrel{\alpha_n}{\longrightarrow} \dots \longrightarrow U_0 \right) \ . $$

So far so good, but, if I understand everything correctly, now this poset $\mathbf{String}({\mathcal{X}})$ must also be a frame. Because: (1) Mac Lane-Moerdijk says so in his theorem 1; (2) also because the second step of the Diaconescu-Barr theorem (theorem 3.39 in Jardine's book, lemma 3 in Mac Lane-Moerdijk's one) says:

Proposition. For every frame $\mathcal{S}$ there exists a complete Boolean algebra $\mathcal{B}$ and a topos morphism $i: \mathbf{Sh}(\mathcal{B}) \longrightarrow \mathbf{Sh}(\mathcal{S})$ such that the inverse image functor $i^*: \mathbf{Sh}(\mathcal{S}) \longrightarrow \mathbf{Sh}(\mathcal{B}) $ is faithful.

Hence, you put $\mathcal{S} = \mathbf{String}({\mathcal{X}}) $ in this proposition and you are done: you have the Diaconescu-Barr theorem proved for you. Notice, however, that in the proof of this proposition you do indeed need the frame structure of $\mathcal{S}$.

Ok, so my question is the following:

Question. Which are the meets $\wedge$ and joints $\vee$ of the frame $\mathbf{String}({\mathcal{X}})$?

Neither book says anything about them, so I imagine this must be an easy exercise -that I'm unfortunately unable to solve.

Let me explain my lack of understanding to you.

(1) As for joints, I would say that, given strings

$$ s = \left( U_n \stackrel{\alpha_n}{\longrightarrow} U_{n-1} \stackrel{\alpha_{n-1}}{\longrightarrow} \dots \stackrel{\alpha_1}{\longrightarrow} U_0 \right) $$


$$ t = \left( V_m \stackrel{\beta_m}{\longrightarrow} V_{m-1} \stackrel{\beta_{n-1}}{\longrightarrow} \dots \stackrel{\beta_1}{\longrightarrow} V_0 \right) $$

their meet could be something like the $0$-string

$$ s \vee t = U_0 \sqcup V_0 \ , $$

where $\sqcup$ is the coproduct in the category $\mathcal{X}$: by definition, we have morphisms $U_0 \longrightarrow U_0 \sqcup V_0 \longleftarrow V_0$, so both $s$ and $t$ prolong $s\vee t$ to the left. Right.

But: the existence of coproducts is not included in the definition of the Grothendieck site $\mathcal{X}$, is it?

(2) As for meets, my lack of understanding is even worse: if $s \wedge t$ should prolong both $s$ and $t$ to the left, then I cannot imagine how every pair of strings $s$ and $t$ could have a meet.

Because, if there is a string $s\wedge t$ that prolongs both $s$ and $t$ to the left, then shouldn't $s$ and $t$ be essentially the same string (except for having, perhaps, some arrows deleted in one of them with respect to the other)?

I guess the answers to my questions are pretty obvious, but at this moment I'm stuck with them. What am I missing? Thank you for your help, even if you embarras me a lot.

  • 2
    $\begingroup$ There is no claim that $\text{String}(\mathcal{X})$ is a frame, at least not in Mac Lane-Moerdijk. And indeed it's not (for example, there is no bottom element). $\endgroup$ – Todd Trimble Sep 6 '16 at 12:31
  • $\begingroup$ @Trimble. Yep, you're right. Although, on the one hand, the statement in Mac Lane-Moerdijk says: "there exists a locale...". But, on the other hand, as godelian points out, it's true: $\mathbf{String}(\mathcal{X})$ needs not be a locale (a frame) but just a poset, and then the topos $\mathbf{Sh}\mathbf{String}(\mathcal{X}) $ is localic because of their theorem 5.1. Maybe the authors should have mention theorem 5.1 in this proof. Anyway, thank you both for helping me in this issue. $\endgroup$ – Agustí Roig Sep 6 '16 at 12:53
  • 2
    $\begingroup$ But they did mention theorem 5.1! At least in the 2nd edition they did. $\endgroup$ – Todd Trimble Sep 6 '16 at 13:05
  • $\begingroup$ @Trimble. Again, you're right. Page 514, third paragraph. My bad: read the sentence and the whole proof several times, and instead the conclusion eluded me. :-( $\endgroup$ – Agustí Roig Sep 6 '16 at 14:44

I think that the missing step is to build the locale $X$ from your poset of strings. But you should not look for a frame structure in the poset; rather, you are supposed to apply Theorem 5.1 in Maclane-Moerdijk to get that locale. If the site of the topos is a poset, the proof of that theorem (which uses in turn Giraud's theorem in the appendix of the same book) says that the topos is equivalent to the localic topos $\mathcal{S}h(X)$, where $X$ is the poset of subobjects of $1$, hence equipped with the operations you want.

  • $\begingroup$ Thank you, godelian. I think you're right: I forgot the theorem you mention. $\endgroup$ – Agustí Roig Sep 6 '16 at 12:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.