Kaplansky's unit conjecture

InductiveGenerators of Gardam's presentation#✓fully proved

This is the two-element set consisting of the distinct formal symbols \(a\) and \(b\), which serve as the generators of the group presentation in Theorem A of Gardam's counterexample to the unit conjecture.

inductive generators where
  | a
  | b

Used by 13

Used byFirst free generator of Gardam's presentation · Second free generator of Gardam's presentation · Gardam's group · Gardam's element p · Gardam's element q · Gardam's element r · Relators of Gardam's group · Gardam's element s · Gardam's counterexample to the unit conjecture · Gardam's unit · The element x of Gardam's group · The element y of Gardam's group · The element z of Gardam's group

DefinitionFirst free generator of Gardam's presentation#✓fully proved

\(a\) is the generator \(a\), viewed as an element of the free group on the two generators \(a\) and \(b\).

def a : FreeGroup generators := .of generators.a

Uses 1 · Used by 4

Statement usesGenerators of Gardam's presentation

Used byRelators of Gardam's group · Gardam's unit · The element x of Gardam's group · The element z of Gardam's group

DefinitionSecond free generator of Gardam's presentation#✓fully proved

\(b\) is the generator \(b\), viewed as an element of the free group on the two generators \(a\) and \(b\).

def b : FreeGroup generators := .of generators.b

Uses 1 · Used by 4

Statement usesGenerators of Gardam's presentation

Used byRelators of Gardam's group · Gardam's unit · The element y of Gardam's group · The element z of Gardam's group

DefinitionRelators of Gardam's group#✓fully proved

In the free group on the generators \(a\) and \(b\), the relators are the two elements \(b^{-1}a^2ba^2\) and \(a^{-1}b^2ab^2\).

Imposing them gives the relations \(b^{-1}a^2b = a^{-2}\) and \(a^{-1}b^2a = b^{-2}\) of Theorem A of Gardam's counterexample to the unit conjecture.

def relations : Set (FreeGroup generators) :=
  {b⁻¹ * a ^ 2 * b * a ^ 2, a⁻¹ * b ^ 2 * a * b ^ 2}

Uses 3 · Used by 10

Statement usesFirst free generator of Gardam's presentation · Second free generator of Gardam's presentation · Generators of Gardam's presentation

Used byGardam's group · Gardam's element p · Gardam's element q · Gardam's element r · Gardam's element s · Gardam's counterexample to the unit conjecture · Gardam's unit · The element x of Gardam's group · The element y of Gardam's group · The element z of Gardam's group

DefinitionGardam's group#✓fully proved

\(P\) is the group with generators \(a\) and \(b\) and relators \(b^{-1}a^2ba^2\) and \(a^{-1}b^2ab^2\), that is, \(P = \langle a, b \mid b^{-1}a^2b = a^{-2}, a^{-1}b^2a = b^{-2} \rangle\).

This is the group of Theorem A of Gardam's counterexample to the unit conjecture.

def P := PresentedGroup relations
deriving Coe (FreeGroup generators), Group

Uses 2 · Used by 10

Statement usesGenerators of Gardam's presentation · Relators of Gardam's group

Used byGardam's element p · Gardam's element q · Group ring of Gardam's group over the field with two elements · Gardam's element r · Gardam's element s · Gardam's counterexample to the unit conjecture · Gardam's unit · The element x of Gardam's group · The element y of Gardam's group · The element z of Gardam's group

DefinitionThe element x of Gardam's group#✓fully proved

In the group \(P\) with presentation \(\langle a, b \mid b^{-1}a^2b = a^{-2},\ a^{-1}b^2a = b^{-2} \rangle\), \(x = a^2\).

def x : P := a ^ 2

Uses 4 · Used by 4

Statement usesGardam's group · First free generator of Gardam's presentation · Generators of Gardam's presentation · Relators of Gardam's group

Used byGardam's element p · Gardam's element q · Gardam's element r · Gardam's element s

DefinitionThe element y of Gardam's group#✓fully proved

In the group \(P\) with presentation \(\langle a, b \mid b^{-1}a^2b = a^{-2},\ a^{-1}b^2a = b^{-2} \rangle\), \(y = b^2\).

def y : P := b ^ 2

Uses 4 · Used by 4

Statement usesGardam's group · Second free generator of Gardam's presentation · Generators of Gardam's presentation · Relators of Gardam's group

Used byGardam's element p · Gardam's element q · Gardam's element r · Gardam's element s

DefinitionThe element z of Gardam's group#✓fully proved

In the group \(P\) with presentation \(\langle a, b \mid b^{-1}a^2b = a^{-2},\ a^{-1}b^2a = b^{-2} \rangle\), \(z = (ab)^2\).

def z : P := (a * b) ^ 2

Uses 5 · Used by 4

Statement usesGardam's group · First free generator of Gardam's presentation · Second free generator of Gardam's presentation · Generators of Gardam's presentation · Relators of Gardam's group

Used byGardam's element p · Gardam's element q · Gardam's element r · Gardam's element s

AbbreviationGroup ring of Gardam's group over the field with two elements#✓fully proved

\(\mathbb{F}_2[P]\) is the group ring of Gardam's group \(P\) over the field \(\mathbb{F}_2 = \mathbb{Z}/2\mathbb{Z}\).

abbrev R := MonoidAlgebra (ZMod 2) P

Uses 1 · Used by 6

Statement usesGardam's group

Used byGardam's element p · Gardam's element q · Gardam's element r · Gardam's element s · Gardam's counterexample to the unit conjecture · Gardam's unit

DefinitionGardam's element p#✓fully proved

In the group ring \(\mathbb{F}_2[P]\) of Gardam's group \(P\) with generators \(a\) and \(b\), let \(x = a^2\), \(y = b^2\) and \(z = (ab)^2\) in \(P\), viewed as elements of \(\mathbb{F}_2[P]\). Then \(p\) is the element \((1 + x)(1 + y)(1 + z^{-1})\) of \(\mathbb{F}_2[P]\).

def p : R := (1 + x) * (1 + y) * (1 + z⁻¹)

Uses 7 · Used by 1

Statement usesGardam's group · Group ring of Gardam's group over the field with two elements · Generators of Gardam's presentation · Relators of Gardam's group · The element x of Gardam's group · The element y of Gardam's group · The element z of Gardam's group

Used byGardam's unit

DefinitionGardam's element q#✓fully proved

In the group ring \(\mathbb{F}_2[P]\) of Gardam's group \(P\) with generators \(a\) and \(b\), let \(x = a^2\), \(y = b^2\) and \(z = (ab)^2\) in \(P\), viewed as elements of \(\mathbb{F}_2[P]\). Then \(q\) is the element \(x^{-1}y^{-1} + x + y^{-1}z + z\) of \(\mathbb{F}_2[P]\).

def q : R := x⁻¹ * y⁻¹ + x + y⁻¹ * z + z

Uses 7 · Used by 1

Statement usesGardam's group · Group ring of Gardam's group over the field with two elements · Generators of Gardam's presentation · Relators of Gardam's group · The element x of Gardam's group · The element y of Gardam's group · The element z of Gardam's group

Used byGardam's unit

DefinitionGardam's element r#✓fully proved

In the group ring \(\mathbb{F}_2[P]\) of Gardam's group \(P\) with generators \(a\) and \(b\), let \(x = a^2\), \(y = b^2\) and \(z = (ab)^2\) in \(P\), viewed as elements of \(\mathbb{F}_2[P]\). Then \(r\) is the element \(1 + x + y^{-1}z + xyz\) of \(\mathbb{F}_2[P]\).

def r : R := 1 + x + y⁻¹ * z + x * y * z

Uses 7 · Used by 1

Statement usesGardam's group · Group ring of Gardam's group over the field with two elements · Generators of Gardam's presentation · Relators of Gardam's group · The element x of Gardam's group · The element y of Gardam's group · The element z of Gardam's group

Used byGardam's unit

DefinitionGardam's element s#✓fully proved

In the group ring \(\mathbb{F}_2[P]\) of Gardam's group \(P\) with generators \(a\) and \(b\), let \(x = a^2\), \(y = b^2\) and \(z = (ab)^2\) in \(P\), viewed as elements of \(\mathbb{F}_2[P]\). Then \(s\) is the element \(1 + (x + x^{-1} + y + y^{-1})z^{-1}\) of \(\mathbb{F}_2[P]\).

def s : R := 1 + (x + x⁻¹ + y + y⁻¹) * z⁻¹

Uses 7 · Used by 1

Statement usesGardam's group · Group ring of Gardam's group over the field with two elements · Generators of Gardam's presentation · Relators of Gardam's group · The element x of Gardam's group · The element y of Gardam's group · The element z of Gardam's group

Used byGardam's unit

DefinitionGardam's unit#✓fully proved

Let \(P\) be the group with presentation \(\langle a, b \mid b^{-1}a^2b = a^{-2},\ a^{-1}b^2a = b^{-2} \rangle\) and set \(x = a^2\), \(y = b^2\), \(z = (ab)^2\). In the group ring \(\mathbb{F}_2[P]\), \(u = p + qa + rb + sab\), where \(p = (1 + x)(1 + y)(1 + z^{-1})\), \(q = x^{-1}y^{-1} + x + y^{-1}z + z\), \(r = 1 + x + y^{-1}z + xyz\) and \(s = 1 + (x + x^{-1} + y + y^{-1})z^{-1}\).

def u : R := p + q * a + r * b + s * (a * b)

Uses 10 · Used by 1

Statement usesGardam's group · Group ring of Gardam's group over the field with two elements · First free generator of Gardam's presentation · Second free generator of Gardam's presentation · Generators of Gardam's presentation · Gardam's element p · Gardam's element q · Gardam's element r · Relators of Gardam's group · Gardam's element s

Used byGardam's counterexample to the unit conjecture

TheoremGardam's counterexample to the unit conjecture#●ready to prove

Let \(P\) be the group with presentation \(\langle a, b \mid b^{-1}a^2b = a^{-2},\ a^{-1}b^2a = b^{-2} \rangle\), and set \(x = a^2\), \(y = b^2\) and \(z = (ab)^2\). In the group ring \(\mathbb{F}_2[P]\) set \(p = (1 + x)(1 + y)(1 + z^{-1})\), \(q = x^{-1}y^{-1} + x + y^{-1}z + z\), \(r = 1 + x + y^{-1}z + xyz\) and \(s = 1 + (x + x^{-1} + y + y^{-1})z^{-1}\), and let \(u = p + qa + rb + sab\). Then \(P\) is torsion-free (if \(g \in P\) and \(g^n = 1\) for some natural number \(n \neq 0\), then \(g = 1\)), \(u\) is a unit of \(\mathbb{F}_2[P]\), and \(u\) is not equal to any element \(g\) of \(P\) viewed in \(\mathbb{F}_2[P]\); that is, \(u\) is a non-trivial unit.

public theorem_wanted theorem_A : (∀ g : P, ∀ n ≠ 0, g ^ n = 1 → g = 1) ∧ IsUnit u ∧ ¬ ∃ g : P, u = g

Sources

• G. Gardam, A counterexample to the unit conjecture for group rings, Annals of Math, 194 (3) 2021. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_unit_conjecture of the lean-eval benchmark.

Uses 5

Statement usesGardam's group · Group ring of Gardam's group over the field with two elements · Generators of Gardam's presentation · Relators of Gardam's group · Gardam's unit

14 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.