Kunneth for etale cohomology

This is obviously insane, but somehow I started writing it this way and
I couldn't get myself to stop. If you have a better way of writing the
proofs in this section, by all means send me suggestions.

etale-cohomology.tex

@@ -17351,6 +17351,39 @@ \section{K\"unneth in \'etale cohomology}
 (akin to smooth base change).
 Finally we use this to get a more general K\"unneth formula.
 
+\begin{remark}
+\label{remark-define-kunneth-map}
+Consider a cartesian diagram in the category of schemes:
+$$
+\xymatrix{
+X \times_S Y \ar[d]_p \ar[r]_q \ar[rd]_c & Y \ar[d]^g \\
+X \ar[r]^f & S
+}
+$$
+Let $\Lambda$ be a ring and let $E \in D(X_\etale, \Lambda)$
+and $K \in D(Y_\etale, \Lambda)$. Then there is a canonical map
+$$
+Rf_*E \otimes_\Lambda^\mathbf{L} Rg_*K
+\longrightarrow
+Rc_*(p^{-1}E \otimes_\Lambda^\mathbf{L} q^{-1}K)
+$$
+For example we can define this using the canonical maps
+$Rf_*E \to Rc_*p^{-1}E$ and $Rg_*K \to Rc_*q^{-1}K$ and
+the relative cup product defined in Cohomology on Sites,
+Remark \ref{sites-cohomology-remark-cup-product}.
+Or you can use the adjoint to the map
+$$
+c^{-1}(Rf_*E \otimes_\Lambda^\mathbf{L} Rg_*K)
+=
+p^{-1}f^{-1}Rf_*E \otimes_\Lambda^\mathbf{L} q^{-1} g^{-1}Rg_*K
+\to
+p^{-1}E \otimes_\Lambda^\mathbf{L} q^{-1}K
+$$
+which uses the adjunction maps $f^{-1}Rf_*E \to E$ and
+$g^{-1}Rg_*K \to K$.
+\end{remark}
+
+
 \begin{lemma}
 \label{lemma-kunneth-one-proper}
 Let $k$ be a separably closed field. Let $X$ be a proper scheme over $k$.
@@ -17763,7 +17796,7 @@ \section{K\"unneth in \'etale cohomology}
 $K$-subalgebras $B_i$. Let $J$ be the set of pairs $(i, g)$ where
 $i \in I$ and $g \in B_i$ nonzero with ordering
 $(i', g') \geq (i, g)$ if and only if $i' \geq i$ and
-$g$ maps to an invertible element of $B_{i'}$.
+$g$ maps to an invertible element of $(B_{i'})_{g'}$.
 Then $L = \colim_{(i, g) \in J} (B_i)_g$.
 For $j = (i, g) \in J$ set $S_j = \Spec(B_i)$
 and $U_j = \Spec((B_i)_g)$.
@@ -17789,6 +17822,28 @@ \section{K\"unneth in \'etale cohomology}
 proved in Lemma \ref{lemma-kunneth-localize-on-X}.
 \end{proof}
 
+\begin{lemma}
+\label{lemma-punctual-base-change-upgrade}
+Let $K$ be a field. Let $X$ be a scheme over $K$.
+For any commutative diagram
+$$
+\xymatrix{
+X \ar[d] & X' \ar[l] \ar[d]_{f'} & Y \ar[l]^h \ar[d]^e \\
+\Spec(K) & S' \ar[l] & T \ar[l]_g
+}
+$$
+$X' = X \times_{\Spec(K)} S'$ and $Y = X' \times_{S'} T$ and
+$g$ quasi-compact and quasi-separated, and every abelian sheaves
+$\mathcal{G}$ on $X_\etale$ and $\mathcal{F}$ on $T_\etale$
+whose stalks are torsion of orders invertible in $K$ the base change map
+$$
+\mathcal{G} \otimes (f')^{-1}Rg_*\mathcal{F}
+\longrightarrow
+Rh_*(\mathcal{G} \otimes e^{-1}\mathcal{F})
+$$
+is an isomorphism.
+\end{lemma}
+