starting i.8

trees/sga1/sga1-i/sga1-i.7.tree

@@ -235,9 +235,9 @@
   \taxon{Remark}
 
   \p{
-    We must be able to state \ref{sga1-i.7.6} for a ring $\sh{O}$ that is only semi-local, so that we also cover \ref{sga1-i.7.5}:
-    we make the hypothesis that $\sh{O}/\mathfrak{m}\sh{O}$ is a \em{monogenous} $k$-algebra;
-    we can thus find some $u\in B$ whose image in $B/\mathfrak{m}B$ is a generator, and belongs to every maximal ideal of $B$ that doesn't come from $\sh{O}$.
+    We must be able to state \ref{sga1-i.7.6} for a ring #{\sh{O}} that is only semi-local, so that we also cover \ref{sga1-i.7.5}:
+    we make the hypothesis that #{\sh{O}/\mathfrak{m}\sh{O}} is a \em{monogenous} #{k}-algebra;
+    we can thus find some #{u\in B} whose image in #{B/\mathfrak{m}B} is a generator, and belongs to every maximal ideal of #{B} that doesn't come from #{\sh{O}}.
     Both \ref{sga1-i.7.9} and \ref{sga1-i.7.10} should be able to be adapted without difficulty.
     More generally, ...
   }

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

@@ -0,0 +1,73 @@
+\title{Infinitesimal lifting of étale schemes. Applications to formal schemes}
+\taxon{section}
+\number{I.8}
+\parent{sga1-i}
+
+\import{sga1-macros}
+\put\transclude/numbered{false}
+
+\subtree[sga1-i.8.1]{
+  \taxon{proposition}
+  \number{I.8.1}
+
+  \p{
+    Let #{Y} be a prescheme, #{Y_0} a sub-prescheme, #{X_0} an étale #{Y_0}-scheme, and #{x} a point of #{X_0}.
+    Then there exists an étale #{Y}-scheme #{X}, a neighbourhood #{U_0} of #{x} in #{X_0}, and a #{Y_0}-isomorphism #{U_0\xrightarrow{\sim}X\times_Y Y_0}.
+  }
+
+  \proof{
+    \p{
+      Let #{y} be the projection of #{x} in #{Y_0};
+      applying \ref{sga1-i.7.6} to the étale local homomorphism #{A_0\to B_0} of local rings of #{y} and #{x} in #{Y_0} and #{X_0}, we obtain an isomorphism
+      ##{
+        \begin{aligned}
+          B_0 &= (C_0)_{\mathfrak{n}_0}
+        \\C_0 &= A_0[t]/F_0A_0[t]
+        \end{aligned}
+      }
+      where #{F_0} is a monic polynomial, and #{\mathfrak{n}_0} is a maximal ideal of #{C_0} not containing the class of #{F'_0(t)} in #{C_0}.
+      Let #{A} be the local ring of #{y} in #{Y}, let #{F} be a monic polynomial in #{A[t]} that gives #{F_0} under the surjective homomorphism #{A\to A_0} (we lift the coefficients of #{F_0}), and let #{C=A[t]/FA[t]}, with #{\mathfrak{n}} the maximal ideal of #{C} given by the inverse image of #{\mathfrak{n}_0} under the natural epimorphism #{C\to C\otimes_A A_0=C_0}.
+      Let
+      ##{
+        B = C_\mathfrak{n}.
+      }
+      It is immediate, by construction and by \ref{sga1-i.7.1}, that #{B} is étale over #{A}, and that we have an isomorphism #{B\otimes_A A_0=A_0}.
+    }
+
+    \p{
+      We know that there exists a #{Y}-scheme #{X} of finite type, along with a point #{z} of #{X} over #{y} such that #{\sh{O}_z} is #{A}-isomorphic to #{C};
+      since the latter is étale over #{A=\sh{O}_y}, we can (by taking #{X} to be small enough) assume that #{X} is étale over #{Y}.
+      Let #{X'_0=X\times_Y Y_0}.
+      Then the local ring of #{z} in #{X'_0} can be identified with #{\sh{O}_z\otimes_A A_0=B\otimes_A A_0}, and is thus isomorphic to #{B_0}.
+      This isomorphism is defined by an isomorphism from a neighbourhood #{U_0} of #{x} in #{X} to a neighbourhood of #{z} in #{X'_0}, and we can assume this to be identical to #{X'_0} by taking #{X} to be small enough.
+    }
+  }
+}
+
+\subtree[sga1-i.8.2]{
+  \taxon{corollary}
+  \number{I.8.2}
+
+  \p{
+    The analogous claim holds for étale \em{covers}, if we suppose the residue field #{k(y)} to be infinite.
+  }
+
+  \proof{
+    \p{
+      The proof is the same, just replacing \ref{sga1-i.7.5} by \ref{sga1-i.7.6}.
+    }
+  }
+}
+
+\subtree[sga1-i.8.3]{
+  \taxon{theorem}
+  \number{I.8.3}
+
+  \p{
+    The functor described in \ref{sga1-i.5.5} is an \em{equivalence} of \em{categories}.
+  }
+
+  \proof{
+    By
+  }
+}

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

@@ -16,3 +16,4 @@
 \transclude{sga1-i.5}
 \transclude{sga1-i.6}
 \transclude{sga1-i.7}
+\transclude{sga1-i.8}