The local ring $A_0$ of rational functions regular at $q=0$

Evaluation at $0$ has kernel $(q)$ and induces $\mathbb{Q}[q]\mathrm{/}(q)\cong \mathbb{Q}$, so $(q)$ is a maximal ideal of $\mathbb{Q}[q]$ and $q\mathrm{\ne }0$ (A local ring is a nonzero commutative ring with a unique maximal ideal); in particular $(q)$ is a nonzero prime ideal of the PID $\mathbb{Q}[q]$.

The field of fractions of $A_0$ is $\mathbb{Q}(q)$: every polynomial $f\in \mathbb{Q}[q]$ lies in $A_0$ as $f\mathrm{/}1$, so $\mathrm{Frac}(A_0)$ contains $\mathrm{Frac}(\mathbb{Q}[q])=\mathbb{Q}(q)$ by [L3]; conversely $A_0\subseteq \mathbb{Q}(q)$ and $\mathbb{Q}(q)$ is a field, so $\mathrm{Frac}(A_0)\subseteq \mathbb{Q}(q)$.

By [F2] applied to $\mathfrak{p}=(q)$, the localisation $A_0$ is a local ring with maximal ideal $(q)A_0=q{A}_0$, residue field $\mathbb{Q}$ under evaluation $f\mathrm{/}g\mapsto f(0)\mathrm{/}g(0)$: this map is surjective on constants and its kernel consists precisely of fractions with $f(0)=0$, namely $q{A}_0$, and units exactly the fractions $f\mathrm{/}g$ with $f\mathrm{\notin }(q)$, that is, $f(0)\mathrm{\ne }0$ and $g(0)\mathrm{\ne }0$.

By step 1.1, $(q)$ is a nonzero prime ideal of the principal ideal domain $\mathbb{Q}[q]$, and by step 2.1 the ring $A_0$ is a local domain with maximal ideal $q{A}_0\mathrm{\ne }0$. Every ideal $J$ of $A_0$ is generated by its contraction: if $f\mathrm{/}g\in J$ with $g(0)\mathrm{\ne }0$ then $f=g\cdot (f\mathrm{/}g)\in J\cap \mathbb{Q}[q]$ and $f\mathrm{/}g=f\cdot (1\mathrm{/}g)\in (J\cap \mathbb{Q}[q])A_0$, while $J\cap \mathbb{Q}[q]\subseteq J$ gives the reverse inclusion, so $J=(J\cap \mathbb{Q}[q])A_0$. The contraction $J\cap \mathbb{Q}[q]$ is an ideal of the principal ideal domain $\mathbb{Q}[q]$, hence principal, so $J$ is principal and $A_0$ is a local principal ideal domain with nonzero maximal ideal. By [L1] it is a discrete valuation ring; its maximal ideal is generated by $q\mathrm{/}1$, so $q\mathrm{/}1$ is a uniformiser, and by [L2] there is a discrete valuation $v$ of $\mathbb{Q}(q)$ with $A_0=\{h:v(h)\ge 0\}$.

Normalisation. Every nonzero $x=f\mathrm{/}g\in \mathbb{Q}(q)$ can be written uniquely as $q^{n}u$ with $n\in \mathbb{Z}$ and $u\in A_0^{\times }$: factor the maximal powers of $q$ from the nonzero polynomials $f,g$ and subtract their exponents. For the discrete valuation $v$ of step 3.1, units have value zero because both $u$ and $u^{-1}$ lie in $A_0$, so $v(x)=nv(q)$. Surjectivity of $v$ onto $\mathbb{Z}$ therefore forces $v(q)=1$. Set ${\mathrm{ord}}_q=v$; this is the vanishing order just computed, with value group $\mathbb{Z}$ and valuation ring $A_0$.

Uniqueness and units: if $w$ is any discrete valuation with $V_w=A_0$ and $w(q)=1$, then $w={\mathrm{ord}}_q$. Indeed, for $x\in \mathbb{Q}(q{)}^{\times }$ one has $w(x)=0$ exactly when $x\in A_0$ and $x^{-1}\in A_0$, that is, exactly when $x\in A_0^{\times }$; for nonzero $x$ the element $x\mathrm{/}{q}^{{\mathrm{ord}}_q(x)}$ lies in $A_0^{\times }$, so $w(x)=w(q^{{\mathrm{ord}}_q(x)})+0={\mathrm{ord}}_q(x)$, using $w(q)=1$, additivity and $w(1)=0$. Thus ${\mathrm{ord}}_q$ is the unique such valuation and $A_0=\{h:{\mathrm{ord}}_q(h)\ge 0\}$, with units $\{h\mathrm{\ne }0:{\mathrm{ord}}_q(h)=0\}$.

Units and comparisons with $A$: step 2.1 gives the units. For the comparisons, $q^{-1}\in A$ by [L4] with $u=q^{-1}$ in $R=\mathbb{Q}(q)$ but $q^{-1}\mathrm{\notin }{A}_0$, because $q^{-1}=f\mathrm{/}g$ with $g(0)\mathrm{\ne }0$ would give $g=qf$ and hence $g(0)=0$, a contradiction; and $(1+q{)}^{-1}\in A_0$ because $1+q$ has value $1\mathrm{\ne }0$ at $0$, while $(1+q{)}^{-1}\mathrm{\notin }A$, because the unique homomorphism $A\to \mathbb{Z}$ with $q\mapsto 1$ of [L4] would send $(1+q{)}^{-1}(1+q)=1$ to ${\mathrm{e}\mathrm{v}}_1((1+q{)}^{-1})\cdot 2=1$, forcing the integer ${\mathrm{e}\mathrm{v}}_1((1+q{)}^{-1})=1\mathrm{/}2$, which is impossible.

The crystal limit: let $L={⨁}_{j\in J}{A}_0{e}_j$ be a free $A_0$-module with the displayed basis. The residue classes $e_j+qL$ form a $\mathbb{Q}$-basis of $L\mathrm{/}qL$ because $A_0\mathrm{/}q{A}_0\cong \mathbb{Q}$ by step 2.1, and the elements $1\otimes e_j$ form a $\mathbb{Q}$-basis of $\mathbb{Q}{\otimes }_{A_0}L$; the displayed map sends the second basis to the first, so it is an isomorphism. For $\lambda \in \mathbb{Q}(q{)}^{\times }$, multiplication by $\lambda$ is a bijection $L\to \lambda L$ carrying $qL$ onto $q\lambda L=\lambda qL$, hence induces an $A_0$-module isomorphism $L\mathrm{/}qL\to \lambda L\mathrm{/}q\lambda L$. No choice principle is used: the basis of $L$ is given, and all further objects are residue projections of explicitly presented fractional ideals of $\mathbb{Q}[q]$.