7.3. Virasoro Verma modules
Triangular decomposition of the Virasoro algebra. A triangular decomposition
\begin{aligned}
\vir = \vir^0 \oplus \vir^+ \oplus \vir^-
\end{aligned}
of \vir is defined so that \vir^0 is spanned by L_0, C \in \vir,
\vir^+ is spanned by L_n for n > 0,
and \vir^- is spanned by L_n for n < 0.
(Without further comment, for the Virasoro algebra we always use this triangular decomposition.)
Lean code for Definition7.3.1●1 definition
Associated Lean declarations
-
VirasoroProject.virasoroTri[complete]
-
VirasoroProject.virasoroTri[complete]
-
defdefined in VirasoroProject/VirasoroVerma.leancomplete
def VirasoroProject.virasoroTri.{u_1} (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : VirasoroProject.TriangularDecomposition 𝕜 (VirasoroProject.VirasoroAlgebra 𝕜)
def VirasoroProject.virasoroTri.{u_1} (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : VirasoroProject.TriangularDecomposition 𝕜 (VirasoroProject.VirasoroAlgebra 𝕜)
The triangular decomposition of the Virasoro algebra with upper and lower (essentially nilpotent) parts spanned by the `Lₙ` with positive and negative `n`, respectively, and the Cartan subalgebra spanned by `L₀` and the central element `C`.
Virasoro Verma module.
Let c, h \in \bbk.
The Virasoro Verma module with central charge c and conformal weight h
is the Verma module \Verma^{\eta} associated to the linear functional
\eta \colon \vir^0 \to \bbk with
\begin{aligned}
\eta(L_0) = h, \quad \eta(C) = c .
\end{aligned}
We denote the Virasoro Verma module by \Verma^{c,h}.
Lean code for Definition7.3.2●1 definition
Associated Lean declarations
-
VirasoroProject.VirasoroVerma[complete]
-
VirasoroProject.VirasoroVerma[complete]
-
abbrevdefined in VirasoroProject/VirasoroVerma.leancomplete
abbrev VirasoroProject.VirasoroVerma.{u_1} (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (c h : 𝕜) : Type u_1
abbrev VirasoroProject.VirasoroVerma.{u_1} (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (c h : 𝕜) : Type u_1
The Verma module for the Virasoso algebra with central charge `c` and conformal weight `h`.