diffgeo: fix proof

Author: felixwellen

diffgeo/etale.tex

@@ -150,15 +150,11 @@ \subsection{Examples}
 \end{proposition}
 
 \begin{proof}
-  We have to extend maps $f:\Spec (A/(a))\to \Bool$, with $a^2=0$.
-  Since $\Bool\subseteq R$, the map $f$ yields an element $f:A/(a)$
-  and we have a lift $\tilde{f}:A$ with $f=\tilde{f}+ab$.
-  By \cref{nilpotent-ideal-not-not-dense},
-  we have for any $x:\Spec A$, that $\neg\neg(\tilde{f}(x)=0)$ or $\neg\neg(\tilde{f}(x)=1)$.
-
-  By Z-choice or computation, we find a $n:\N$,
-  such that $\tilde{f}^n(x)=0$ or $\neg\neg(\tilde{f}^n(x)=1)$.
-  With the map $1-\_:R\to R$, we can achieve the same for $1$.
+  We have to extend maps $e:\Spec (R/(a))\to \Bool$, with $a^2=0$.
+  Since $\Bool\subseteq R$, the map $e$ yields an idempotent element $f:R/(a)$.
+  There is a preimage $r:R$ and $b:R$ such that $r^2=r+ab$.
+  But then $(r^2-ab)$ is an idempotent element of $R$ such that $r+(a)=f$
+  and any idempotent in $R$ is $0$ or $1$ which gives an extension of the original map $e$.
 \end{proof}
 
 \begin{proposition}\label{finite-are-etale}