Proper base change for ringed spaces $\newcommand{\Oo}{\mathcal{O}}$
Let $f:X\to Y$ be a proper map of topological spaces. Then we can consider the basechange along any continuous map $g:Y'\to Y$. Denote by $X'=X\times_Y Y'$ the base change and by $F:X'\to Y'$ and $G:X'\to X$ the natural morphisms.
Then it is well known than the natural morphism $g^{-1}f_*\Rightarrow F_*G^{-1}$ is an isomorphism.
Is there a similar statement for ringed spaces, i.e. when every space carries a fixed sheaf of rings $\Oo_X,\Oo_Y,\Oo_{Y'},\Oo_{X'}$ and all maps being maps of ringed spaces. We then define $g^*-=g^{-1}-\otimes_{g^{-1}\Oo_Y} \Oo_{Y'}$.
What can we say about $g^*f_*\Rightarrow F_*G^*$. Somehow using the projection formula we should be able to say something more than existance, i.e. give some sort of flatness criterion for when it is an isomorphism.
Any references are most welcome.
 A: The Stacks Project is a good reference for this, since it sets up a good deal of cohomology theory for general ringed topological spaces (or more generally, ringed topoi). See in particular Tag 09V4, which proves the proper base change formula for abelian sheaves, as you note above. (You're implicitly using the fact that cohomology/derived pushforward for an $\mathscr{O}_X$-module is the same as its cohomology when viewed as an abelian sheaf, which comes from the fact that injective $\mathscr{O}_X$-modules are flasque).
We'll need to assume something stronger than flatness of $\mathscr{O}_{Y'}$ over $g^{-1} \mathscr{O}_Y$, since unlike the case of schemes, we do not have the all-important fact that we can explicitly compute global sections of tensor products of quasicoherent sheaves on any affine open. Thus, we need something that lets us understand the functor $F_* ( - \otimes_{G^{-1} \mathscr{O}_X} \mathscr{O}_{X'})$.
Thus, we assume $\mathscr{O}_{Y'}$ is a finite locally free $g^{-1} \mathscr{O}_Y$-module.
Note that this implies the analogous fact for $\mathscr{O}_{X'}$.
So we're in the following situation. We have a sheaf of $\mathscr{O}_X$-modules $\mathscr{E}$, and we are asking for the following natural map $\Psi$ to be an isomorphism:
$\Psi \colon g^* R^i f_* \mathscr{E} = (g^{-1} R^i f_* \mathscr{E}) \otimes_{g^{-1} \mathscr{O}_Y} \mathscr{O}_{Y'} \xrightarrow{\sim} (R^i F_* G^{-1} \mathscr{E}) \otimes_{g^{-1} \mathscr{O}_Y} \mathscr{O}_{Y'} \xrightarrow{\psi} R^i F_*(G^{-1} \mathscr{E} \otimes_{h^{-1}\mathscr{O}_Y} F^{-1}\mathscr{O}_{Y'}) \xrightarrow{\sim} R^i F_* G^* \mathscr{E}$.
Here, we take $h \colon X' \rightarrow Y$ to be the composition $f \circ G = g \circ F$.
To see the final isomorphism, we have:
$G^* \mathscr{E} = G^{-1} \mathscr{E} \otimes_{G^{-1} \mathscr{O}_X} \mathscr{O}_{X'} = G^{-1} \mathscr{E} \otimes_{G^{-1} \mathscr{O}_X} (G^{-1} \mathscr{O}_X \otimes_{h^{-1} \mathscr{O}_Y} F^{-1} \mathscr{O}_{Y'}) = G^{-1} \mathscr{E} \otimes_{h^{-1} \mathscr{O}_{Y}} F^{-1} \mathscr{O}_{Y'}$
The map $\psi$ is the $\mathscr{O}_{Y'}$-linearization of the functor $R^i F_*$ applied to the natural $G^{-1} \mathscr{O}_X$-linear map $G^{-1} \mathscr{E} \rightarrow G^{-1} \mathscr{E} \otimes_{h^{-1} \mathscr{O}_Y} F^{-1} \mathscr{O}_{Y'}$.
Consider the map $\widetilde{F}$ of ringed spaces $(X', G^{-1} \mathscr{O}_X) \rightarrow (Y', g^{-1} \mathscr{O}_Y)$. We may identify $R^i F_*$ with $R^i \widetilde{F}_*$, as these functors only depend on the underlying abelian sheaves. Furthermore, we may make the following identification:
$\widetilde{F}^* \mathscr{O}_{Y'} = G^{-1}\mathscr{O}_X  \otimes_{h^{-1} \mathscr{O}_Y} F^{-1} \mathscr{O}_{Y'} $
This comes from the fact that $F^{-1}$ and $\widetilde{F}^{-1}$ are naturally identified (as they may be computed at the level of abelian sheaves), and the fact that $F^{-1} g^{-1} \mathscr{O}_Y = h^{-1} \mathscr{O}_Y$.
Now, by Tag 01E6, we have the projection formula for the map $\widetilde{F}$ of ringed spaces, assuming that $\mathscr{O}_{Y'}$ is locally free over $g^{-1} \mathscr{O}_Y$:
$R \widetilde{F}_* G^{-1} \mathscr{E} \otimes_{g^{-1} \mathscr{O}_Y} \mathscr{O}_{Y'} \xrightarrow{\sim} R \widetilde{F}_*(G^{-1} \mathscr{E} \otimes_{G^{-1} \mathscr{O}_X} \widetilde{F}^* \mathscr{O}_{Y'}) = R F_* (G^{-1} \mathscr{E} \otimes_{h^{-1} \mathscr{O}_Y} F^{-1} \mathscr{O}_{Y'})$
Working through the definition of the map in the projection formula shows that this map is none other than the map $\psi$ above. Thus, $\psi$ is an isomorphism, and therefore so is $\Psi$.
Note that something a little bit strange is going on here: to apply the topological proper base change theorem, we need to take $X'$ to be the topological fiber product $X \times_Y Y'$. This is the underlying set of the fiber product $(X, \mathscr{O}_X) \times_{(Y, \mathscr{O}_Y)} (Y', \mathscr{O}_{Y'})$ in the category of ringed spaces, where we take the structure sheaf on $X \times_Y Y'$ to be $G^{-1} \mathscr{O}_X \otimes_{(F \circ G)^{-1} \mathscr{O}_Y} F^{-1} \mathscr{O}_{Y'}$. However, this is usually not the right object to consider in algebraic geometry: if $(X, \mathscr{O}_X)$ and $(Y, \mathscr{O}_Y)$ are schemes, this construction is not the fiber product of $X$ and $Y$ as schemes; the problem is that this ringed space fiber product will not be a locally ringed space in general. (For example, take $Y = \mathrm{Spec}(k)$ and $X = Y' = \mathrm{Spec}(k')$ for some finite Galois extension $k'/k$. Then as the underlying topological spaces of $X, Y, Y'$ are all points, the construction above gives a point with structure sheaf $k' \otimes_k k' = \prod_{\sigma \in \mathrm{Gal}(k'/k)} k'$, which is certainly not a local ring).
