Linearity of one-relator groups

DefinitionThe relator of Kourovka Problem 18.86#✓fully proved

This is the element \([[a, b], b]\) of the free group on two generators \(a\) and \(b\), where \([x, y] = x^{-1} y^{-1} x y\); explicitly, \([[a, b], b] = c^{-1} b^{-1} c b\) with \(c = a^{-1} b^{-1} a b\).

def relator : FreeGroup (Fin 2) :=
  let a := FreeGroup.of (0 : Fin 2)
  let b := FreeGroup.of (1 : Fin 2)
  let c := a⁻¹ * b⁻¹ * a * b
  c⁻¹ * b⁻¹ * c * b

Used by 2

Used byThe one-relator group of Kourovka Problem 18.86 · Kourovka Problem 18.86 (statement)

AbbreviationThe one-relator group of Kourovka Problem 18.86#✓fully proved

This is the group \(G = \langle a, b \mid [[a, b], b] = 1 \rangle\) with generators \(a, b\) and the single defining relation \([[a, b], b] = 1\), where \([x, y] = x^{-1} y^{-1} x y\); that is, \(G\) is the quotient of the free group on \(a\) and \(b\) by the normal subgroup generated by \([[a, b], b]\).

abbrev OneRelatorGroup : Type := PresentedGroup ({relator} : Set (FreeGroup (Fin 2)))

def relator : FreeGroup (Fin 2) :=
  let a := FreeGroup.of (0 : Fin 2)
  let b := FreeGroup.of (1 : Fin 2)
  let c := a⁻¹ * b⁻¹ * a * b
  c⁻¹ * b⁻¹ * c * b

WantedExt/GroupTheory/UnitriangularOneRelatorLinearKourovka18Problem86Wanted.lean:38

Uses 1 · Used by 1

Statement usesThe relator of Kourovka Problem 18.86

Used byKourovka Problem 18.86 (statement)

DefinitionKourovka Problem 18.86 (statement)#✓fully proved

The statement that the group \(G\) with generators \(a, b\) and the single defining relation \([[a, b], b] = 1\), where \([x, y] = x^{-1} y^{-1} x y\), is linear: there are a field \(K\), a natural number \(n\) and an injective group homomorphism \(G \to \mathrm{GL}_n(K)\).

def oneRelatorGroupIsLinear : Prop :=
  ∃ (K : Type) (_ : Field K) (n : ℕ) (ρ : OneRelatorGroup →* Matrix.GeneralLinearGroup (Fin n) K),
    Function.Injective ρ

Uses 2 · Used by 1

Statement usesThe one-relator group of Kourovka Problem 18.86 · The relator of Kourovka Problem 18.86

Used byThe one-relator group of Kourovka Problem 18.86 is linear

TheoremThe one-relator group of Kourovka Problem 18.86 is linear#●ready to prove

Let \(G\) be the group with generators \(a, b\) and the single defining relation \([[a, b], b] = 1\), where \([x, y] = x^{-1} y^{-1} x y\). Then \(G\) is linear: there are a field \(K\), a natural number \(n\) and an injective group homomorphism \(G \to \mathrm{GL}_n(K)\).

public theorem_wanted oneRelatorGroupIsLinear_holds : oneRelatorGroupIsLinear

def oneRelatorGroupIsLinear : Prop :=
  ∃ (K : Type) (_ : Field K) (n : ℕ) (ρ : OneRelatorGroup →* Matrix.GeneralLinearGroup (Fin n) K),
    Function.Injective ρ

WantedExt/GroupTheory/UnitriangularOneRelatorLinearKourovka18Problem86Wanted.lean:49

Sources

E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Archive of Solved Problems, Problem 18.86 (V. A. Roman'kov); resolution: V. G. Bardakov and O. V. Bryukhanov, Vestnik Novosibirsk Univ. Ser. Mat. Mekh. Inf. 7 (2007), no. 3, 45-58 (Russian); V. A. Roman'kov, J. Siberian Federal Univ. Math. Phys. 6 (2013), no. 4, 516-520, Kourovka Archive, Problem 18.86: Yes, it is linear, since it embeds in Hol F_2 (adding c = [a, b] gives G = ⟨a, b, c | a^b = ac, c^b = c⟩), and Hol F_2 is linear by Corollary 3 of Bardakov-Bryukhanov; another proof by Roman'kov, https://arxiv.org/abs/1401.0300v49.

Uses 1

Statement usesKourovka Problem 18.86 (statement)

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.