VirasoroProject

4.1. Definition of the Witt algebra🔗

Definition4.1.1
uses 0
Used by 2
Reverse dependency previews
Preview
Lemma 4.1.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Witt algebra. Let \bbk be a field (or a commutative ring). The Witt algebra over \bbk is the \bbk-vector space \witt (or free \bbk-module) with basis (\ell_n)_{n \in \bZ} and a \bbk-bilinear bracket \witt \times \witt \to \witt given on basis elements by

\begin{aligned} [\ell_n , \ell_m] = (n-m) \, \ell_{n+m} . \end{aligned}

Lean code for Definition4.1.1●2 definitions
  • defdefined in VirasoroProject/WittAlgebra.lean
    complete
    def VirasoroProject.WittAlgebra.{u_1} (𝕜 : Type u_1) [CommRing 𝕜] : Type u_1
    def VirasoroProject.WittAlgebra.{u_1}
  (𝕜 : Type u_1) [CommRing 𝕜] : Type u_1
    The Witt algebra: an ∞-dimensional Lie algebra (polynomial vector fields on a circle).
  • defdefined in VirasoroProject/WittAlgebra.lean
    complete
    def VirasoroProject.WittAlgebra.bracket.{u_1} (𝕜 : Type u_1) [CommRing 𝕜] :
  VirasoroProject.WittAlgebra 𝕜 →ₗ[𝕜]
    VirasoroProject.WittAlgebra 𝕜 →ₗ[𝕜] VirasoroProject.WittAlgebra 𝕜
    def VirasoroProject.WittAlgebra.bracket.{u_1}
  (𝕜 : Type u_1) [CommRing 𝕜] :
  VirasoroProject.WittAlgebra 𝕜 →ₗ[𝕜]
    VirasoroProject.WittAlgebra 𝕜 →ₗ[𝕜]
      VirasoroProject.WittAlgebra 𝕜
    The Lie bracket for the Witt algebra `WittAlgebra` as a bilinear map.

With some assumptions on \bbk, the Witt algebra \witt with the above bracket is an \infty-dimensional Lie algebra over \bbk.

Lemma4.1.2
uses 1
Used by 3
Reverse dependency previews
Preview
Definition 4.2.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Witt algebra is a Lie algebra. If \bbk is a field of characteristic zero, then \witt is a Lie algebra over \bbk.

(In the case when \bbk is a commutative ring, the \witt is also a Lie algebra assuming the \bbk has characteristic zero and that for c \in \bbk and X \in \witt we have c \cdot X = 0 only if either c = 0 or X = 0.)

Lean code for Lemma4.1.2●1 definition
  • defdefined in VirasoroProject/WittAlgebra.lean
    complete
    def VirasoroProject.WittAlgebra.instLieAlgebra.{u_1} {𝕜 : Type u_1}
  [CommRing 𝕜] [CharZero 𝕜]
  [NoZeroSMulDivisors 𝕜 (VirasoroProject.WittAlgebra 𝕜)] :
  LieAlgebra 𝕜 (VirasoroProject.WittAlgebra 𝕜)
    def VirasoroProject.WittAlgebra.instLieAlgebra.{u_1}
  {𝕜 : Type u_1} [CommRing 𝕜] [CharZero 𝕜]
  [NoZeroSMulDivisors 𝕜
      (VirasoroProject.WittAlgebra 𝕜)] :
  LieAlgebra 𝕜
    (VirasoroProject.WittAlgebra 𝕜)
    The Lie algebra structure on the Witt algebra `WittAlgebra`.
Proof for Lemma 4.1.2
uses 1

By construction, the bracket in Definition 4.1.1 is bilinear. It is antisymmetric on the basis vectors \ell_n, n \in \bZ, so by bilinearity the bracket is antisymmetric. It remains to check that the bracket satisfies Leibnitz rule (or the Jacobi identity), i.e., that for any X, Y, X \in \witt we have

\begin{aligned} \big[X, [Y, Z] \big] = \big[[X, Y] , Z \big] + \big[Y , [X, Z] \big] . \end{aligned}

This formula is trilinear in X,Y,Z, so it suffices to verify it on basis vectors X = \ell_n, Y = \ell_m, Z = \ell_k. Calculating, with Definition 4.1.1, we have

\begin{aligned} \big[\ell_n, [\ell_m, \ell_k] \big] = \big[\ell_n, (m-k) \ell_{m+k} \big] = (m-k) \big(n-(m+k)\big) \, \ell_{n+m+k} \end{aligned}

and

\begin{aligned} & \big[[\ell_n, \ell_m] , \ell_k \big] + \big[\ell_m , [\ell_n, \ell_k] \big] \\ = \; & \big[(n-m) \ell_{n+m} , \ell_k \big] + \big[\ell_m , (n-k) \ell_{n+k}] \big] \\ = \; & (n-m) \big( n+m-k \big) \, \ell_{n+m+k} + (n-k) \big( m-(n+k) \big) \, \ell_{m+n+k} . \end{aligned}

Noting that

\begin{aligned} (n-m) \big( n+m-k \big) + (n-k) \big( m-(n+k) \big) = (m-k) \big(n-(m+k)\big) , \end{aligned}

the Leibniz rule follows.