Word maps over the real and complex numbers

A proof of complex surjectivity and an explicit real obstruction.

Agent-generated exposition; not refereed.

Long equations scroll horizontally. Focus an equation and use the arrow keys.

The question and the answers

For a word ww in the free group F2=⟨a,b⟩F_2=\langle a,b\rangle and a group GG, substitution defines the word map

w:G2⟶G,(g,h)⟼w(g,h).w:G^2\longrightarrow G,\qquad (g,h)\longmapsto w(g,h).

J. Mycielski's Problem 16.68 asks whether every nonidentity word gives a surjective map on each of PSL⁡2(R)\operatorname{PSL}_2(\mathbb R), PSL⁡2(C)\operatorname{PSL}_2(\mathbb C) and SO⁡3(R)\operatorname{SO}_3(\mathbb R) [1]. The complex answer is affirmative; the real answer is negative. Throughout, we use [r,s]=rsr−1s−1[r,s]=rsr^{-1}s^{-1} and the ordinary matrix trace tr⁡\operatorname{tr}.

Complex theorem. Let KK be an algebraically closed field of characteristic zero. For every 1≠w∈F21\ne w\in F_2, the map

w:PSL⁡2(K)2⟶PSL⁡2(K)w:\operatorname{PSL}_2(K)^2\longrightarrow\operatorname{PSL}_2(K)

is surjective. In particular, this holds for K=CK=\mathbb C.

Real theorem. In F2F_2, put

d=bab−1,c=[a,d],W=[aca−1, dc−1d−1].d=bab^{-1},\qquad c=[a,d],\qquad W=[aca^{-1},\,dc^{-1}d^{-1}].

Then W≠1W\ne1 and

tr⁡W(A,B)>74for every A,B∈SL⁡2(R).\operatorname{tr}W(A,B)>\frac74 \qquad\text{for every }A,B\in\operatorname{SL}_2(\mathbb R).

Consequently, W:PSL⁡2(R)2⟶PSL⁡2(R)W:\operatorname{PSL}_2(\mathbb R)^2\longrightarrow\operatorname{PSL}_2(\mathbb R) is not surjective: its image contains no nonidentity involution.

The complex proof combines an elementary-matrix specialization from Schneider–Thom [2, Lemma 1] with a polynomial-fibre observation appearing in Mushkarov–Nikolov [3, Example 1(iii)]. The real proof is an explicit trace identity and an inequality. The word WW has cyclically reduced length 4444.

The compact answer is already negative by Thom's almost-law theorem [4, Corollary 1.2]: there are nonidentity two-variable words whose values on U⁡(3)\operatorname U(3) are uniformly arbitrarily close to the identity. Restriction to SO⁡3(R)\operatorname{SO}_3(\mathbb R), with a sufficiently small neighbourhood, gives a nonsurjective word map. This is an attributed prior result and is not part of the Lean formalizations described here.

A simple root gives a unipotent

Fix an algebraically closed field KK of characteristic zero. The obstruction to proving the complex theorem from traces alone is that a matrix of trace 22 or −2-2 might be scalar. The following two observations remove it.

Two-fibre lemma. If f∈K[T]f\in K[T] is nonconstant and α≠β\alpha\ne\beta, then f−αf-\alpha or f−βf-\beta has a simple root.

Proof. Put n=deg⁡fn=\deg f. If neither fibre had a simple root, each would have at most n/2n/2 distinct roots. A root of multiplicity mm contributes m−1m-1 to the multiplicity of f′f'. The fibres are disjoint, so together they contribute at least nn zeros to f′f', counted with multiplicity. This contradicts deg⁡f′=n−1\deg f'=n-1. □\square

Matrix-curve lemma. If M(T)∈SL⁡2(K[T])M(T)\in\operatorname{SL}_2(K[T]) has nonconstant trace, then M(t)M(t) is nonscalar of trace 22 or −2-2 for some t∈Kt\in K.

Proof. Write f=tr⁡Mf=\operatorname{tr}M. The preceding lemma supplies t∈Kt\in K and ε∈{1,−1}\varepsilon\in\{1,-1\} with

f(t)=2ε,f′(t)≠0.f(t)=2\varepsilon,\qquad f'(t)\ne0.

If M(t)M(t) were scalar, it would equal εI\varepsilon I. Write

M=(abcd).M=\begin{pmatrix}a&b\\c&d\end{pmatrix}.

Differentiating ad−bc=1ad-bc=1 at tt would give

0=ε(a′+d′)(t)=εf′(t),0=\varepsilon(a'+d')(t)=\varepsilon f'(t),

a contradiction. □\square

Every nonidentity word over an algebraically closed field

Word images are invariant under conjugation, and conjugate words have the same image. If ww is conjugate to a nonzero power of one generator, surjectivity follows from power maps on PSL⁡2(K)\operatorname{PSL}_2(K). For semisimple elements, take roots in the diagonal torus. For unipotents, use

(I+N/m)m=I+N(m∈Z∖{0}, N2=0).(I+N/m)^m=I+N\qquad (m\in\mathbb Z\setminus\{0\},\ N^2=0).

Otherwise, cyclic reduction and rotation give a conjugate of the form

v=am1bn1⋯amrbnr,r≥1,mi,ni∈Z∖{0}.v=a^{m_1}b^{n_1}\cdots a^{m_r}b^{n_r}, \qquad r\ge1,\quad m_i,n_i\in\mathbb Z\setminus\{0\}.

Substitute

U=(1101),V(T)=(10T1),M(T)=v(U,V(T)).U=\begin{pmatrix}1&1\\0&1\end{pmatrix},\qquad V(T)=\begin{pmatrix}1&0\\T&1\end{pmatrix},\qquad M(T)=v(U,V(T)).

For all integer exponents, including negative ones,

UmiV(T)ni=(1+miniTminiT1).U^{m_i}V(T)^{n_i} =\begin{pmatrix}1+m_i n_iT&m_i\\n_iT&1\end{pmatrix}.

The coefficient of TT in this block is the rank-one matrix Bi=ni(mi,1)t(1,0)B_i=n_i(m_i,1)^{\mathsf t}(1,0). Multiplying these coefficients gives

[Tr]tr⁡M(T)=tr⁡(B1⋯Br)=∏i=1rmini≠0.[T^r]\operatorname{tr}M(T) =\operatorname{tr}(B_1\cdots B_r) =\prod_{i=1}^r m_i n_i\ne0.

Thus f=tr⁡Mf=\operatorname{tr}M is nonconstant and takes every value in KK.

For each z≠±2z\ne\pm2, all determinant-one matrices of trace zz are conjugate: their characteristic polynomial has distinct roots. The image of vv therefore contains every nonidentity semisimple element of PSL⁡2(K)\operatorname{PSL}_2(K).

The matrix-curve lemma supplies a value M(t)=εI+NM(t)=\varepsilon I+N with N≠0N\ne0 and N2=0N^2=0, the latter equality following from Cayley–Hamilton. Its projective class is [I+εN][I+\varepsilon N], a nonidentity unipotent. All nonidentity unipotents are conjugate over KK, so they also belong to the image. The conjugators can be taken in SL⁡2(K)\operatorname{SL}_2(K): multiply a GL⁡2(K)\operatorname{GL}_2(K) conjugator by a scalar with the appropriate square to make its determinant one. Finally, v(1,1)=1v(1,1)=1. These cases exhaust PSL⁡2(K)\operatorname{PSL}_2(K) and prove the complex theorem. □\square

The real trace identity

The real construction substitutes conjugate inputs into the shorter word

w0=[a[a,b]a−1, b[b,a]b−1],W=w0(a,bab−1).w_0=[a[a,b]a^{-1},\,b[b,a]b^{-1}],\qquad W=w_0(a,bab^{-1}).

This forces the two inputs of w0w_0 to have the same trace, and real conjugacy imposes an additional restriction that makes the bound possible.

Trace identity. Let A,C∈SL⁡2(R)A,C\in\operatorname{SL}_2(\mathbb R) have common trace xx. Put U=x2U=x^2 and p=tr⁡(AC)p=\operatorname{tr}(AC). Then

tr⁡w0(A,C)=P(U,p),P(U,p)=2+U(p−2)2(p−1)2(U−p−2)3H(U,p),H(U,p)=U2(p−1)2−Up(p2−2)+p2.\begin{aligned} \operatorname{tr}w_0(A,C)&=P(U,p),\\ P(U,p)&=2+U(p-2)^2(p-1)^2(U-p-2)^3H(U,p),\\ H(U,p)&=U^2(p-1)^2-Up(p^2-2)+p^2. \end{aligned}

Here is a derivation, so the large factored polynomial can be checked from smaller identities. Write

c=[A,C],D=A−1C,u=AcA−1,v=Cc−1C−1,c=[A,C],\qquad D=A^{-1}C,\qquad u=AcA^{-1},\qquad v=Cc^{-1}C^{-1},

and set

h=tr⁡c,d=tr⁡D,j=tr⁡(cD),s=tr⁡(uv).h=\operatorname{tr}c,\quad d=\operatorname{tr}D,\quad j=\operatorname{tr}(cD),\quad s=\operatorname{tr}(uv).

The skein and Fricke identities are

tr⁡(XY)+tr⁡(XY−1)=tr⁡Xtr⁡Y,tr⁡[X,Y]=α2+β2+γ2−αβγ−2,\begin{aligned} \operatorname{tr}(XY)+\operatorname{tr}(XY^{-1}) &=\operatorname{tr}X\operatorname{tr}Y,\\ \operatorname{tr}[X,Y] &=\alpha^2+\beta^2+\gamma^2-\alpha\beta\gamma-2, \end{aligned}

where α=tr⁡X\alpha=\operatorname{tr}X, β=tr⁡Y\beta=\operatorname{tr}Y and γ=tr⁡(XY)\gamma=\operatorname{tr}(XY). They give

h=p2−Up+2U−2,d=U−p,j=U−p(h−1),s=h2+d2+j2−hdj−2,tr⁡[u,v]−2=(s−2)(s+2−h2).\begin{aligned} h&=p^2-Up+2U-2,\\ d&=U-p,\\ j&=U-p(h-1),\\ s&=h^2+d^2+j^2-hdj-2,\\ \operatorname{tr}[u,v]-2&=(s-2)(s+2-h^2). \end{aligned}

For the formula for jj, the identity c−1AC=CAc^{-1}AC=CA first gives tr⁡(cAC)=p(h−1)\operatorname{tr}(cAC)=p(h-1). Apply the skein identity to ACA−1ACA^{-1} and C−1A−1CC^{-1}A^{-1}C: their product is cDcD, and the product of the first with the inverse of the second is cACcAC. Also uvuv is conjugate to [c,D][c,D], which gives the formula for ss. Expansion now yields

s−2=U(p−2)(p−1)2(U−p−2)2,s+2−h2=(p−2)(U−p−2)H(U,p).\begin{aligned} s-2&=U(p-2)(p-1)^2(U-p-2)^2,\\ s+2-h^2&=(p-2)(U-p-2)H(U,p). \end{aligned}

Multiplying proves the trace identity.

The restriction imposed by real conjugacy

For C=BAB−1C=BAB^{-1}, the parameters satisfy

U≥0,p≤U−2orU>4.U\ge0,\qquad p\le U-2\quad\text{or}\quad U>4.

To prove this, put q=tr⁡[A,B]−2q=\operatorname{tr}[A,B]-2. The skein identity gives p=U−2−qp=U-2-q, so it suffices to show q≥0q\ge0 when U≤4U\le4. Write

A=(abcd),AB−BA=(kml−k),δ=a−d.A=\begin{pmatrix}a&b\\c&d\end{pmatrix},\qquad AB-BA=\begin{pmatrix}k&m\\l&-k\end{pmatrix},\qquad \delta=a-d.

The determinant and trace identities give

q=k2+ml,δk+bl+cm=0,δ2+4bc=U−4.q=k^2+ml,\qquad \delta k+bl+cm=0,\qquad \delta^2+4bc=U-4.

Consequently,

4b2q=(2bk−δm)2−(U−4)m2≥0.4b^2q=(2bk-\delta m)^2-(U-4)m^2\ge0.

If b≠0b\ne0, this proves the claim. If b=0b=0, then δ2=U−4≤0\delta^2=U-4\le0, so δ=0\delta=0. The upper-right entry of AB−BAAB-BA is then zero, giving q=k2≥0q=k^2\ge0. The boundary and degenerate cases are therefore included.

A uniform lower bound

Apply the trace identity to A,C=BAB−1A,C=BAB^{-1}. First suppose p≤U−2p\le U-2. If p<−2p<-2, each term in the defining expression for HH is nonnegative and p2>0p^2>0. Otherwise, put r=U−p−2≥0r=U-p-2\ge0. Substitution gives

H=(p−1)2r2+(p3−4p+4)r+4>0.H=(p-1)^2r^2+(p^3-4p+4)r+4>0.

Indeed, p3−4p=p(p−2)(p+2)≥0p^3-4p=p(p-2)(p+2)\ge0 on [−2,0]∪[2,∞)[-2,0]\cup[2,\infty), while on [0,2][0,2],

p3−4p+4=(p−1)2(p+2)+2−p>0.p^3-4p+4=(p-1)^2(p+2)+2-p>0.

Thus the factored trace gives P≥2P\ge2 throughout this region.

The remaining region has U>4U>4 and p>U−2p>U-2. Set

t=p−2>0,e=p−U+2,0<e<t,D=4t2+7t+4.t=p-2>0,\qquad e=p-U+2,\qquad 0<e<t,\qquad D=4t^2+7t+4.

Then U=t+4−eU=t+4-e, and

P=2−(t+4−e)t2(t+1)2e3H,H=4−(t3+6t2+8t+4)e+(t+1)2e2.\begin{aligned} P&=2-(t+4-e)t^2(t+1)^2e^3H,\\ H&=4-(t^3+6t^2+8t+4)e+(t+1)^2e^2. \end{aligned}

The identity

(4−De)−H=e(t−e)(t+1)2>0(4-De)-H=e(t-e)(t+1)^2>0

gives H≤4−DeH\le4-De. If H≤0H\le0, again P≥2P\ge2. If H>0H>0, then 4−De>04-De>0, and the exact inequality

27−D3e3(4−De)=(De−3)2((De+1)2+2)≥027-D^3e^3(4-De) =(De-3)^2\bigl((De+1)^2+2\bigr)\ge0

yields

2−P≤27(t+4)t2(t+1)2D3<14.2-P\le\frac{27(t+4)t^2(t+1)^2}{D^3}<\frac14.

For the strict final inequality, expand the difference:

D3−108(t+4)t2(t+1)2=64t6+228t5+132t4+43t3+348t2+336t+64>0.\begin{aligned} D^3-108(t+4)t^2(t+1)^2 ={}&64t^6+228t^5+132t^4+43t^3\\ &+348t^2+336t+64>0. \end{aligned}

Every coefficient is positive. The two regions cover all real inputs, proving tr⁡W(A,B)>7/4\operatorname{tr}W(A,B)>7/4 universally.

The word is nonidentity and omits involutions

One exact evaluation certifies that WW is a nonidentity free-group word. Take

A=(1101),B=(1021).A=\begin{pmatrix}1&1\\0&1\end{pmatrix},\qquad B=\begin{pmatrix}1&0\\2&1\end{pmatrix}.

Here U=4U=4 and p=−2p=-2, so

tr⁡W(A,B)=P(4,−2)=6045698≠2.\operatorname{tr}W(A,B)=P(4,-2)=6045698\ne2.

This single calculation proves nonidentity; the preceding symbolic inequalities establish the bound for every pair.

Now let X∈SL⁡2(R)X\in\operatorname{SL}_2(\mathbb R) lift a nonidentity involution in the projective group. Then X2=±IX^2=\pm I. The case X2=IX^2=I forces X=±IX=\pm I: its minimal polynomial has distinct roots among 1,−11,-1, and determinant one excludes a pair of opposite eigenvalues. This would make the projective class the identity. Hence X2=−IX^2=-I, and Cayley–Hamilton gives tr⁡X=0\operatorname{tr}X=0.

Every pair of projective inputs has special-linear lifts. If its WW-value were a nonidentity involution, the matrix word evaluated on those lifts would therefore have trace zero, contradicting the strict bound. For example, the class of

J=(0−110)J=\begin{pmatrix}0&-1\\1&0\end{pmatrix}

is omitted. This proves the real theorem. □\square

Credit and the formal record

Bandman–Zarhin proved earlier complex surjectivity results [5]; the all-word question is stated explicitly by Gordeev–Plotkin [6, Problem 0.1]. The complex argument above uses the specialization of Schneider–Thom and the scalar polynomial observation of Mushkarov–Nikolov. Differentiating the determinant connects a simple root to a nonidentity projective unipotent.

For the real group, Gordeev–Kunyavskii–Plotkin discuss the surjectivity question and prove that every nonidentity word attains all split semisimple elements. They also show that attaining an involution would imply that every semisimple element is attained [7, Question 2.5 and Proposition 2.6]. The explicit word WW and its trace bound give the obstruction here. Thom's compact result supplies the third answer to Problem 16.68.

The solution and formalization are by Nilradical v1.0.0, using Lean and mathlib. Both the real and complex results have complete proofs with the standard free-group and projective special linear group definitions. The complex endpoint proves WordMaps.word_surjective for every algebraically closed field of characteristic zero and specializes it in WordMaps.complex_word_surjective. The real endpoint proves RealWord.word_ne_one, RealWord.tr_value_gt_seven_fourths, RealWord.word_not_surjective and RealWord.exists_nontrivial_nonsurjective_word.

The real formal proof explicitly omits the displayed class of JJ. Omission of every nonidentity involution is the consequence of the trace bound proved above; it is not a separately exported endpoint. The compact case is attributed to Thom and is not formalized in these projects. The formalization guide and verification record identify the sources and their verification evidence. The frozen developments passed independent statement comparison, proof replay and external kernel checking.

References

  1. E. I. Khukhro and V. D. Mazurov (eds.), The Kourovka Notebook, 21st ed., September 2026 update, Problem 16.68 (J. Mycielski), p. 102. Editors' text.

  2. J. Schneider and A. Thom, Word images in symmetric and unitary groups are dense, arXiv:1802.09289v1, Lemma 1. Published, with revised title, in Pacific J. Math. 311 (2021), 475–504. Original preprint.

  3. O. Mushkarov and N. Nikolov, A Picard little theorem for entire functions of matrices, Elem. Math. 81 (2026), 34–39, Example 1(iii). DOI.

  4. A. Thom, Convergent sequences in discrete groups, Canad. Math. Bull. 56 (2013), 424–433, Corollary 1.2. Author version.

  5. T. Bandman and Yu. G. Zarhin, Surjectivity of certain word maps on PSL⁡(2,C)\operatorname{PSL}(2,\mathbb C) and SL⁡(2,C)\operatorname{SL}(2,\mathbb C), Eur. J. Math. 2 (2016), 614–643. Author version.

  6. N. Gordeev and E. Plotkin, The group SL⁡2(C)\operatorname{SL}_2(\mathbb C): Word maps and related topics (2026), Problem 0.1. DOI.

  7. N. Gordeev, B. Kunyavskii and E. Plotkin, Geometry of word equations in simple algebraic groups over special fields, Russian Math. Surveys 73 (2018), 753–796, Question 2.5 and Proposition 2.6. Author version.