How to show analytification functor commutes with forgetful functor?

Let $$k$$ be a field complete with respect to a non-trivial non-archimedean absolute value (so that rigid $$k$$-space makes sense). Denote $$K$$ a finite field extension of $$k$$.

Denote $$X\rightsquigarrow X^{\mathrm{an}/k}$$ the analytification functor from the category of locally of finite type $$k$$-schemes to the category of rigid $$k$$-spaces. Similarly there is an analytification functor $$X\rightsquigarrow X^{\mathrm{an}/K}$$ over $$K$$.

There is a well-defind forgetful functor $$S:X\rightsquigarrow X$$ from $$K$$-schemes to $$k$$-schemes ($$S$$ represents schemes) and a forgetful functor $$R:Y\rightsquigarrow Y$$ from rigid $$K$$-spaces to rigid $$k$$-spaces ($$R$$ represents rigid).

Let $$X$$ be a locally of finite type $$K$$-scheme. I believe that $$S(X)^{\mathrm{an}/k}\cong R(X^{\mathrm{an}/K})$$ as rigid $$k$$-spaces. The universal property induces a canonical map $$R(X^{\mathrm{an}/K})\to S(X)^{\mathrm{an}/k}$$ but I cannot show it is an isomorphism. A proof or reference would be nice.

p.s. the idea comes from proving absolute/relative Frobenius morphism commutes with analytification, but I first need to make sure the maps have the same source.

Also in ME, but I just got advised not to post the same problem on both MS and ME. So I deleted the one on ME, and will possibly undelete it after a week or two.

I believe I got an answer. Denote $$X^{\mathrm{an}/K},X^{\mathrm{an}/k}$$ the analytifications of $$X$$ over $$K$$ and $$k$$ respectively. Denote $$K$$-maps (resp. $$k$$-maps) the maps of locally $$G$$-ringed $$K$$-spaces (resp. $$k$$-spaces).

Lemma: Let $$X$$ be a locally of finite type $$K$$-schemes. Then $$X^{\mathrm{an}/K}\cong X^{\mathrm{an}/k}$$ both as rigid $$k$$-spaces and rigid $$K$$-spaces.

Plan: Assume $$X$$ is affine. Find maps $$X^{\mathrm{an}/K}\to X^{\mathrm{an}/k}$$ and $$X^{\mathrm{an}/k}\to X^{\mathrm{an}/K}$$ and prove both of them are both $$K$$-maps and $$k$$-maps. Then the result follows from universal properties of $$X^{\mathrm{an}/k}$$ and $$X^{\mathrm{an}/K}$$. Then show it generalizes to the general case.

Proof: Assume $$X$$ is affine. Clearly the canonical $$K$$-map $$X^{\mathrm{an}/K}\to X$$ is also $$k$$-map, hence uniquely factors through the canonical $$k$$-map $$X^{\mathrm{an}/k}\to X$$. So we have a $$k$$-map $$X^{\mathrm{an}/K}\to X^{\mathrm{an}/k}$$.

To find a $$K$$-map from $$X^{\mathrm{an}/k}$$ to $$X^{\mathrm{an}/K}$$, it suffices to show that the canonical $$k$$-map $$X^{\mathrm{an}/k}\to X$$ is actually a $$K$$-map.

We know $$X$$ is affine, say $$X\cong\mathop{\mathrm{Spec}}\frac{k[x_1,...,x_n]}{I}$$. Pick $$c\in k$$ s.t. $$|c|>1$$. Denote $$T_n^{(i)}=k\langle c^{-i}x_1,...,c^{-i}x_n\rangle$$. We know $$X^{\mathrm{an}/k}=\bigcup_{i\geq0}\mathop{\mathrm{Sp}}\frac{T_n^{(i)}}{(I)}$$, and $$X^{\mathrm{an}/k}\to X$$ is determined by the compatible maps $$\frac{k[x_1,...,x_n]}{I}\to \frac{T_n^{(i)}}{(I)}$$. Let $$\frac{T_n^{(i)}}{(I)}$$ equips with a $$K$$-algebra structure via $$K\to \frac{k[x_1,...,x_n]}{I}\to \frac{T_n^{(i)}}{(I)}$$ (note that any ring map from a field to a ring is injective). Then $$\frac{k[x_1,...,x_n]}{I}\to \frac{T_n^{(i)}}{(I)}$$ is a map of $$K$$-algebras. So $$X^{\mathrm{an}/k}$$ is a rigid $$K$$-space and $$X^{\mathrm{an}/k}\to X$$ is actually a $$K$$-map and it induces a $$K$$-map $$X^{\mathrm{an}/k}\to X^{\mathrm{an}/K}$$ which is also a $$k$$-map.

By universal property of $$X^{\mathrm{an}/k}$$, we have an equality of $$k$$-maps $$(X^{\mathrm{an}/k}\to X^{\mathrm{an}/K}\to X^{\mathrm{an}/k})=(X^{\mathrm{an}/k}\stackrel{\mathrm{id}}{\to} X^{\mathrm{an}/k})$$ Next we show that the $$k$$-map $$X^{\mathrm{an}/K}\to X^{\mathrm{an}/k}$$ is also a $$K$$-map so we can prove that the $$K$$-map $$X^{\mathrm{an}/K}\to X^{\mathrm{an}/k}\to X^{\mathrm{an}/K}$$ is the identity map hence an identity $$k$$-map, it follows that $$X^{\mathrm{an}/k}\cong X^{\mathrm{an}/K}$$ both as rigid $$K$$-spaces and rigid $$k$$-spaces.

Just like $$X^{\mathrm{an}/k}=\bigcup_{i\geq0}\mathop{\mathrm{Sp}}\frac{T_n^{(i)}}{(I)}$$, we have $$X^{\mathrm{an}/K}=\bigcup_{j\geq0}\mathop{\mathrm{Sp}}A_j$$ for some $$K$$-algebras $$A_j$$. It suffices to show that $$\mathop{\mathrm{Sp}}A_j\to X^{\mathrm{an}/k}$$ is a $$K$$-map for all $$j$$. Fix $$j\geq 0$$, then there exists $$\alpha(j)\geq 0$$ s.t. $$\mathop{\mathrm{Sp}}A_j\to X^{\mathrm{an}/k}\to X$$ induces $$\frac{k[x_1,...,x_n]}{I}\to \frac{T_n^{(\alpha(j))}}{(I)}\to A_j$$ where the composition is a map of $$K$$-algebras, hence all intermediate maps are of $$K$$-algebras, and $$X^{\mathrm{an}/K}\to X^{\mathrm{an}/k}$$ is a $$K$$-map and we finished the affine case.

The patching part can be annoying. For a general scheme $$X$$, pick an open affine cover $$\{X_i\}_{i\in I}$$. For each pair $$X_{ij}=X_i \cap X_j$$, we know it can be covered by simultaneous distinguished open affines $$\{D_{ijk}\}_{k\in S_{ij}}$$. We know that $$X^{\mathrm{an}/k}$$ is obtained by gluing $$\{X_i^{\mathrm{an}/k}\}_{i\in I}$$ and $$X^{\mathrm{an}/K}$$ is obtained by gluing $$\{X_i^{\mathrm{an}/K}\}_{i\in I}$$. In particular, the gluing data of $$X^{\mathrm{an}/k}$$ over $$k$$ also has a structure of gluing data over $$K$$ (i.e. the spaces and the maps are over $$K$$, if we want to be precise, we will need to use $$D_{ijk}$$), so $$X^{\mathrm{an}/k}$$ is a rigid $$K$$-space. With this we can show $$(X^{\mathrm{an}/k}\to X^{\mathrm{an}/K}\to X^{\mathrm{an}/k})=(X^{\mathrm{an}/k}\stackrel{\mathrm{id}}{\to} X^{\mathrm{an}/k})$$

Now we need the following pasting lemmas for $$K$$-maps.

Lemma: Let $$X$$ and $$Y$$ be rigid $$K$$-spaces admitting admissible coverings $$\{X_i\}_{i\in I}$$ and $$\{Y_i\}_{i\in I}$$, respectively. Let $$\psi_i :X_i \to Y_i,i\in I$$ be $$K$$-maps such that for all $$i,j\in I$$, we have $$\psi_i|_{X_i\cap X_j}=\psi_j|_{X_i\cap X_j}:X_i\cap X_j \to Y_i \cap Y_j$$. Then there exists a unique $$K$$-map $$\psi:X\to Y$$ extending all $$\psi_i,i\in I$$. For proof see [Non-Archimedean analysis] by Bosch, 9.3.3 Prop 1.

The $$k$$-map $$\psi:X^{\mathrm{an}/K}\to X^{\mathrm{an}/k}$$ descends to a gluing data of $$k$$-maps: $$\psi_i:X_i^{\mathrm{an}/K}\to X_i^{\mathrm{an}/k},\psi_{ij}:X_{ij}^{\mathrm{an}/K}\to X_{ij}^{\mathrm{an}/k}$$ In particular, $$\psi_i$$ is already a $$K$$-map by the proof for affine case. Thus $$\psi_{ij}$$ is a $$K$$-map as a restriction map. So we have a gluing data of $$K$$-maps, then we obtain a $$K$$-map $$\psi_K:X^{\mathrm{an}/K}\to X^{\mathrm{an}/k}$$ s.t. $$\psi_K=\psi$$ as $$k$$-maps.

The rest of the proof is the same as the affine case, the result follows from the universal properties.$$\square$$

Bosch, S.; Güntzer, Ulrich; Remmert, Reinhold, Non-Archimedean analysis. A systematic approach to rigid analytic geometry, Grundlehren der Mathematischen Wissenschaften, 261. Berlin etc.: Springer Verlag. XII, 436 p. DM 168.00 (1984). ZBL0539.14017.