Reference request: Gruson's theorem on the tensor product of Banach spaces over a non-Archimedean field I am looking for a reference for theorem 3.21 of these notes: https://web.math.princeton.edu/~takumim/Berkovich.pdf
The theorem states that if $k$ is a non-Archimedean field and $X$ and $Y$ are $k$-Banach algebras then the canonical map $X\otimes_k Y \rightarrow X\hat{\otimes}_k Y$ is injective. That is the seminorm on the tensor product is in fact a norm. Said seminorm is defined on page 12 of the above notes.
This theorem is originally part 4 part of theorem 1 in section 3 of: http://www.numdam.org/item/10.24033/bsmf.1635.pdf
I'm asking for another reference because I would like a published reference which proves said theorem in the case when $k$ is trivially valued, and I believe the original paper takes the field to be nontrivially valued. I would also still be interested if the theorem isn't generally true but holds when the spaces $X$ and $Y$ are of countable type, or are even complete $k$-algebras with multiplicative norms. I'm primarily interested in looking at the tensor products of residue fields of Berkovich analytifications of schemes.
Thanks in advance.
 A: I do not think I know of any reference, but let me sketch a proof that one can reduce to the non-trivially valued case.
Let $r>0$ and consider the valued field $k_r$ defined as $k((t))$ endowed with the absolute value that is trivial on $k$ and satisfies $|t|=r$. The point is that for any $k$-Banach space $X$, the space $X\hat{\otimes}_k k_r$ is a $k_r$-Banach space with a very explicit description: the space of series $f = \sum_{i\in \mathbf Z} x_i T^i$ such that $\|x_i\| r^i$ tends to 0 when $i$ goes to $\pm \infty$. Moreover, the tensor norm of $f$ is also explicit: $\|f\| = \sup_{i\in\mathbf Z} (\|x_i\| r^i)$. In particular $X \to X\hat{\otimes}_k k_r$ is an isometry (and so is $X \to X\otimes_k k_r$). This is a standard technique in Berkovich theory. See for instance Berkovich's book "Spectral Theory..." around Proposition 2.1.2.
Using this construction in your situation, you may embed $X \otimes_k Y$ isometrically into $(X \otimes_k Y) \otimes_k k_r = (X \otimes_k k_r) \otimes_{k_r} (Y \otimes_k k_r)$. Moreover, $X \otimes_k k_r$ and $Y \otimes_k k_r$ embed isometrically into the $k_r$-Banach spaces $X \hat{\otimes}_k k_r$ and $Y \hat{\otimes}_k k_r$, hence $(X \otimes_k k_r) \otimes_{k_r} (Y \otimes_k k_r)$ embeds isometrically into $(X \hat{\otimes}_k k_r) \otimes_{k_r} (Y \hat{\otimes}_k k_r)$ (by Lemme 3.1 in my paper "Les espaces de Berkovich sont angéliques", Bulletin SMF 141 (2), 2013 for instance). Now, you have a tensor product of Banach spaces over the non-trivially valued field $k_r$ and Gruson's result applies.
