Word maps on Lie groups

DefinitionMycielski's trace-range property for \(\mathrm{GL}(2, \mathbb{R})\) (Kourovka 16.69(a))#✓fully proved

For every nontrivial element \(w\) of the free group on two generators \(x, y\), the set of traces \(\operatorname{tr} w(A, B)\), where \(A, B\) range over \(\mathrm{GL}(2, \mathbb{R})\) and \(w(A, B)\) is obtained by substituting \(A\) for \(x\) and \(B\) for \(y\), contains the interval \([-2, \infty)\).

def gl2TraceRangeContainsRay : Prop :=
  ∀ w : FreeGroup (Fin 2), w ≠ 1 →
    Set.Ici (-2 : ℝ) ⊆ Set.range fun xy : Matrix.GeneralLinearGroup (Fin 2) ℝ ×
        Matrix.GeneralLinearGroup (Fin 2) ℝ =>
      Matrix.trace (FreeGroup.lift ![xy.1, xy.2] w : Matrix (Fin 2) (Fin 2) ℝ)
Used by 1

DefinitionMycielski's real-part property for quaternion word maps (Kourovka 16.69(b))#✓fully proved

For every nontrivial element \(w\) of the free group on two generators \(x, y\), the set of real parts \(\operatorname{Re} w(p, q)\), where \(p, q\) range over the nonzero real quaternions and \(w(p, q)\) is obtained by substituting \(p\) for \(x\) and \(q\) for \(y\), contains the interval \([-5/27, 1]\).

def quaternionRealPartRangeContainsInterval : Prop :=
  ∀ w : FreeGroup (Fin 2), w ≠ 1 →
    Set.Icc (-5 / 27 : ℝ) 1 ⊆ Set.range fun xy : (Quaternion ℝ)ˣ × (Quaternion ℝ)ˣ =>
      (FreeGroup.lift ![xy.1, xy.2] w : Quaternion ℝ).re
Used by 1

TheoremMycielski's trace-range question for \(\mathrm{GL}(2, \mathbb{R})\) has a negative answer#●ready to prove

There is a nontrivial element \(w\) of the free group on two generators \(x, y\) such that some real number \(t \ge -2\) is not the trace of \(w(A, B)\) for any \(A, B \in \mathrm{GL}(2, \mathbb{R})\), where \(w(A, B)\) is obtained by substituting \(A\) for \(x\) and \(B\) for \(y\).

Resolved false: the Kourovka Notebook (21st issue) answers 16.69(a), posed for x, y ∈ GL(2, ℝ), "No, it need not" (AI solution confirmed by A. Thom), citing the Nilradical note, whose Theorem 2 gives an explicit word W ≠ 1 with tr W(A, B) > 7/4 for all A, B ∈ SL(2, ℝ). Source: E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 16.69 (J. Mycielski); resolution: Nilradical v1.0.0, Word maps on PSL2: real and complex cases, result notes (21 September 2026); A. Thom, Convergent sequences in discrete groups, Canad. Math. Bull. 56 (2013), 424-433, (a) Nilradical, Theorem 2 (an explicit W ≠ 1 with tr W(A, B) > 7/4 for all A, B ∈ SL_2(ℝ)); (b) Thom, Corollary 1.2 (for every n and ε > 0 a word w ≠ 1 with ‖1 - w(u, v)‖ ≤ ε for all u, v ∈ U(n)); the Kourovka Notebook (21st issue) marks 16.69 solved (a: No, AI solution confirmed by A. Thom; b: No, Thom 2013), https://kourovkanotebookorg.wordpress.com/wp-content/uploads/2026/09/nilradical-kourovka-16-68-69.pdf.

public theorem_wanted gl2TraceRangeContainsRay_refuted : ¬ gl2TraceRangeContainsRay
Uses 1

TheoremMycielski's real-part question for quaternion word maps has a negative answer#●ready to prove

There is a nontrivial element \(w\) of the free group on two generators \(x, y\) such that some real number \(t\) with \(-5/27 \le t \le 1\) is not the real part of \(w(p, q)\) for any nonzero real quaternions \(p, q\), where \(w(p, q)\) is obtained by substituting \(p\) for \(x\) and \(q\) for \(y\).

Resolved false: the Kourovka Notebook (21st issue) answers 16.69(b) "No, it need not", citing Thom (2013), whose Corollary 1.2 gives, for every n and ε > 0, a word w ≠ 1 with ‖1 - w(u, v)‖ ≤ ε for all u, v ∈ U(n). Source: E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 16.69 (J. Mycielski); resolution: Nilradical v1.0.0, Word maps on PSL2: real and complex cases, result notes (21 September 2026); A. Thom, Convergent sequences in discrete groups, Canad. Math. Bull. 56 (2013), 424-433, (a) Nilradical, Theorem 2 (an explicit W ≠ 1 with tr W(A, B) > 7/4 for all A, B ∈ SL_2(ℝ)); (b) Thom, Corollary 1.2 (for every n and ε > 0 a word w ≠ 1 with ‖1 - w(u, v)‖ ≤ ε for all u, v ∈ U(n)); the Kourovka Notebook (21st issue) marks 16.69 solved (a: No, AI solution confirmed by A. Thom; b: No, Thom 2013), https://kourovkanotebookorg.wordpress.com/wp-content/uploads/2026/09/nilradical-kourovka-16-68-69.pdf.

public theorem_wanted quaternionRealPartRangeContainsInterval_refuted :
    ¬ quaternionRealPartRangeContainsInterval
Uses 1

DefinitionWord map#✓fully proved

For a group \(G\) and an element \(w\) of the free group \(F_2\) on two generators \(x_0, x_1\), the word map of \(w\) is the map \(G \times G \to G\) sending \((x, y)\) to \(w(x, y)\), the image of \(w\) under the group homomorphism \(F_2 \to G\) with \(x_0 \mapsto x\) and \(x_1 \mapsto y\).

def wordMap (G : Type*) [Group G] (w : FreeGroup (Fin 2)) (xy : G × G) : G :=
  FreeGroup.lift ![xy.1, xy.2] w
Used by 3

DefinitionSurjectivity of word maps on \(\mathrm{PSL}(2, \mathbb{R})\) (Kourovka 16.68(a))#✓fully proved

The statement, asked about by J. Mycielski, that for every nontrivial element \(w\) of the free group \(F_2\) on two generators, the word map \(\mathrm{PSL}(2, \mathbb{R}) \times \mathrm{PSL}(2, \mathbb{R}) \to \mathrm{PSL}(2, \mathbb{R})\), \((x, y) \mapsto w(x, y)\), is surjective.

def psl2RealWordMapsSurjective : Prop :=
  ∀ w : FreeGroup (Fin 2), w ≠ 1 →
    Function.Surjective (wordMap (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) w)
Uses 1 · Used by 1

DefinitionSurjectivity of word maps on \(\mathrm{PSL}(2, \mathbb{C})\) (Kourovka 16.68(b))#✓fully proved

The statement, asked about by J. Mycielski, that for every nontrivial element \(w\) of the free group \(F_2\) on two generators, the word map \(\mathrm{PSL}(2, \mathbb{C}) \times \mathrm{PSL}(2, \mathbb{C}) \to \mathrm{PSL}(2, \mathbb{C})\), \((x, y) \mapsto w(x, y)\), is surjective.

def psl2ComplexWordMapsSurjective : Prop :=
  ∀ w : FreeGroup (Fin 2), w ≠ 1 →
    Function.Surjective (wordMap (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℂ) w)
Uses 1 · Used by 1

DefinitionSurjectivity of word maps on \(\mathrm{SO}(3, \mathbb{R})\) (Kourovka 16.68(c))#✓fully proved

The statement, asked about by J. Mycielski, that for every nontrivial element \(w\) of the free group \(F_2\) on two generators, the word map \(\mathrm{SO}(3, \mathbb{R}) \times \mathrm{SO}(3, \mathbb{R}) \to \mathrm{SO}(3, \mathbb{R})\), \((x, y) \mapsto w(x, y)\), is surjective.

def so3WordMapsSurjective : Prop :=
  ∀ w : FreeGroup (Fin 2), w ≠ 1 →
    Function.Surjective (wordMap (Matrix.specialOrthogonalGroup (Fin 3) ℝ) w)
Uses 1 · Used by 1

TheoremSome nontrivial word map on \(\mathrm{PSL}(2, \mathbb{R})\) is not surjective (Kourovka 16.68(a))#●ready to prove

There is a nontrivial element \(w\) of the free group \(F_2\) on two generators whose word map \(\mathrm{PSL}(2, \mathbb{R}) \times \mathrm{PSL}(2, \mathbb{R}) \to \mathrm{PSL}(2, \mathbb{R})\), \((x, y) \mapsto w(x, y)\), is not surjective. That is, Mycielski's question has a negative answer for \(\mathrm{PSL}(2, \mathbb{R})\).

Nilradical (Theorem 2) gives an explicit nontrivial word \(W\) (cyclically reduced length 44) with \(\operatorname{tr} W(A, B) > 7/4\) for all \(A, B \in \mathrm{SL}(2, \mathbb{R})\); a nonidentity involution of \(\mathrm{PSL}(2, \mathbb{R})\) lifts to a matrix of trace \(0\), so the word map of \(W\) misses it. The Kourovka Notebook (21st issue) records the negative answer for \(\mathrm{PSL}(2, \mathbb{R})\) (AI solution confirmed by A. Thom).

public theorem_wanted psl2RealWordMapsSurjective_refuted : ¬ psl2RealWordMapsSurjective
Sources
  • E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 16.68 (J. Mycielski); resolution: Nilradical v1.0.0, Word maps on PSL2: real and complex cases, result notes (21 September 2026); A. Thom, Convergent sequences in discrete groups, Canad. Math. Bull. 56 (2013), 424-433, Nilradical, Theorem 1 (every w ≠ 1 in F_2 induces a surjective map PSL_2(K)² → PSL_2(K) for K algebraically closed of characteristic 0) and Theorem 2 (an explicit W ≠ 1 with tr W(A, B) > 7/4 for all A, B ∈ SL_2(ℝ)); Thom, Corollary 1.2 (for every n and ε > 0 a word w ≠ 1 with ‖1 - w(u, v)‖ ≤ ε for all u, v ∈ U(n)), for SO(3, ℝ); the Kourovka Notebook (21st issue) marks 16.68 solved (AI solution confirmed by A. Thom; SO(3, ℝ) from Thom 2013), https://kourovkanotebookorg.wordpress.com/wp-content/uploads/2026/09/nilradical-kourovka-16-68-69.pdf.
Uses 1

TheoremNontrivial word maps on \(\mathrm{PSL}(2, \mathbb{C})\) are surjective (Kourovka 16.68(b))#●ready to prove

For every nontrivial element \(w\) of the free group \(F_2\) on two generators, the word map \(\mathrm{PSL}(2, \mathbb{C}) \times \mathrm{PSL}(2, \mathbb{C}) \to \mathrm{PSL}(2, \mathbb{C})\), \((x, y) \mapsto w(x, y)\), is surjective. That is, Mycielski's question has an affirmative answer for \(\mathrm{PSL}(2, \mathbb{C})\).

Nilradical (Theorem 1) proves that for every algebraically closed field \(K\) of characteristic zero, in particular \(\mathbb{C}\), every nontrivial word \(w \in F_2\) induces a surjective map \(\mathrm{PSL}(2, K)^2 \to \mathrm{PSL}(2, K)\); the Kourovka Notebook (21st issue) records the affirmative answer for \(\mathrm{PSL}(2, \mathbb{C})\) (AI solution confirmed by A. Thom).

public theorem_wanted psl2ComplexWordMapsSurjective_holds : psl2ComplexWordMapsSurjective
Sources
  • E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 16.68 (J. Mycielski); resolution: Nilradical v1.0.0, Word maps on PSL2: real and complex cases, result notes (21 September 2026); A. Thom, Convergent sequences in discrete groups, Canad. Math. Bull. 56 (2013), 424-433, Nilradical, Theorem 1 (every w ≠ 1 in F_2 induces a surjective map PSL_2(K)² → PSL_2(K) for K algebraically closed of characteristic 0) and Theorem 2 (an explicit W ≠ 1 with tr W(A, B) > 7/4 for all A, B ∈ SL_2(ℝ)); Thom, Corollary 1.2 (for every n and ε > 0 a word w ≠ 1 with ‖1 - w(u, v)‖ ≤ ε for all u, v ∈ U(n)), for SO(3, ℝ); the Kourovka Notebook (21st issue) marks 16.68 solved (AI solution confirmed by A. Thom; SO(3, ℝ) from Thom 2013), https://kourovkanotebookorg.wordpress.com/wp-content/uploads/2026/09/nilradical-kourovka-16-68-69.pdf.
Uses 1

TheoremSome nontrivial word map on \(\mathrm{SO}(3, \mathbb{R})\) is not surjective (Kourovka 16.68(c))#●ready to prove

There is a nontrivial element \(w\) of the free group \(F_2\) on two generators whose word map \(\mathrm{SO}(3, \mathbb{R}) \times \mathrm{SO}(3, \mathbb{R}) \to \mathrm{SO}(3, \mathbb{R})\), \((x, y) \mapsto w(x, y)\), is not surjective. That is, Mycielski's question has a negative answer for \(\mathrm{SO}(3, \mathbb{R})\).

The Kourovka Notebook (21st issue) answers 16.68 negatively for \(\mathrm{SO}(3, \mathbb{R})\), noting that this follows from Thom (2013), whose Corollary 1.2 gives, for every \(\varepsilon > 0\), a nontrivial word \(w\) with \(\|1 - w(u, v)\| \le \varepsilon\) for all unitary \(u, v\), in particular for all \(u, v \in \mathrm{SO}(3, \mathbb{R})\).

public theorem_wanted so3WordMapsSurjective_refuted : ¬ so3WordMapsSurjective
Sources
  • E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 16.68 (J. Mycielski); resolution: Nilradical v1.0.0, Word maps on PSL2: real and complex cases, result notes (21 September 2026); A. Thom, Convergent sequences in discrete groups, Canad. Math. Bull. 56 (2013), 424-433, Nilradical, Theorem 1 (every w ≠ 1 in F_2 induces a surjective map PSL_2(K)² → PSL_2(K) for K algebraically closed of characteristic 0) and Theorem 2 (an explicit W ≠ 1 with tr W(A, B) > 7/4 for all A, B ∈ SL_2(ℝ)); Thom, Corollary 1.2 (for every n and ε > 0 a word w ≠ 1 with ‖1 - w(u, v)‖ ≤ ε for all u, v ∈ U(n)), for SO(3, ℝ); the Kourovka Notebook (21st issue) marks 16.68 solved (AI solution confirmed by A. Thom; SO(3, ℝ) from Thom 2013), https://kourovkanotebookorg.wordpress.com/wp-content/uploads/2026/09/nilradical-kourovka-16-68-69.pdf.
Uses 1
6 fully proved5 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.