Plus construction of a presheave factors every sheaf-valued morphism.

I'm having some trouble understanding the correctness of some proof in Sheaves in Geometry and Logic (Mac Lane, Moerdijk). It concerns the lemma III.5.3 :

If $F$ is a sheaf and $P$ a presheaf, then any map $\phi \colon P \to F$ of presheaves factors uniquely through $\eta$ as $\phi = \tilde\phi \circ \eta$.

$$\begin{matrix} P & \stackrel \eta \to & P^+ \\ & \!\!\!\!\!\!_\phi\searrow & \downarrow \small{\tilde\phi} \\ & & \!\!\!\!F\end{matrix}$$

Recall the plus construction : $P^+(C)$ is the equivalent class of matching families under the relation $(x_f)_{f\in S} \sim (y_g)_{g \in R}$ ($R,S$ covering sieves of $C$) iff there is some covering sieve $T \subseteq S \cap R$ on which $x_f = y_f$ forall $f \in T$.

Recall the morphism $\eta$ : $$\eta_C \colon P(C) \to P^+(C),\, x \to [(Pf(x))_{f \colon D \to C}].$$

I easily understand the definition of $\tilde\phi_C(\mathbf x)$ for some equivalent class $\mathbf x = (x_f)_{f\in S}$ : we push the matching family $(x_f)$ by $\phi_C$ into a matching family of $F$ ; being a sheaf, $F$ admit a unique amalgamation in $F(C)$ that we define to be $\tilde\phi_C(\mathbf x)$. The well-definition is no problem. What bother me is to check that $\tilde\phi = (\tilde\phi_C)_C$ is actually natural in C.

We want a commutative diagram $$\begin{matrix} P^+C & \stackrel {Ph} \to & P^+D \\ \small{\tilde\phi_C}\downarrow \ \ \ & & \ \ \ \downarrow\small{\tilde\phi_D} \\ FC & \stackrel{Fh} \to & FD \end{matrix}$$ for all $h \colon D \to C$. For an element $\mathbf x = (x_f)_{f\in S}$, and $h \in S$, the stability axiom of Grothendieck topologies assure $h^\ast S = \hom(-, D)$, and so the commutativity is immediat from the definition of $\tilde\phi_C(\mathbf x)$ as amalgamation.

But I'm stuck with the case where $h \notin S$, and (it seems to me that) it is not treated in the proof of Mac Lane. Maybe can we always find $\mathbf y = (y_g)_{g\in R}$ with $\mathbf x \sim \mathbf y$ and $h \in R$, but I can't see it.

-
General advice: if you're doing topos theory, you can almost always do everything intuitionistically; in particular, you should not need to appeal to the law of excluded middle. So don't do case analysis! – Zhen Lin May 15 '13 at 11:00
@ZhenLin I know that because of the structure of internal Heyting algebra of the subobject classifier, a topos is a suitable universe for intuitionistic logic based mathematics. But doesn't it concern the internal logic of the topos ? That is, people working inside the topos are working without excluded middle. However, the construction of the topos itself is relative to the external logic of the mathematician defining it, which isn't necessarily intuitionistic. (I don't claim anything, just thinking out loud.) – Pece May 15 '13 at 13:17
Yes, but that's not what I mean. There is a notion of $\mathcal{S}$-topos, where $\mathcal{S}$ is another topos, which one thinks of as being a topos "based on" $\mathcal{S}$, and there is a surprising amount of topos theory that carries over to this relative context including, yes, the machinery of Grothendieck topologies. The whole of Part B of Sketches of an elephant is devoted to relative topos theory. – Zhen Lin May 15 '13 at 14:26
@ZhenLin Ok, looking as Johnstone's book, it seems a little advanced for my current knowledge. Howerver, maybe can I think of it as follow : taking an elementary topos $\mathcal S$, it can be used as a universe to found mathematics (Lawvere's ideas) ; then I can internally define the notions of category, Grothendieck topology and sheaves (as far as it doesn't require excluded middle arguments) to have a internal theory of topos. Is that something of that kind ? – Pece May 15 '13 at 14:35
Something like that. Doing things internally in $\mathcal{S}$ is a bit too restrictive, however; it would be like working only with small categories. – Zhen Lin May 15 '13 at 15:17

Let me write $w$ for the equivalence class in $P^{+}C$ of a matching family $(x_{f})_{f\in R}$ for a covering sieve $R$ of $C$. Now the down-right path sends $w$ to $Fh(y)$, where $y$ is the only amalgamation for the matching family $(\phi_{dom (f)}(x_{f}))_{f\in R}$. The right-down path maps $w$ to $z\in FD$, where $z$ is the only amalgamation for $(\phi_{dom (hf')}(x_{hf'}))_{f'\in h^{\ast}(R)}=:k$ (recall the definition of $P^{+}h$ for an arrow $h$). In order to show that going the two way gives the same result it suffices to show that $Fh(y)$ is an amalgamation of $k$: if $f'\in h^{\ast}(R)$ $$Ff'(Fh(y))=(F(hf'))(y)=\phi_{dom (hf')}(x_{hf'})$$ where the last equality is by definition of $y$ and we are done. I hope it's clear enough (fill in the details!) and that I didn't make some mistakes.

-
Well, it is pretty straightforward. I just did not see it. Thanks a lot. (If you have the Mac Lane-Moerdijk at hand, do you agree that this is skipped ?) – Pece May 15 '13 at 10:04
Yes, that proof is quite weird; somehow the only thing they really show is that $\tilde\phi$ makes $\phi$ factorizing through $\eta$. – Marco Vergura May 15 '13 at 10:11

I don't know about you, but I find the whole business with equivalence classes very confusing. Looking at the question from a more category theoretical point of view should make it easier:

Let $P$ be a $\mathscr A$-valued presheaf on a site $\mathscr C$ and $X\in \mathscr C$. Then for any covering family $\mathscr U=\{U_i\rightarrow X\}$, define $P_X(\mathscr U)$ as the equalizer of the sequence $$P_X(\mathscr U)\rightarrow \prod_i P(U_i)\rightrightarrows \prod_{i,j}P(U_i\times_XU_j).$$ Further define $P^+(X)$ as the colimit $$P^+(X)=colim_{\mathscr U}P_X(\mathscr U)$$ running over all covering families $\mathscr U$ of $X$.

Then the universal property gives you immediately the morphism $\eta: P\to P^+$, and also a morphism $\tilde \phi: P^+\to F^+=F$. Being defined via the universal property, naturality should be easy to check.

To see how you get a morphism $P\to P^+$, note that the restriction map

$$P(X)\to \prod_i P(U_i)$$ induces a map $P(X)\to P_X(\mathscr U)$ via the universal property of the equalizer. Now the colimit comes with maps $P_X(\mathscr U)\to P^+(X)$, which after composition yields $P(X)\to P^+(X)$. This is independent of the choice of the covering, because for a refinement $\mathscr V=\{V_i\rightarrow X\}$ of $\mathscr U$, the diagram

$$\begin{matrix} P(X) & \to & P_X(\mathscr U) \\ & \searrow & \downarrow \\ & & \!\!\!\!P_X(\mathscr V)\end{matrix}$$

commutes.

-
I agree that the description by equivalence classes is kind of heavy. But I was trying to understand the proof of the book so stuck to it. However, I miss something in your argument : how the universal property could give an arrow $P \to P^+$ ? Doesn't the universal property of colimit provide morphism from the colimit ? – Pece May 15 '13 at 13:09
Yes, I tried working with the book as well at one point, but chose a different path in the end. Does the edit make sense? – Simon Markett May 15 '13 at 13:56
Thanks for the edit. I expected something like that because the maximal covering $\mathscr U = \hom(-, X)$ gives easily rise to the $\eta$ I depicted. I didn't notice that this morphism is independent of $\mathscr U$ until you pointed it out. I think I now get it completely. Thanks. – Pece May 15 '13 at 14:06