# 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.

• Small comment: I would be a little careful with the operation $/$, because dividing on the left or on the right may not be the same thing. E.g. $x_1x_2^{-1}$ should not equal $x_2^{-1}x_1$. I guess part of the difficulty is that probably not every element is of the form $fg^{-1}$ for $f$ and $g$ in the free algebra, and it might be desirable to allow both left and right division. (Disclaimer: my comment is not burdened by any relevant knowledge.) – R. van Dobben de Bruyn Jun 21 '20 at 20:52
• @R.vanDobbendeBruyn: True, I should say "inverse" rather than "division". – darij grinberg Jun 21 '20 at 20:56
• If $F=\mathbb{Q}$ and A2 and equality is decidable and $+,-,\cdot,\,^{-1}$ are computable, then you end up with a normal form: the first equal element in the order in which elements are generated. – Matt F. Jun 22 '20 at 2:49