Basic commutators

InductiveFormal commutators#✓fully proved

The formal commutators (bracket arrangements) in an alphabet \(\alpha\) are the formal expressions generated by two rules: every letter \(a \in \alpha\) is a formal commutator, and for formal commutators \(u\) and \(v\), the bracket \([u, v]\) is a formal commutator.

inductive Bracket (α : Type*)
  /-- A letter, a formal commutator of weight 1. -/
  | letter : α → Bracket α
  /-- The formal commutator `[u, v]`. -/
  | comm : Bracket α → Bracket α → Bracket α

Used by 4

Used byGaglione–Spellman claim on equal commutators of basic commutators · Value of a formal commutator · Basic commutators · Weight of a formal commutator

DefinitionWeight of a formal commutator#✓fully proved

The weight of a formal commutator is the number of occurrences of letters in it: a letter has weight \(1\), and \([u, v]\) has weight the weight of \(u\) plus the weight of \(v\).

def Bracket.weight {α : Type*} : Bracket α → ℕ
  | letter _ => 1
  | comm u v => u.weight + v.weight

Uses 1 · Used by 1

Statement usesFormal commutators

Used byGaglione–Spellman claim on equal commutators of basic commutators

DefinitionCommutator, Kourovka–Hall convention#✓fully proved

For elements \(x\) and \(y\) of a group, their commutator is \([x, y] = x^{-1} y^{-1} x y\) (the convention of the Kourovka Notebook and of Hall).

def kcomm {G : Type*} [Group G] (x y : G) : G := x⁻¹ * y⁻¹ * x * y

Used by 2

Used byGaglione–Spellman claim on equal commutators of basic commutators · Value of a formal commutator

DefinitionValue of a formal commutator#✓fully proved

Each formal commutator in the letters \(\alpha\) has a value in the free group \(F(\alpha)\) on \(\alpha\): a letter \(a\) has the value of the generator \(a\), and \([u, v]\) has the value \(\bar u^{-1} \bar v^{-1} \bar u \bar v\), where \(\bar u\) and \(\bar v\) are the values of \(u\) and \(v\).

def Bracket.eval {α : Type*} : Bracket α → FreeGroup α
  | letter a => FreeGroup.of a
  | comm u v => kcomm u.eval v.eval

Uses 2 · Used by 1

Statement usesFormal commutators · Commutator, Kourovka–Hall convention

Used byGaglione–Spellman claim on equal commutators of basic commutators

DefinitionBasic commutators#✓fully proved

Let \(<\) be a relation on the formal commutators in the letters \(\alpha\) (in applications, a linear order). Every letter is basic for \(<\), and a formal commutator \([u, v]\) is basic for \(<\) when \(u\) and \(v\) are basic for \(<\), \(v < u\), and, in case \(u = [y, z]\) is itself a bracket, \(v < z\) fails (for a linear order: \(z \le v\)). This is M. Hall's definition.

def Bracket.IsBasic {α : Type*} (lt : Bracket α → Bracket α → Prop) : Bracket α → Prop
  | letter _ => True
  | comm u v => u.IsBasic lt ∧ v.IsBasic lt ∧ lt v u ∧
      match u with
      | letter _ => True
      | comm _ z => ¬ lt v z

Uses 1 · Used by 1

Statement usesFormal commutators

Used byGaglione–Spellman claim on equal commutators of basic commutators

DefinitionGaglione–Spellman claim on equal commutators of basic commutators#✓fully proved

The proposition (Kourovka Problem 11.20, A. Gaglione and D. Spellman) that the following holds. Write \([x, y] = x^{-1} y^{-1} x y\). For every linearly ordered type \(\alpha\) and every linear order \(<\) on the formal commutators in the letters \(\alpha\) that orders the letters as in \(\alpha\) and puts formal commutators of smaller weight first (within one weight it is arbitrary), if \(a\) and \(b\) are formal commutators such that the formal commutator \([a, b]\) is basic for \(<\) (so \(a\) and \(b\) are basic too), \(c\) and \(d\) are elements of the free group \(F(\alpha)\), each of the form \([x, y]\) with \(x, y \in F(\alpha)\), and \([\bar a, \bar b] = [c, d]\) in \(F(\alpha)\), where \(\bar a\) and \(\bar b\) are the values of \(a\) and \(b\) in \(F(\alpha)\), then \(\bar a = c\) and \(\bar b = d\).

def basicCommutatorEqualityDetermines : Prop :=
  ∀ (α : Type) [LinearOrder α] (o : LinearOrder (Bracket α)),
    (∀ u v : Bracket α, u.weight < v.weight → o.lt u v) →
    (∀ a b : α, a < b → o.lt (.letter a) (.letter b)) →
    ∀ ta tb : Bracket α, (Bracket.comm ta tb).IsBasic o.lt →
    ∀ c d : FreeGroup α, (∃ x y : FreeGroup α, c = kcomm x y) →
      (∃ x y : FreeGroup α, d = kcomm x y) →
      kcomm ta.eval tb.eval = kcomm c d → ta.eval = c ∧ tb.eval = d

Uses 5 · Used by 1

Statement usesFormal commutators · Basic commutators · Value of a formal commutator · Weight of a formal commutator · Commutator, Kourovka–Hall convention

Used byEqual commutators of basic commutators do not determine their entries

TheoremEqual commutators of basic commutators do not determine their entries#●ready to prove

The Gaglione–Spellman claim on equal commutators of basic commutators (Kourovka Problem 11.20) is false: writing \([x, y] = x^{-1} y^{-1} x y\), there are a linearly ordered type \(\alpha\), a linear order \(<\) on the formal commutators in the letters \(\alpha\) that orders the letters as in \(\alpha\) and puts formal commutators of smaller weight first, formal commutators \(a\) and \(b\) such that the formal commutator \([a, b]\) is basic for \(<\), and elements \(c\) and \(d\) of the free group \(F(\alpha)\), each of the form \([x, y]\) with \(x, y \in F(\alpha)\), such that \([\bar a, \bar b] = [c, d]\) in \(F(\alpha)\), where \(\bar a\) and \(\bar b\) are the values of \(a\) and \(b\) in \(F(\alpha)\), but \(\bar a \ne c\) or \(\bar b \ne d\).

public theorem_wanted basicCommutatorEqualityDetermines_refuted :
    ¬ basicCommutatorEqualityDetermines

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 11.20 (A. Gaglione, D. Spellman); resolution: V. G. Bardakov, Abstracts of the IIIrd Intern. Conf. on Algebra, Krasnoyarsk, 1993, p. 33 (Russian), Kourovka Archive, Problem 11.20: "No, not always"; for free generators x₁ < x₂ < x₃, a = [[x₂, x₁], x₃], b = [x₂, x₁], c = b⁻¹, d = b^{x₃ b}, https://arxiv.org/abs/1401.0300v49.

Uses 1

Statement usesGaglione–Spellman claim on equal commutators of basic commutators

6 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.