finished i.8

trees/sga1/sga1-i/sga1-i.8.tree

@@ -68,6 +68,41 @@
   }
 
   \proof{
-    By
+    By \ref{sga1-i.5.5}, it remains only to show that every étale #{S_0}-scheme #{X_0} is isomorphic to an #{S_0}-scheme #{X\times_S S_0}, where #{X} is an étale #{S}-scheme.
+    The underlying topological space of #{X} must necessarily be identical to the one of #{X_0}, and with #{X_0} being identified with a closed sub-prescheme of #{X}.
+    The problem is thus equivalent to the following:
+    find, on the underlying topological space #{|X_0|} of #{X_0}, a sheaf of algebras #{\sh{O}_X} over #{f_0^*(\sh{O}_S)} (where #{f_0} is the projection #{X_0\to S_0}, thought of here as a continuous map of the underlying spaces) that makes #{|X_0|} an étale #{S}-prescheme #{X}, as well as an algebra homomorphism #{\sh{O}_X\to\sh{O}_{X_0}} that is compatible with the homomorphism #{f_0^*(\sh{O}_S)\to f_0^*(\sh{O}_{S_0})} on the sheaves of scalars, and that induces an isomorphism #{\sh{O}_X\otimes_{f_0^*(\sh{O}_S)*}f_0^*(\sh{O}_{S_0})\xrightarrow{\sim}\sh{O}_{X_0}}.
+    (Then #{X} will be an étale #{S}-prescheme that is reduced along #{X_0}, and thus separated over #{S}, since #{X_0} is separated over #{S_0}, and #{X} satisfies all the desired properties).
+
+    If #{(U_i)} is an open cover of #{X_0}, and if we find a solution to the problem on each of the #{U_i}, then it follows from the uniqueness theorem \ref{sga1-i.5.5} that these solutions glue (i.e. the sheaves of algebras that they define, endowed with their augmentation homomorphisms, glue), and we claim that the ringed space thus constructed over #{S} is an étale #{S}-prescheme #{X} endowed with an isomorphism #{X\times_S S_0\xleftarrow{\sim}X_0}.
+    It thus suffices to find a solution locally, which we know is possible by \ref{sga1-i.8.1}.
+  }
+}
+
+\subtree[sga1-i.8.4]{
+  \taxon{corollary}
+  \number{I.8.4}
+
+  \p{
+    Let #{S} be a locally Noetherian formal prescheme, endowed with an ideal of definition #{\sh{J}}, and let #{S_0=(|S|,\sh{O}_S/\sh{J})} be the corresponding ordinary prescheme.
+    Then the functor #{\mathfrak{X}\mapsto\mathfrak{X}\times_S S_0} from the category of étale covers of #{S} to the category of étale covers of #{S_0} is an equivalence of categories.
+  }
+
+  \proof{
+    \p{
+      Of course, we define an étale cover of a \em{formal} prescheme #{S} to be a cover of #{S} (i.e a formal prescheme over #{S} defined by a coherent sheaf of algebras #{\sh{B}}) such that #{\sh{B}} is \em{locally free}, and such that the residue fibres #{\sh{B}_s\otimes_{\sh{O}_s}k(s)} of #{\sh{B}} are \em{separable} algebras over #{k(s)}.
+      If we denote by #{S_n} the ordinary prescheme #{(|S|,\sh{O}_S/\sh{J}^{n+1})}, then the data of a coherent sheaf of algebras #{\sh{B}} on #{S} is equivalent to the data of a sequence of coherent sheaves of algebras #{\sh{B}_n} on the #{S_n}, endowed with a transitive system of homomorphisms #{\sh{B}_m\to\sh{B}_n} (for #{m\geq n}) defining the isomorphisms #{\sh{B}_m\otimes_{\sh{O}_{S_m}}\sh{O}_{S_n}\xrightarrow{\sim}\sh{B}_n}.
+      It is immediate that #{\sh{B}} is locally free if and only if the #{\sh{B}_n} are locally free over the #{S_n}, and that the separability condition is satisfied if and only if it is satisfied for #{\sh{B}_0}, or for all the #{\sh{B}_n}.
+      Thus #{\sh{B}} is étale over #{S} if and only if the #{\sh{B}_n} are étale over the #{S_n}.
+      Taking this into account, \ref{sga1-i.8.4} follows immediately from \ref{sga1-i.8.3}.
+    }
   }
-}
+}
+
+\subtree{
+  \taxon{remark}
+
+  \p{
+    It was not necessary to restrict ourselves to the case of \em{covers} in \ref{sga1-i.8.4}, but this is the only case that we will use for the moment.
+  }
+}