Fix a proof in proetale

This was quite bad!

Thanks to Owen Barrett
https://stacks.math.columbia.edu/tag/099S#comment-6318
https://stacks.math.columbia.edu/tag/099S#comment-6321

proetale.tex

@@ -3752,31 +3752,60 @@ \section{Comparison with the \'etale site}
 \label{lemma-limit-pullback}
 Let $X$ be a scheme. Let $Y = \lim Y_i$ be the limit of a directed inverse
 system of quasi-compact and quasi-separated objects of $X_\proetale$
-with affine transition morphisms. For any sheaf $\mathcal{F}$
-on $X_\etale$ we have
-$\epsilon^{-1}\mathcal{F}(Y) = \colim \mathcal{F}(Y_i)$.
+with affine transition morphisms. For any sheaf $\mathcal{F}$ on $X_\etale$
+we have
+$$
+\epsilon^{-1}\mathcal{F}(Y) = \colim \epsilon^{-1}\mathcal{F}(Y_i)
+$$
+Moreover, for any object $U$ of $X_\etale$ we have
+$\epsilon^{-1}\mathcal{F}(U) = \mathcal{F}(U)$.
 \end{lemma}
 
 \begin{proof}
-Let $\mathcal{F} = h_U$ be a representable sheaf on $X_\etale$
-with $U$ an object of $X_\etale$. In this case
-$\epsilon^{-1}h_U = h_{u(U)}$ where $u(U)$ is $U$ viewed as an object of
-$X_\proetale$ (Sites, Lemma \ref{sites-lemma-pullback-representable-sheaf}).
-Then
+Let us denote $u : X_\etale \to X_\proetale$ the inclusion functor.
+Let $U$ be an object of $X_\etale$. We have
+$\epsilon^{-1}h_U = h_{u(U)}$ by
+Sites, Lemma \ref{sites-lemma-pullback-representable-sheaf}.
+Thus we have
 \begin{align*}
 (\epsilon^{-1}h_U)(Y)
 & = h_{u(U)}(Y) \\
 & = \Mor_X(Y, U) \\
 & = \colim \Mor_X(Y_i, U) \\
-& = \colim h_U(Y_i)
+& = \colim h_{u(U)}(Y_i) \\
+& = \colim \epsilon^{-1}h_U(Y_i)
 \end{align*}
-Here the only nonformal equality is the $3$rd which holds
-by Limits, Proposition
+Here the $3$rd equality holds by Limits, Proposition
 \ref{limits-proposition-characterize-locally-finite-presentation}.
-Hence the lemma holds for every representable sheaf. Since every sheaf
-is a coequalizer of a map of coproducts of representable sheaves
-(Sites, Lemma \ref{sites-lemma-sheaf-coequalizer-representable})
-we obtain the result in general.
+Hence the lemma holds for every representable sheaf on $X_\etale$.
+Now, let $\mathcal{F}$ be an arbitrary sheaf of sets on $X_\etale$.
+By Sites, Lemma \ref{sites-lemma-colimit-representable} we can
+choose a diagram $\mathcal{J} \to X_\etale$, $j \mapsto U_j$
+such that $\mathcal{F} = \colim_{j \in \mathcal{J}} h_{U_j}$.
+We obtain
+\begin{align*}
+\epsilon^{-1}\mathcal{F}(Y)
+& =
+(\colim_j \epsilon^{-1}h_{U_j})(Y) \\
+& =
+\colim_j \epsilon^{-1}h_{U_j}(Y) \\
+& =
+\colim_j \colim_i \epsilon^{-1}h_{U_j}(Y_i) \\
+& =
+\colim_i \colim_j \epsilon^{-1}h_{U_j}(Y_i) \\
+& =
+\colim_i \epsilon^{-1}\mathcal{F}(Y_i)
+\end{align*}
+The first equality holds because $\epsilon$ is a left adjoint and hence
+commutes with colimits. The second equality holds by
+Sites, Lemma \ref{sites-lemma-directed-colimits-sections}
+and the fact that $Y$ is quasi-compact and quasi-separated
+(we omit the verification that this means the object $Y$ of the site
+$X_\proetale$ satisfies the assumptions of the fourth part of the cited lemma).
+The third equality was shown above. Then fourth equality because colimits
+commute with colimits. The fifth equality by
+Sites, Lemma \ref{sites-lemma-directed-colimits-sections}
+applied to $Y_i$. This finishes the proof.
 \end{proof}
 
 \begin{lemma}

sites.tex

@@ -2406,6 +2406,50 @@ \section{Representable sheaves}
 as above. See Lemma \ref{lemma-coequalizer-surjection}.
 \end{proof}
 
+\begin{lemma}
+\label{lemma-colimit-representable}
+Let $\mathcal{C}$ be a site. Let $\mathcal{F}$ be a sheaf of sets on
+$\mathcal{C}$. Then there exists a diagram $\mathcal{I} \to \mathcal{C}$,
+$i \mapsto U_i$ such that
+$$
+\mathcal{F} = \colim_{i \in \mathcal{I}} h_{U_i}^\#
+$$
+Moreover, if $E \subset \Ob(\mathcal{C})$ is a subset such that every
+object of $\mathcal{C}$ has a covering by elements of $E$, then we may
+assume $U_i$ is an element of $E$ for all $i \in \Ob(\mathcal{I})$.
+\end{lemma}
+
+\begin{proof}
+Let $\mathcal{I}$ be the category whose objects are pairs
+$(U, s)$ with $U \in \Ob(\mathcal{C})$ and $s \in \mathcal{F}(U)$
+and whose morphisms $(U, s) \to (U', s')$ are morphisms $f : U \to U'$
+in $\mathcal{C}$ with $f^*s' = s$. For each object $(U, s)$ of $\mathcal{I}$
+the element $s$ defines by the Yoneda lemma a map $s : h_U \to \mathcal{F}$
+of presheaves. Hence by the universal property of sheafification a map
+$h_U^\# \to \mathcal{F}$. These maps are immediately seen to be compatible
+with the morphisms in the category $\mathcal{I}$. Hence we obtain
+a map $\colim_{(U, s)} h_U \to \mathcal{F}$ of presheaves (where the
+colimit is taken in the category of presheaves) and a map
+$\colim_{(U, s)} (h_U)^\# \to \mathcal{F}$ of sheaves (where the
+colimit is taken in the category of sheaves).
+Since sheafification is the left adjoint to the inclusion functor
+$\Sh(\mathcal{C}) \to \textit{PSh}(\mathcal{C})$
+(Proposition \ref{proposition-sheafification-adjoint}) we have
+$\colim (h_U)^\# = (\colim h_U)^\#$ by
+Categories, Lemma \ref{categories-lemma-adjoint-exact}.
+Thus it suffices to show that $\colim_{(U, s)} h_U \to \mathcal{F}$
+is an isomorphism of presheaves. To see this we show that for every object
+$X$ of $\mathcal{C}$ the map $\colim_{(U, s)} h_U(X) \to \mathcal{F}(X)$
+is bijective. Namely, it has an inverse sending the element
+$t \in \mathcal{F}(X)$ to the element of the set $\colim_{(U, s)} h_U(X)$
+corresponding to $(X, t)$ and $\text{id}_X \in h_X(X)$.
+
+\medskip\noindent
+We omit the proof of the final statement.
+\end{proof}
+
+
+
 
 \section{Continuous functors}
 \label{section-continuous-functors}