Linearity of Sapir's group

AbbreviationSapir's group#✓fully proved

Sapir's group is the group with presentation \(\langle a, b, t \mid a^t = ab, b^t = ba \rangle\), where \(a^t = t^{-1} a t\): the quotient of the free group on \(a\), \(b\), \(t\) by the normal subgroup generated by \(t^{-1} a t (ab)^{-1}\) and \(t^{-1} b t (ba)^{-1}\).

abbrev SapirGroup : Type :=
  PresentedGroup ({(FreeGroup.of 2)⁻¹ * FreeGroup.of 0 * FreeGroup.of 2 *
      (FreeGroup.of 0 * FreeGroup.of 1)⁻¹,
    (FreeGroup.of 2)⁻¹ * FreeGroup.of 1 * FreeGroup.of 2 * (FreeGroup.of 1 * FreeGroup.of 0)⁻¹} :
      Set (FreeGroup (Fin 3)))

Used by 1

Used byLinearity of Sapir's group over the integers (Kourovka 17.108)

DefinitionLinearity of Sapir's group over the integers (Kourovka 17.108)#✓fully proved

The statement that the group \(\langle a, b, t \mid a^t = ab, b^t = ba \rangle\), where \(a^t = t^{-1} a t\), embeds in \(\mathrm{GL}_n(\mathbb{Z})\) for some natural number \(n\), that is, that it is linear over \(\mathbb{Z}\).

This is the form of the Kourovka Archive's resolution of M. Sapir's question whether the group is linear.

def sapirGroupIntegerLinear : Prop :=
  ∃ n : ℕ, ∃ f : SapirGroup →* Matrix.GeneralLinearGroup (Fin n) ℤ, Function.Injective f

Uses 1 · Used by 1

Statement usesSapir's group

Used bySapir's group is linear over the integers

TheoremSapir's group is linear over the integers#●ready to prove

The group \(\langle a, b, t \mid a^t = ab, b^t = ba \rangle\), where \(a^t = t^{-1} a t\), embeds in \(\mathrm{GL}_n(\mathbb{Z})\) for some natural number \(n\). That is, Kourovka Problem 17.108 has a positive answer.

The Kourovka Archive answers 17.108 "Yes, this group is linear" (M. F. Hagen, letter of 6 August 2018): the group is the mapping torus of an irreducible atoroidal self-monomorphism of a free group, so it is virtually special and hence \(\mathbb{Z}\)-linear by Theorem B of Hagen and Wise (2016).

public theorem_wanted sapirGroupIntegerLinear_holds : sapirGroupIntegerLinear

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 17.108 (M. Sapir); resolution: M. F. Hagen, letter of 6 August 2018, as recorded in the Kourovka Archive; M. F. Hagen and D. T. Wise, Duke Math. J. 165 (2016), 1753-1813, Kourovka Archive, Problem 17.108 (Yes, this group is linear: as noticed by M. Sapir it is the mapping torus of an irreducible atoroidal self-monomorphism of a free group, hence virtually special, hence Z-linear by Theorem B of Hagen-Wise).

Uses 1

Statement usesLinearity of Sapir's group over the integers (Kourovka 17.108)

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.