Valuation Extensions of Algebras Defined by Monic Gr\"obner Bases

Let $K$ be a field, $\mathcal {O}_v$ a valuation ring of $K$ associated to a valuation $v$: $K\rightarrow\Gamma\cup\{\infty\}$, and ${\bf m}_v$ the unique maximal ideal of $\mathcal {O}_v$. Consider an ideal $\mathcal {I}$ of the free $K$-algebra $K\langle X\rangle =K\langle X_1,...,X_n\rangle$ on $X_1,...,X_n$. If ${\cal I}$ is generated by a subset $\mathcal {G}\subset{\cal O}_v\langle X\rangle$ which is a monic Gr\"obner basis of ${\cal I}$ in $K\langle X\rangle$, where $\mathcal {O}_v\langle X\rangle =\mathcal{O}_v\langle X_1,...,X_n\rangle$ is the free $\mathcal{O}_v$-algebra on $X_1,...,X_n$, then the valuation $v$ induces naturally an exhaustive and separated $\Gamma$-filtration $F^vA$ for the $K$-algebra $A=K\langle X\rangle /\mathcal {I}$, and moreover $\mathcal{I}\cap\mathcal{O}_v\langle X\rangle =\langle\mathcal{G}\rangle$ holds in $\mathcal{O}_v\langle X\rangle$; it follows that, if furthermore $\mathcal{G}\not\subset {\bf m}_v{O}_v\langle X\rangle$ and $k\langle X\rangle /\langle\overline{\mathcal G}\rangle$ is a domain, where $k=\mathcal{O}_v/{\bf m}_v$ is the residue field of $\mathcal{O}_v$, $k\langle X\rangle =k\langle X_1,...,X_n\rangle$ is the free $k$-algebra on $X_1,...,X_n$, and $\overline{\mathcal G}$ is the image of $\mathcal{G}$ under the canonical epimorphism $\mathcal{O}_v\langle X\rangle\rightarrow k\langle X\rangle$, then $F^vA$ determines a valuation function $A\rightarrow \Gamma\cup\{\infty\}$, and thereby $v$ extends naturally to a valuation function on the (skew-)field $\Delta$ of fractions of $A$ provided $\Delta$ exists.