Improve the proof of a lemma

Thanks to Keenan Kidwell
http://stacks.math.columbia.edu/tag/04KP#comment-749
http://stacks.math.columbia.edu/tag/037V#comment-748

algebra.tex

@@ -9941,29 +9941,26 @@ \section{Geometrically irreducible algebras}
 Note that as $k \subset \overline{k}$ is integral all the prime ideals
 of $\overline{k} \otimes_k K$ and $\overline{k} \otimes_k k'$ are maximal, see
 Lemma \ref{lemma-integral-no-inclusion}.
-In particular the residue field of any prime ideal of
-$\overline{k} \otimes_k k'$ is isomorphic to $\overline{k}$.
-Hence the prime ideals of $\overline{k} \otimes_k k'$ correspond one to
-one to elements of $\Hom_k(k', \overline{k})$ with
-$\sigma \in \Hom_k(k', \overline{k})$ corresponding to the
-kernel $\mathfrak p_\sigma$ of
+By Lemma \ref{lemma-geometrically-irreducible-any-base-change}
+the map
+$$
+\Spec(\overline{k} \otimes_k K) \to \Spec(\overline{k} \otimes_k k')
+$$
+is bijective because (1) all primes are mimimal primes, (1)
+$\overline{k} \otimes_k K = (\overline{k} \otimes_k k') \otimes_{k'} K$,
+and (3) $K$ is geometrically irreducible over $k'$.
+Hence it suffices to prove the lemma for the action of
+$\text{Gal}(\overline{k}/k)$ on the primes of $\overline{k} \otimes_k k'$.
+
+\medskip\noindent
+As every prime of $\overline{k} \otimes_k k'$ is maximal, the residue fields
+are isomorphic to $\overline{k}$. Hence the prime ideals of
+$\overline{k} \otimes_k k'$ correspond one to one to elements of
+$\Hom_k(k', \overline{k})$ with $\sigma \in \Hom_k(k', \overline{k})$
+corresponding to the kernel $\mathfrak p_\sigma$ of
 $1 \otimes \sigma : \overline{k} \otimes_k k' \to \overline{k}$.
 In particular $\text{Gal}(\overline{k}/k)$ acts transitively on
-this set.
-Finally, since $K$ is geometrically irreducible over $k'$ we
-see that there is a unique prime of $\overline{k} \otimes_k K$
-lying over each $\mathfrak p_\sigma$ since the set of these primes
-is the set of primes in the ring
-$$
-(\overline{k} \otimes_k K)
-\otimes_{(\overline{k} \otimes_k k'), 1 \otimes \sigma}
-\kappa(\mathfrak p_\sigma)
-=
-\overline{k} \otimes_{\overline{k}} (K \otimes_{k'} \overline{k})
-=
-K \otimes_{k', \sigma} \overline{k}
-$$
-Thus the lemma holds.
+this set as desired.
 \end{proof}
 
 
@@ -10077,7 +10074,7 @@ \section{Geometrically connected algebras}
 $k$-subalgebra.
 \item If all finitely generated $k$-subalgebras of $S$ are
 geometrically connected, then $S$ is geometrically connected.
-\item A directed colimit of geometrically irreducible $k$-algebras
+\item A directed colimit of geometrically connected $k$-algebras
 is geometrically connected.
 \end{enumerate}
 \end{lemma}