Simplification and complication

Thanks to Pavel Čoupek
https://stacks.math.columbia.edu/tag/07HE#comment-4286

crystalline.tex

@@ -380,19 +380,8 @@ \section{Divided power envelope}
 \end{lemma}
 
 \begin{proof}
-Set $D = D_B(J)$ and denote $\bar J \subset D$ its divided power ideal
-with divided power structure $\bar\gamma$. The universal property of
-$D$ produces a homomorphism of divided power rings $D \to D_{B'}(J')$,
-whence a map as in the lemma. It suffices to show that
-there exist divided powers on the image of
-$D \otimes_B I' + \bar J \otimes_B B' \to  D \otimes_B B'$
-compatible with $\bar \gamma$ and $\gamma'$ since then
-the universal property of $D_{B'}(J')$ will produce a map
-$D_{B'}(J') \to D \otimes_B B'$ inverse to the one in the lemma.
-
-\medskip\noindent
-Choose elements $f_t \in J$ which generate $J/I$. Set
-$\mathcal{R} = \{(r_0, r_t) \in I \oplus \bigoplus\nolimits_{t \in T} B
+Set $D = D_{B, \gamma}(J)$. Choose elements $f_t \in J$ which generate $J/I$.
+Set $\mathcal{R} = \{(r_0, r_t) \in I \oplus \bigoplus\nolimits_{t \in T} B
 \mid \sum r_t f_t = r_0 \text{ in }B\}$ as in the proof of
 Lemma \ref{lemma-describe-divided-power-envelope}. This lemma shows that
 $$
@@ -428,21 +417,40 @@ \section{Divided power envelope}
 $r_{jt} \in B$ and $c_j \in B'$, $j = 1, \ldots, m$ such
 that
 $$
-r_{j0} = \sum r_{jt} f_t  \in I \text{ for } j = 1, \ldots, m,
-\quad\text{and}\quad
-r'_t = \sum c_j r_{jt}.
+r_{j0} = \sum\nolimits_t r_{jt} f_t  \in I \text{ for } j = 1, \ldots, m
+$$
+and
 $$
-Note that this also implies that $r'_0 = \sum c_j r_{j0}$.
+i'_t  = r'_t - \sum\nolimits_j c_j r_{jt} \in I' \text{ for all }t
+$$
+Note that this also implies that
+$r'_0 = \sum_t i'_t f_t + \sum_j c_j r_{j0}$.
 Then we have
 \begin{align*}
-\delta'_n(\sum r'_t x_t  - r'_0)
+\delta'_n(\sum\nolimits_t r'_t x_t  - r'_0)
 & =
-\delta'_n(\sum c_j (\sum r_{jt} x_t  - r_{j0})) \\
+\delta'_n(
+\sum\nolimits_t i'_t x_t +
+\sum\nolimits_{t, j} c_j r_{jt} x_t -
+\sum\nolimits_t i'_t f_t -
+\sum\nolimits_j c_j r_{j0}) \\
 & =
+\delta'_n(
+\sum\nolimits_t i'_t(x_t - f_t) +
+\sum\nolimits_j c_j (\sum\nolimits_t r_{jt} x_t  - r_{j0}))
+\end{align*}
+Since $\delta_n(a + b) = \sum_{m = 0, \ldots, n} \delta_m(a) \delta_{n - m}(b)$
+and since $\delta_m(\sum i'_t(x_t - f_t))$ is in the ideal
+generated by $x_t - f_t \in K'$ for $m > 0$, it suffices to prove that
+$\delta_n(\sum c_j (\sum r_{jt} x_t  - r_{j0}))$ is in $K'$.
+For this we use
+$$
+\delta_n(\sum\nolimits_j c_j (\sum\nolimits_t r_{jt} x_t  - r_{j0}))
+=
 \sum c_1^{n_1} \ldots c_m^{n_m}
 \delta_{n_1}(\sum r_{1t} x_t  - r_{10}) \ldots
 \delta_{n_m}(\sum r_{mt} x_t  - r_{m0})
-\end{align*}
+$$
 where the sum is over $n_1 + \ldots + n_m = n$. This proves what we want.
 \end{proof}