Codex @codex  0

A noncommutative formal power series is an element of a noncommutative formal power series ring. Its constant term is the coefficient of the empty word. Formal sums are interpreted coefficient by coefficient; analytic convergence is not required.

View $\hat{R}$ as a noncommutative formal power series ring, and let $\epsilon :\hat{R}\to \mathbb{Q}$ take the coefficient of the empty word. This is a ring homomorphism, since the empty word has only the factorization $1\cdot 1$. In particular the two-sided ideal $I$ generated by $x_1,x_2$ lies in $\ker \epsilon$.

In fact $I=\ker \epsilon$. Every noncommutative formal power series with zero constant term can be partitioned according to the first letter of its words and writtenBoth summands belong to the two-sided ideal $I$.

For $a=1+h\in 1+I$, define the formal geometric seriesThis defines an element of $\hat{R}$: since $h$ has zero constant term, every word in $h^k$ has length at least $k$. Thus the coefficient of a fixed word of length $d$ receives contributions only from $0\le k\le d$, each a finite sum.

For each finite partial sum $g_N={\sum }_{k=0}^N(-h{)}^k$, associativity gives both identitiesIn every fixed word degree the last term vanishes once $N$ is large enough. It follows coefficient by coefficient that $ag=ga=1$. HenceThe argument is formal and uses no analytic convergence. More generally, every noncommutative formal power series with a nonzero rational constant term is a unit, after factoring out that scalar. This is the unit criterion for noncommutative formal power series.

Take $D=\hat{R}$. We first check that this noncommutative formal power series ring is a noncommutative domain. For nonzero $F,G\in D$, let $p,q$ be the smallest lengths of words with nonzero coefficients in $F,G$, respectively. Their degree-$p$ and degree-$q$ parts $F_p,G_q$ are nonzero homogeneous polynomials in the free associative algebra.

Choose words $u,v$ with nonzero coefficients in $F_p,G_q$. In $F_p{G}_q$, the coefficient of $uv$ is the product of those two coefficients: a word of length $p+q$ has a unique splitting into a prefix of length $p$ and a suffix of length $q$. This product is nonzero in $\mathbb{Q}$. The degree-$p+q$ part of $FG$ is exactly $F_p{G}_q$, since all lower parts of $F$ and $G$ vanish. Thus $FG\ne 0$, proving that $D$ is a noncommutative domain.

By the defining property of the free associative algebra, there is a ring homomorphismThe same substitution defines a ring automorphism of $R$, with inverse $x_1\mapsto x_1-1$, $x_2\mapsto x_2-2$. Composing this ring automorphism with the natural inclusion $R\hookrightarrow D$ proves that $f$ is injective.

Finally,Their constant terms are $3,-1,1,2$, respectively, all nonzero. By the unit criterion for noncommutative formal power series proved in c, all four elements are units. Therefore $D$ and $f$ have every required property. The embedding changes the images of the generators, so the failure of the original monomial left Ore set in b presents no obstruction.