# The question

Let $F$ be a field. (I am fine with assuming $F=\mathbb{Q}$, but I suspect that a "right" answer will be independent of $F$.) Let $k$ be a nonnegative integer.

Question.Is there a constructive definition of a skew field $S_k$ of noncommutative rational functions in $k$ variables $x_{1},x_{2},\ldots,x_{k}$ over $F$ ?

"Noncommutative rational functions" should mean the following assumptions:

**Assumption A1:** $S_k$ is an $F$-algebra and a skew field. Here, "skew field"
is to be understood constructively -- i.e., there is an
algorithm that takes any element $a\in S_k$ as input and returns either
$a^{-1}$ or a proof that $a=0$.

**Assumption A2:** Every element of $S_k$ is obtained from the generators
$x_{1},x_{2},\ldots,x_{k}$ and
the elements of $F$ by the operations $+,-,\cdot,^{-1}$, where the latter
operation means inverting a nonzero element.

**Assumption A3:** For any $F$-algebra $A$,
there is a partially-defined "evaluation map"
$\operatorname{ev} : S_k \times A^k \to A \sqcup \left\{\operatorname{undefined}\right\}$
that sends every pair $\left(f, \left(a_1, a_2, \ldots, a_k\right)\right)$
(with $f \in S_k$ and $a_1, a_2, \ldots, a_k \in A$) either to an
element of $A$ or to the value $\operatorname{undefined}$.
This map $\operatorname{ev}$ should send each such pair
$\left(f, \left(a_1, a_2, \ldots, a_k\right)\right)$ to the result
of substituting $a_1, a_2, \ldots, a_k$ for $x_1, x_2, \ldots, x_k$
in $f$ (more precisely, in some representation of $f$ as a $+,-,\cdot,^{-1}$-expression in the $x_{1},x_{2},\ldots,x_{k}$)
if this substitution is well-defined (i.e., if the denominators are
invertible after the substitution), and otherwise to $\operatorname{undefined}$.
(Thus, this map should be an $F$-algebra homomorphism in its first
argument, and should send $\left(x_i, \left(a_1, a_2, \ldots, a_k\right)\right)$
to $a_i$ for each $i \in \left\{1,2,\ldots, k\right\}$. It should also be "maximally defined" -- i.e., it shouldn't take the value $\operatorname{undefined}$ without reason.)

**Assumption A4:** For any $f \in S_k$, there exist (and can be explicitly
constructed) a positive integer $n$ and some $n\times n$-matrices $A_1, A_2, \ldots, A_k$ over $F$
such that $\operatorname{ev} \left(f, \left(A_1, A_2, \ldots, A_k\right)\right)$
is not $\operatorname{undefined}$.
(This means that the nonvanishing of the denominators in
$f$ can be "witnessed" by explicit matrices.)

The definitions I've seen (via some handwavy noncommutative localization, or via explicit embedding into noncommutative power series) are both nonconstructive, but I haven't looked beyond the surveys.

I'd also want $S_k$ to embed into $S_{k+1}$.

# Why I care

Free skew fields come up in algebraic combinatorics as the theater for noncommutative birational rowmotion, for Kontsevich--Iyudu--Shkarin periodicity and for quasideterminants, as well as in the work of Schützenberger apparently inspired by automata theory. In simple cases, the use of $S_k$ is completely optional, and it suffices to work in an arbitrary ring and just require that denominators appearing in one's theorems are invertible. However, this kind of reasoning doesn't allow us to introduce extra denominators by WLOG assumption, as is commonly done in the commutative case using Zariski density. That is, if I want to prove that two noncommutative rational expressions $a$ and $b$ are equal everywhere they are defined, I cannot use any rational expressions with denominators that don't appear in $a$ or $b$. (In particular, I cannot argue that $ac = bc$ and $c \neq 0$ imply $a = b$; there is nothing that a-priori guarantees the equality of $a$ and $b$ outside of the domain where $c$ is invertible.) The situation is even worse if I want to use Zariski topology properly, such as defining birational equivalences (a followup question I will ask once this one is resolved). The concrete impetus for this question is a theorem about periodicity of birational rowmotion (joint work with Tom Roby), which we can prove in the noncommutative case but only up to the existence of a reasonably well-behaved notion of "general position" (i.e., Zariski density).

# What (little) I know

From what I understand, the only(?) systematic textbook on this subject is
Paul Cohn, *Free Ideal Rings and Localization in General
Rings*, which gets to the existence of $S_k$ (or at
least something similar) somewhere in Section 7.5 after 400+ pages of general
theory. Admittedly, Cohn probably doesn't use too much of the earlier chapters
there, but still it is a daunting perspective to read a whole book for a
single theorem. Worse yet, I have no reason to expect that the proof is
constructive (Zorn's lemma is being used at least 3 times before that point).

Gelfand and Retakh, in their paper *Determinants of matrices over
noncommutative rings*, take a different
road to $S_k$, or at least to the inverses that they need in their study of
quasideterminants (probably a smaller ring than $S_k$, and not quite a skew
field): they embed things in a completed monoid ring $\mathcal{R}$ of a
certain monoid. (The monoid consists of what they call "special monomials".
The word "completed" means completed with respect to degree -- thus, a
noncommutative version of formal power series.) Unfortunately, the "completed"
part here destroys constructivity, because checking whether two elements of
$\mathcal{R}$ are equal reduces to the halting problem. This is quite possibly
sufficient for a good chunk of the theory quasideterminants, where equality
checking isn't necessary; but for what I am doing, it certainly is not.

Cohn and Reutenauer have a paper called *A Normal Form in Free
Fields*, which however is not
constructive either (again due to power series being involved). Note that I am
not insisting on a normal form, merely on decidable equality and computable inverses.