Hall-Witt identity (source code)

= Hall-Witt identity
{c}

Use the <group commutator> convention $[x,y]=x^{-1}y^{-1}xy$ and write $u^v=v^{-1}uv$ for <conjugation>. The Hall-Witt identity is
$$
[[x,y^{-1}],z]^y\;[[y,z^{-1}],x]^z\;[[z,x^{-1}],y]^x=1.
$$
It holds in every <group>. Substituting the definitions and cancelling adjacent inverse letters proves the formula directly; the three cyclic factors are all necessary for that cancellation.

Modulo the fourth term of the <lower central series>, the triple <group commutators> are central, so the outer conjugations disappear. Replacing an inverse input changes the corresponding leading <group commutator> by its inverse. In additive notation for the <graded Lie algebra> associated with the <lower central series>, the identity becomes
$$
[[x,y],z]+[[y,z],x]+[[z,x],y]=0,
$$
the <Jacobi identity>. This explains how a group-theoretic cancellation identity supplies the Lie-theoretic compatibility of leading commutators.