Proof of Noncommutative Polynomials Form a Unital Complex Algebra with Involution: Linear Extension from Monomials, Products, Adjoints and Self-Adjoint Parts

We use the definitions The Algebra of Noncommutative Polynomials in Finitely Many Self-Adjoint Variables (clauses The Algebra of Noncommutative Polynomials in Finitely Many Self-Adjoint Variables §polynomials, The Algebra of Noncommutative Polynomials in Finitely Many Self-Adjoint Variables §linear, The Algebra of Noncommutative Polynomials in Finitely Many Self-Adjoint Variables §monomials, The Algebra of Noncommutative Polynomials in Finitely Many Self-Adjoint Variables §product, The Algebra of Noncommutative Polynomials in Finitely Many Self-Adjoint Variables §adjoint, The Algebra of Noncommutative Polynomials in Finitely Many Self-Adjoint Variables §self-adjoint), Words over a Finite Alphabet: the Empty Word, Concatenation and Reversal, Field, The Complex Numbers, Complex Conjugate, Real and Imaginary Parts of a Complex Number, Vector Space over a Field, Linear Map, Finite Set, Sum over a Finite Index Set, Finite Sum Notation in a Field and Finite Sum Notation in a Vector Space; the sibling drafts Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus and Basic Properties of Words: Associativity, Reversal, Finitely Many Factorisations, and Countability; and the lemmas Properties of a Sum over a Finite Index Set, Properties of Finite Sums, Properties of Finite Sums of Vectors, Elementary Identities in a Vector Space, Zero Products and Elementary Identities in a Field, Additive Cancellation and Elementary Additive Identities in a Field, Properties of Complex Conjugation and Modulus, Canonical Form and Arithmetic of Complex Numbers, Properties of the Canonical Map from the Natural Numbers to an Ordered Field, Basic Properties of Finite Sets, Peeling an Element off a Finite Set, and Unions of Finite Sets, Basic Properties of Initial Segments of the Natural Numbers, Inverse of a Bijection and Characteristic Property of the Ordered Pair.

Preliminaries. Write $\mathcal{P}=\mathcal{P}_{n}$. Arithmetic in $\mathbb{C}$ uses the field axioms of Field without further mention.

(P1) Sums over a singleton. For an object $y$ and a map $g:\{y\}\to\mathbb{C}$, $\sum_{x\in\{y\}}g(x)=g(y)$: the set $\{y\}$ has $1$ element (claim 2 of Basic Properties of Finite Sets), $1\mapsto y$ is a bijection $[1]\to\{y\}$ as $[1]=\{1\}$ (claim 2 of Basic Properties of Initial Segments of the Natural Numbers), and $\sum_{k=1}^{1}a_{k}=a_{1}$ by claim 1 of Properties of Finite Sums; now apply Sum over a Finite Index Set.

(P2) Constants. By claim 1 of Canonical Form and Arithmetic of Complex Numbers, $0$, $1$ and $-1$ of $\mathbb{C}$ are real numbers. The natural number $2=1+1$ satisfies $\iota_{\mathbb{R}}(2)=1+1$ and $\iota_{\mathbb{R}}(2)\neq0$ by claims 1 and 3 of Properties of the Canonical Map from the Natural Numbers to an Ordered Field; so $2=1+1$ is a nonzero real number (its sum in $\mathbb{C}$ is the real one by condition 1 of The Complex Numbers), and its inverse $\tfrac12$ in $\mathbb{C}$ is real by claim 1 of Canonical Form and Arithmetic of Complex Numbers. We read $-\tfrac{i}{2}$ as $-(i\cdot\tfrac12)$, $a^{2}$ as $aa$, and $p-q$ as $p+(-1)q$ (The Algebra of Noncommutative Polynomials in Finitely Many Self-Adjoint Variables §linear). Also $i\neq0$, since $i\notin\mathbb{R}$ (claim 2 of Canonical Form and Arithmetic of Complex Numbers) while $0\in\mathbb{R}$.

(P3) Conjugates. By claim 1 of Properties of Complex Conjugation and Modulus, conjugation is additive and multiplicative, involutive, and fixes every real number, in particular $0$, $1$, $-1$, $\tfrac12$ by (P2); hence $\overline{z-w}=\overline{z}-\overline{w}$. Since $i=0+1\cdot i$ with $0,1$ real, Real and Imaginary Parts of a Complex Number gives $\operatorname{Re}i=0$, $\operatorname{Im}i=1$, so $\overline{i}=0-1\cdot i=-i$ by Complex Conjugate.

(P4) $\mathbb{C}$ as a vector space. As in the statement, $\mathbb{C}$ is a complex vector space with its field operations (conditions 1-8 of Vector Space over a Field are instances of the field axioms), and its finite sums of vectors (Finite Sum Notation in a Vector Space) are the finite sums of Finite Sum Notation in a Field, both definitions prescribing the same recursion. Linear operations on $\mathcal{P}$ are pointwise, so for each $w\in W_{n}$ the evaluation $\mathrm{ev}_{w}(p)=p(w)$ is a linear map $\mathcal{P}\to\mathbb{C}$ (The Algebra of Noncommutative Polynomials in Finitely Many Self-Adjoint Variables §linear, Linear Map), once Claim 1 is shown.

Claim 1 (vector space). By The Algebra of Noncommutative Polynomials in Finitely Many Self-Adjoint Variables §linear, $p+q$ and $cp$ are polynomials, and the zero polynomial is a polynomial as its support is empty, hence finite (Finite Set). The conditions of Vector Space over a Field hold pointwise: 1, 2 by axioms 1, 4 of Field; 3 with $0_{V}$ the zero polynomial, by axiom 2; 4 with $w=(-1)p$, because $(-1)p(v)=-p(v)$ by claim 2 of Zero Products and Elementary Identities in a Field (and $1\cdot p(v)=p(v)$), and $p(v)+(-p(v))=0$ by axiom 3; 5 by axiom 5; 6 by axioms 6 and 8; 7 by axiom 9; 8 by axioms 8 and 9. The zero vector is unique by claim 1 of Elementary Identities in a Vector Space, so it is the zero polynomial.

Claim 2 (linear extension). (a) Define $\ell$ as in the statement. Note $p\neq0$ means $\operatorname{supp}p\neq\emptyset$, and $\operatorname{supp}p$ is finite (The Algebra of Noncommutative Polynomials in Finitely Many Self-Adjoint Variables §polynomials).

Step 1 (common index sets). If $S\subseteq W_{n}$ is nonempty and finite and $\operatorname{supp}p\subseteq S$, then $\ell(p)=\sum_{w\in S}p(w)c(w)$. If $p=0$, every term is $0\cdot c(w)=0$ (claim 1 of Zero Products and Elementary Identities in a Field), so the sum is $0=\ell(0)$ by the first sentence of Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus §vanishing. If $p\neq0$, the terms with $w\in S\setminus\operatorname{supp}p$ are $0\cdot c(w)=0$, so the second sentence of Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus §vanishing, with $G=\operatorname{supp}p$, gives the claim.

Step 2 (linearity). Let $p,q\in\mathcal{P}$, $\lambda\in\mathbb{C}$, and $S=\operatorname{supp}p\cup\operatorname{supp}q\cup\{\varnothing\}$, nonempty and finite by claims 3 and 1 of Peeling an Element off a Finite Set, and Unions of Finite Sets. It contains $\operatorname{supp}p$, $\operatorname{supp}q$, $\operatorname{supp}(p+q)$ and $\operatorname{supp}(\lambda p)$ (The Algebra of Noncommutative Polynomials in Finitely Many Self-Adjoint Variables §linear). By Step 1, distributivity, and claims 3 and 4 of Properties of a Sum over a Finite Index Set,

So $\ell$ is linear (Linear Map, with (P4)).

Step 3. $\operatorname{supp}x_{w}=\{w\}$ (The Algebra of Noncommutative Polynomials in Finitely Many Self-Adjoint Variables §monomials), so by (P1), $\ell(x_{w})=x_{w}(w)c(w)=c(w)$.

Step 4 (expansion in monomials). Let $p\neq0$, let $N$ be the number of elements of $\operatorname{supp}p$ and $\varphi:[N]\to\operatorname{supp}p$ a bijection (Finite Set), and $v_{k}=p(\varphi(k))\,x_{\varphi(k)}\in\mathcal{P}$. We claim $p=\sum_{k=1}^{N}v_{k}$ (finite sum in the vector space $\mathcal{P}$). Fix $w\in W_{n}$. By claim 4 of Properties of Finite Sums of Vectors applied to $\mathrm{ev}_{w}$ (see (P4)), $\bigl(\sum_{k=1}^{N}v_{k}\bigr)(w)=\sum_{k=1}^{N}p(\varphi(k))\,x_{\varphi(k)}(w)$. If $w\in\operatorname{supp}p$, then $w=\varphi(i)$ for exactly one $i\in[N]$; the $i$th term is $p(w)$ and the others are $p(\varphi(k))\cdot0=0$, so the sum is $p(w)$ by claim 7 of Properties of Finite Sums. If $w\notin\operatorname{supp}p$, all terms are $0$, so the sum is $0=p(w)$ by the same claim (with $i=1$).

Step 5 (uniqueness). Let $\ell'$ be linear with $\ell'(x_{w})=c(w)$ for all $w$. Then $\ell'(0)=\ell'(0\cdot0)=0\cdot\ell'(0)=0$ by claim 3 of Elementary Identities in a Vector Space and annihilation. For $p\neq0$, Step 4 and claim 4 of Properties of Finite Sums of Vectors give

the third equality by Sum over a Finite Index Set with the bijection $\varphi$. Hence $\ell'=\ell$.

(b) Step 1 ($T(p)\in\mathcal{P}_{m}$). Let $p\neq0$. If $T(p)(v)\neq0$, then by the first sentence of Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus §vanishing some term $p(w)c(w)(v)$ with $w\in\operatorname{supp}p$ is nonzero, so $c(w)(v)\neq0$ by annihilation (claim 1 of Zero Products and Elementary Identities in a Field), i.e. $v\in\operatorname{supp}c(w)$. Thus $\operatorname{supp}T(p)\subseteq\bigcup_{w\in\operatorname{supp}p}\operatorname{supp}c(w)$, which is finite by Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus §finite-union; so $T(p)$ is a polynomial by claim 3 of Basic Properties of Finite Sets. $T(0)=0$ is one by Claim 1.

Step 2. For $v\in W_{m}$ let $c_{v}(w)=c(w)(v)$ and let $\ell_{v}$ be the linear map of (a) for $c_{v}$. Then $T(p)(v)=\ell_{v}(p)$ for all $p$ (both are $0$ at $p=0$). Hence $T(p+q)(v)=\ell_{v}(p)+\ell_{v}(q)=(T(p)+T(q))(v)$ and $T(\lambda p)(v)=\lambda\,T(p)(v)=(\lambda T(p))(v)$, so $T$ is linear; and $T(x_{w})(v)=\ell_{v}(x_{w})=c(w)(v)$, so $T(x_{w})=c(w)$.

Step 3 (uniqueness). If $T'$ is linear with $T'(x_{w})=c(w)$, then for each $v$ the composite $p\mapsto T'(p)(v)=\mathrm{ev}_{v}(T'(p))$ is linear (both conditions of Linear Map pass through composition) and sends $x_{w}$ to $c_{v}(w)$, so it equals $\ell_{v}$ by (a). Thus $T'(p)(v)=T(p)(v)$ for all $p,v$, and $T'=T$.

Claim 3 (monomials). By The Algebra of Noncommutative Polynomials in Finitely Many Self-Adjoint Variables §product, $(x_{u}x_{v})(w)=\sum_{(s,t)\in F(w)}x_{u}(s)x_{v}(t)$, and the term is $1$ if $s=u$ and $t=v$, and $0$ otherwise (annihilation, claim 1 of Zero Products and Elementary Identities in a Field). If $w=uv$, then $(u,v)\in F(w)$, every $(s,t)\in F(w)$ other than $(u,v)$ has $s\neq u$ or $t\neq v$ (Characteristic Property of the Ordered Pair), so by Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus §vanishing with $G=\{(u,v)\}$ and (P1) the sum is $1$. If $w\neq uv$, no $(s,t)\in F(w)$ equals $(u,v)$ (else $w=st=uv$), so the sum is $0$ by Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus §vanishing. Hence $x_{u}x_{v}=x_{uv}$.

For $1p$: $(1p)(w)=\sum_{(s,t)\in F(w)}x_{\varnothing}(s)p(t)$, and $(\varnothing,w)\in F(w)$ by Basic Properties of Words: Associativity, Reversal, Finitely Many Factorisations, and Countability §monoid. If $(s,t)\in F(w)$ and $s=\varnothing$, then $t=\varnothing t=w$ by the same clause; so every other pair has $s\neq\varnothing$ and term $0$ (claim 1 of Zero Products and Elementary Identities in a Field). By Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus §vanishing and (P1), $(1p)(w)=x_{\varnothing}(\varnothing)p(w)=p(w)$. Symmetrically, with the pair $(w,\varnothing)$, $(p1)(w)=p(w)$.

Claim 4 (algebra). Step 1 (distributivity and scalars). For $w\in W_{n}$, sums over $F(w)$ and claims 3 and 4 of Properties of a Sum over a Finite Index Set give

and likewise $((p+q)r)(w)=(pr)(w)+(qr)(w)$, and $((cp)q)(w)=\sum c\,p(u)q(v)=c\,(pq)(w)=(p(cq))(w)$.

Step 2 (associativity). Fix $w$. By The Algebra of Noncommutative Polynomials in Finitely Many Self-Adjoint Variables §product and claim 4 of Properties of a Sum over a Finite Index Set (with $\lambda=r(z)$),

where the second equality is Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus §pairs with $A=F(w)$ and $B((s,z))=F(s)$, nonempty and finite by Basic Properties of Words: Associativity, Reversal, Finitely Many Factorisations, and Countability §factorisations (well defined by Characteristic Property of the Ordered Pair), $T_{1}$ is the set of pairs $((s,z),(u,v))$ with $(s,z)\in F(w)$ and $(u,v)\in F(s)$, and $f(((s,z),(u,v)))=p(u)q(v)r(z)$. In the same way, with $\lambda=p(u)$,

with $T_{2}$ the set of pairs $((u,t),(v,z))$ with $(u,t)\in F(w)$, $(v,z)\in F(t)$, and $g(((u,t),(v,z)))=p(u)q(v)r(z)$. Define $\theta:T_{1}\to T_{2}$ by $\theta(((s,z),(u,v)))=((u,vz),(v,z))$ and $\eta:T_{2}\to T_{1}$ by $\eta(((u,t),(v,z)))=((uv,z),(u,v))$. These land in the stated sets: if $uv=s$ and $sz=w$, then $u(vz)=(uv)z=w$; if $vz=t$ and $ut=w$, then $(uv)z=u(vz)=w$ (Basic Properties of Words: Associativity, Reversal, Finitely Many Factorisations, and Countability §monoid). Moreover $\eta(\theta(((s,z),(u,v))))=((uv,z),(u,v))=((s,z),(u,v))$ and $\theta(\eta(((u,t),(v,z))))=((u,vz),(v,z))=((u,t),(v,z))$, so $\theta$ is a bijection by claim 3 of Inverse of a Bijection, and $g\circ\theta=f$. By claim 2 of Properties of a Sum over a Finite Index Set, $\sum_{T_{1}}f=\sum_{T_{2}}g$, so $(pq)r=p(qr)$.

Claim 5 (adjoint). Let $w\in W_{n}$; by The Algebra of Noncommutative Polynomials in Finitely Many Self-Adjoint Variables §adjoint and (P3): $(p+q)^{*}(w)=\overline{p(w^{\mathrm{rev}})}+\overline{q(w^{\mathrm{rev}})}=p^{*}(w)+q^{*}(w)$; $(cp)^{*}(w)=\overline{c}\,\overline{p(w^{\mathrm{rev}})}=(\overline{c}\,p^{*})(w)$; and $(p^{*})^{*}(w)=\overline{\overline{p((w^{\mathrm{rev}})^{\mathrm{rev}})}}=p(w)$ by Basic Properties of Words: Associativity, Reversal, Finitely Many Factorisations, and Countability §reversal.

Monomials: $(x_{w})^{*}(v)=\overline{x_{w}(v^{\mathrm{rev}})}$. If $v=w^{\mathrm{rev}}$ then $v^{\mathrm{rev}}=w$ and the value is $\overline{1}=1$; if $v\neq w^{\mathrm{rev}}$ then $v^{\mathrm{rev}}\neq w$ (else $v=(v^{\mathrm{rev}})^{\mathrm{rev}}=w^{\mathrm{rev}}$) and the value is $\overline{0}=0$. So $(x_{w})^{*}=x_{w^{\mathrm{rev}}}$. Since $\varnothing^{\mathrm{rev}}=\varnothing$ (Words over a Finite Alphabet: the Empty Word, Concatenation and Reversal §reversal) and $(j)^{\mathrm{rev}}=(j)$ (Basic Properties of Words: Associativity, Reversal, Finitely Many Factorisations, and Countability §reversal), $1^{*}=1$ and $x_{j}^{*}=x_{j}$.

Products: by The Algebra of Noncommutative Polynomials in Finitely Many Self-Adjoint Variables §product, Sums over Finite Index Sets: Finite Unions, Disjoint Unions, Vanishing Terms, Dependent Pairs, Conjugation and the Modulus §conjugate and (P3),

where $h((s,t))=\overline{q(s^{\mathrm{rev}})}\,\overline{p(t^{\mathrm{rev}})}$. Let $\beta(u,v)=(v^{\mathrm{rev}},u^{\mathrm{rev}})$ and $\beta'(s,t)=(t^{\mathrm{rev}},s^{\mathrm{rev}})$. By Basic Properties of Words: Associativity, Reversal, Finitely Many Factorisations, and Countability §reversal, if $uv=w^{\mathrm{rev}}$ then $v^{\mathrm{rev}}u^{\mathrm{rev}}=(uv)^{\mathrm{rev}}=w$, and if $st=w$ then $t^{\mathrm{rev}}s^{\mathrm{rev}}=w^{\mathrm{rev}}$; so $\beta:F(w^{\mathrm{rev}})\to F(w)$ and $\beta':F(w)\to F(w^{\mathrm{rev}})$, and they are mutually inverse because reversal is involutive. So $\beta$ is a bijection (claim 3 of Inverse of a Bijection), and $h(\beta(u,v))=\overline{q(v)}\,\overline{p(u)}=\overline{p(u)}\,\overline{q(v)}$. By claim 2 of Properties of a Sum over a Finite Index Set, $(pq)^{*}(w)=(q^{*}p^{*})(w)$.

Claim 6 (self-adjoint part). By Claim 5, $0^{*}=0$ (as $\overline{0}=0$), $1^{*}=1$ and $x_{j}^{*}=x_{j}$. For $a,b\in\mathcal{P}_{n,\mathrm{sa}}$ and $\lambda\in\mathbb{R}$: $(a+b)^{*}=a+b$ and $(\lambda a)^{*}=\overline{\lambda}a=\lambda a$ by (P3). With these operations, conditions 1, 2, 7 of Vector Space over a Field are inherited from Claim 1; 5 and 8 too, because sums and products of real numbers formed in $\mathbb{C}$ are the real ones (condition 1 of The Complex Numbers); 6 because the unit of $\mathbb{R}$ is that of $\mathbb{C}$ (P2); 3 with $0\in\mathcal{P}_{n,\mathrm{sa}}$; and 4 with $(-1)a\in\mathcal{P}_{n,\mathrm{sa}}$, as $-1$ is real (P2). So $\mathcal{P}_{n,\mathrm{sa}}$ is a real vector space.

By Claim 5, $(ab+ba)^{*}=b^{*}a^{*}+a^{*}b^{*}=ba+ab=ab+ba$; $(p+p^{*})^{*}=p^{*}+p=p+p^{*}$; $(p^{*}p)^{*}=p^{*}(p^{*})^{*}=p^{*}p$. For the remaining one, by Claim 5 and (P3), $(i(ab-ba))^{*}=(-i)\bigl(ba+(-1)ab\bigr)$, whose value at $w$ is $(-i)\bigl((ba)(w)-(ab)(w)\bigr)=i\bigl((ab)(w)-(ba)(w)\bigr)$; so $(i(ab-ba))^{*}=i(ab-ba)$.

Claim 7 (real and imaginary parts). Step 1 (existence). Let $a=\tfrac12(p+p^{*})$ and $b=-\tfrac{i}{2}(p-p^{*})$. By Claim 5 and (P3), $a^{*}=\tfrac12(p^{*}+p)=a$, and pointwise $b^{*}(w)=\overline{-\tfrac{i}{2}}\bigl(p^{*}(w)-p(w)\bigr)=\tfrac{i}{2}\bigl(p^{*}(w)-p(w)\bigr)=b(w)$, using $(p^{*})^{*}=p$. Pointwise, since $i\cdot i=-1$ (condition 2 of The Complex Numbers), $i\cdot(-\tfrac{i}{2})=\tfrac12$, so $(a+ib)(w)=\tfrac12\bigl(p(w)+p^{*}(w)\bigr)+\tfrac12\bigl(p(w)-p^{*}(w)\bigr)=\tfrac12(1+1)p(w)=p(w)$.

Step 2 (uniqueness). Let $p=a+ib=a'+ib'$ with $a,b,a',b'$ self-adjoint, and put $d=a-a'$, $e=b'-b$, self-adjoint by Claim 6. Pointwise $d(w)=i\,e(w)$. By (P3), $d(w)=d^{*}(w)=\overline{i\,e(w^{\mathrm{rev}})}=-i\,e^{*}(w)=-i\,e(w)=-d(w)$, so $(1+1)d(w)=0$ and $d(w)=0$ by claim 3 of Zero Products and Elementary Identities in a Field and (P2). Then $i\,e(w)=0$, so $e(w)=0$ as $i\neq0$ (P2). Hence $a=a'$ and $b=b'$.

Step 3 ($p^{*}=a-ib$). Pointwise $p^{*}(w)=\overline{a(w^{\mathrm{rev}})+i\,b(w^{\mathrm{rev}})}=a^{*}(w)-i\,b^{*}(w)=a(w)-i\,b(w)$ by (P3).

Step 4. Write $a-ib=a+(-i)b$ (condition 5 of Vector Space over a Field and claim 2 of Zero Products and Elementary Identities in a Field). By Claim 4 (distributivity and scalars), conditions 1, 2, 5, 6, 7 of Vector Space over a Field, and $(-i)i=-(i\cdot i)=1$ (claim 2 of Zero Products and Elementary Identities in a Field, claim 5 of Additive Cancellation and Elementary Additive Identities in a Field),

using $(-i)(ba)=i\bigl((-1)(ba)\bigr)$ in the last step. $\blacksquare$