VirasoroProject

5. Virasoro algebra🔗

Definition5.1
Statement uses 2
Statement dependency previews
Preview
Definition 3.2.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

Virasoro algebra. Let \bbk be a field of characteristic zero. The Virasoro algebra \vir is the Lie algebra over \bbk obtained as the central extension of the Witt algebra \witt corresponding to the Virasoro cocycle {\gamma}_{\vir} \in C^2(\witt,\bbk).

Lean code for Definition5.1●3 declarations
  • defdefined in VirasoroProject/VirasoroAlgebra.lean
    complete
    def VirasoroProject.VirasoroAlgebra.{u_1} (𝕜 : Type u_1) [Field 𝕜]
  [CharZero 𝕜] : Type u_1
    def VirasoroProject.VirasoroAlgebra.{u_1}
  (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] :
  Type u_1
    The Virasoro algebra.
  • defdefined in VirasoroProject/VirasoroAlgebra.lean
    complete
    def VirasoroProject.VirasoroAlgebra.instLieAlgebra.{u_1} (𝕜 : Type u_1)
  [Field 𝕜] [CharZero 𝕜] :
  LieAlgebra 𝕜 (VirasoroProject.VirasoroAlgebra 𝕜)
    def VirasoroProject.VirasoroAlgebra.instLieAlgebra.{u_1}
  (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] :
  LieAlgebra 𝕜
    (VirasoroProject.VirasoroAlgebra 𝕜)
    The Virasoro algebra is a Lie algebra.
  • theoremdefined in VirasoroProject/VirasoroAlgebra.lean
    complete
    theorem VirasoroProject.VirasoroAlgebra.isCentralExtension.{u_1} (𝕜 : Type u_1)
  [Field 𝕜] [CharZero 𝕜] :
  VirasoroProject.LieAlgebra.IsCentralExtension
    (VirasoroProject.VirasoroAlgebra.ofCentral 𝕜)
    VirasoroProject.VirasoroAlgebra.toWittAlgebra
    theorem VirasoroProject.VirasoroAlgebra.isCentralExtension.{u_1}
  (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] :
  VirasoroProject.LieAlgebra.IsCentralExtension
    (VirasoroProject.VirasoroAlgebra.ofCentral
      𝕜)
    VirasoroProject.VirasoroAlgebra.toWittAlgebra
    The Virasoro algebra is a central extension of the Witt algebra.

From the definition of the Virasoro algebra and the Virasoro cocycle, Definition 5.1 and Definition 4.2.1, we directly obtain that \vir has a basis of the following form.

Definition5.2
uses 1
Used by 2
Reverse dependency previews
Preview
Definition 7.3.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

The standard basis of the Virasoro algebra. The Virasoro algebra \vir has a basis consisting of (L_n)_{n \in \bZ} and C, with Lie brackets determined by the following

\begin{aligned} [L_n, L_m] = \; & (n-m) \, L_{n+m} + \delta_{n+m,0} \frac{n^3 - n}{12} \, C , \end{aligned}

\begin{aligned} [C, L_n] = 0 , \qquad [C, C] = 0 , \end{aligned}

for n,m \in \bZ.

Lean code for Definition5.2●1 definition
  • defdefined in VirasoroProject/VirasoroAlgebra.lean
    complete
    def VirasoroProject.VirasoroAlgebra.basisLC.{u_1} (𝕜 : Type u_1) [Field 𝕜]
  [CharZero 𝕜] :
  Module.Basis (Option ℤ) 𝕜 (VirasoroProject.VirasoroAlgebra 𝕜)
    def VirasoroProject.VirasoroAlgebra.basisLC.{u_1}
  (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] :
  Module.Basis (Option ℤ) 𝕜
    (VirasoroProject.VirasoroAlgebra 𝕜)
    The most commonly used basis of the Virasoro algebra, consisting of `Lₙ` (`n ∈ ℤ`)
and the central element `C`. (Lean notation: `lgen _ n` and `cgen _`, respectively.)