Witt's formula for free Lie algebras

InductiveFree Lie monomials#✓fully proved

Let \(K\) be a field, \(r\) a natural number, and \(L\) the free Lie algebra over \(K\) on generators \(x_0, \dots, x_{r-1}\). The relation "\(x\) is a homogeneous Lie monomial of multidegree \(d\)", for \(d \in \mathbb{N}^r\) and \(x \in L\), is defined inductively: each generator \(x_i\) is a monomial of multidegree \(e_i\), which is \(1\) at \(i\) and \(0\) elsewhere; and if \(x\) is a monomial of multidegree \(a\) and \(y\) is a monomial of multidegree \(b\), then the bracket \([x, y]\) is a monomial of multidegree \(a + b\), computed pointwise. There are no other monomials.

inductive IsFreeLieMonomial : (Fin r → ℕ) → FreeLieAlgebra K (Fin r) → Prop where
  | gen (i : Fin r) :
      IsFreeLieMonomial (Function.update (fun _ => 0) i 1) (FreeLieAlgebra.of K i)
  | bracket {a b : Fin r → ℕ} {x y : FreeLieAlgebra K (Fin r)} :
      IsFreeLieMonomial a x → IsFreeLieMonomial b y →
        IsFreeLieMonomial (fun i => a i + b i) (Bracket.bracket x y)
Used by 2
Used byDimension of a multihomogeneous component of a free Lie algebra · Multihomogeneous components of a free Lie algebra

DefinitionMultihomogeneous components of a free Lie algebra#✓fully proved

Let \(K\) be a field, \(r\) a natural number, and \(L\) the free Lie algebra over \(K\) on generators \(x_0, \dots, x_{r-1}\). For a multidegree \(d \in \mathbb{N}^r\), the multihomogeneous component of \(L\) of multidegree \(d\) is the \(K\)-linear span of the homogeneous Lie monomials of multidegree \(d\), that is, of the iterated brackets of the generators in which each \(x_i\) occurs exactly \(d_i\) times.

These components distinguish multidegrees, not only the total bracket length.

noncomputable def freeLieMultihomogeneousComponent (degree : Fin r → ℕ) :
    Submodule K (FreeLieAlgebra K (Fin r)) :=
  Submodule.span K { x | IsFreeLieMonomial K degree x }
Sources
  • Pieter Moree, Convoluted Convolved Fibonacci Numbers, Journal of Integer Sequences 7 (2004), Article 04.2.2, Witt's formula paragraph (the subspace H generated by homogeneous elements of multidegree (n₁, …, nᵣ)), lines 621–628, https://cs.uwaterloo.ca/journals/JIS/VOL7/Moree/moree12.tex.
Uses 1 · Used by 2
Statement usesFree Lie monomials
Used byDimension of a multihomogeneous component of a free Lie algebra · Witt's multigraded dimension formula

DefinitionWitt's multigraded value#✓fully proved

For natural numbers \(n_1, \dots, n_r\), let \(n = n_1 + \dots + n_r\) and \(g = \gcd(n_1, \dots, n_r)\). The rational number \(M(n_1, \dots, n_r)\) is \(0\) if \(n = 0\), and otherwise \(M(n_1, \dots, n_r) = \frac{1}{n} \sum_{d \mid g} \mu(d) \binom{n/d}{n_1/d, \ldots, n_r/d}\), where the sum runs over the positive divisors \(d\) of \(g\), \(\mu\) is the Möbius function, and the last factor is the multinomial coefficient of \(n_1/d, \dots, n_r/d\).

def wittMultigradedValue {r : ℕ} (degree : Fin r → ℕ) : ℚ :=
  let n := Finset.sum Finset.univ degree
  let g := Finset.univ.gcd degree
  if n = 0 then 0
  else (1 / (n : ℚ)) * Finset.sum (Nat.divisors g) (fun d =>
    ((ArithmeticFunction.moebius d : ℤ) : ℚ) *
      (Nat.multinomial Finset.univ (fun i => degree i / d) : ℚ))
Sources
  • Pieter Moree, Convoluted Convolved Fibonacci Numbers, Journal of Integer Sequences 7 (2004), Article 04.2.2, equations witty/basaal, lines 598–613 (Möbius inversion of the circular-word count; context Circular words and Witt's dimension formula, lines 574–597), https://cs.uwaterloo.ca/journals/JIS/VOL7/Moree/moree12.tex.
Used by 3
Used byDimension of a multihomogeneous component of a free Lie algebra · Witt's multigraded dimension formula · Witt's formula for the number of Lyndon words of given content

TheoremDimension of a multihomogeneous component of a free Lie algebra#✓fully proved

Let \(K\) be a field and let \(n_1, \dots, n_r\) be natural numbers with \(n_1 + \dots + n_r > 0\). Then the multihomogeneous component of multidegree \((n_1, \dots, n_r)\) of the free Lie algebra over \(K\) on \(r\) generators has dimension over \(K\) equal to Witt's multigraded value \(M(n_1, \dots, n_r)\).

theorem finrank_freeLieMultihomogeneousComponent
    (K : Type) [Field K] {r : ℕ} (degree : Fin r → ℕ)
    (hdegree : 0 < ∑ i, degree i) :
    (Module.finrank K (freeLieMultihomogeneousComponent K degree) : ℚ) =
      wittMultigradedValue degree
Uses 11 · Used by 1
Statement usesMultihomogeneous components of a free Lie algebra · Witt's multigraded value
Proof usesFree Lie monomials · Lyndon word · Lyndon words of given content · Words with prescribed content · Witt's formula for the number of Lyndon words of given content · The content of a word sums to its length · Content of a word · Content is additive under concatenation · Content of a one-letter word
Used byWitt's multigraded dimension formula

TheoremWitt's multigraded dimension formula#✓fully proved

Let \(K\) be a field, let \(r > 0\), and let \(n_1, \dots, n_r\) be natural numbers with \(n_1 + \dots + n_r > 0\). Then the multihomogeneous component of multidegree \((n_1, \dots, n_r)\) of the free Lie algebra over \(K\) on \(r\) generators has dimension over \(K\) equal to Witt's multigraded value \(M(n_1, \dots, n_r)\).

Proof: The Lyndon-word basis identifies the component with the Lyndon words of the prescribed content, which are counted by Möbius inversion.

theorem witt_multigraded_dimension_formula
    (K : Type) [Field K] (r : ℕ) (hr : 0 < r)
    (degree : Fin r → ℕ) (hdegree : 0 < ∑ i, degree i) :
    (Module.finrank K (freeLieMultihomogeneousComponent K degree) : ℚ) =
      wittMultigradedValue degree
Sources
Uses 3
Statement usesMultihomogeneous components of a free Lie algebra · Witt's multigraded value
Proof usesDimension of a multihomogeneous component of a free Lie algebra
5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.