Verma modules for the Virasoro algebra

This file defines Verma modules used in Lie algebra representation theory.

Main definitions

• HasCentralCharge: A typeclass for Vierasoro modules where the central element acts by multiplication by a particular scalar (the scalar is called the central charge).
• virasoroTri: The triangular decomposition of the Virasoro algebra whose positive (resp. negative) part is spanned by Lₙ with n positive (resp. negative) and the Cartan subalgebra is spanned by L₀ and the central element C.
• VirasoroAlgebra.hw c h: The (highest) weight of the Virasoro algebra specified by the value c of the central charge (C-eigenvalue) and the value h of the conformal weight (L₀-eigenvalue).
• VirasoroVerma c h: The Virasoro Verma module of highest weight h and central charge c.
• VirasoroVerma.hwVec: The highest weight vector of the Virasoro Verma module.
• VirasoroVerma.universalMap: The universal property of the Virasoro Verma module: Given another module M over 𝓤 𝕜 (VirasoroAlgebra 𝕜) and a "target" vector hwv ∈ M satisfying Lₙ • hwv = 0 for all n > 0, L₀ • hwv = h • hwv, and C • hwv = c • hwv, one obtains an A-module map from the Verma module to M uniquely specified by the requirement hwVec c h ↦ hwv.

Main statements

• VirasoroVerma.hwVec_cyclic: The Virasoro Verma module is generated by its highest weight vector.
• TriangularDecomposition.VermaHW.cartan_smul_hwVec: The highest weight vector of a Verma module is an eigenvector of the Cartan subalgebra with the eigenvalues specified by the highest weight.
• VirasoroVerma.lgen_zero_hwVec: The highest weight vector of a Virasoro Verma module has L₀-eigenvalue h.
• VirasoroVerma.lgen_pos_hwVec: The highest weight vector of a Virasoro Verma module is annihilated Lₙ for n > 0.
• VirasoroVerma.cgen_smul: The central element C acts as scalar c in the Virasoro Verma module.

Tags

Virasoro algebra, Verma module

@[reducible, inline]

abbrev VirasoroProject.HasCentralCharge (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (M : Type u_2) [AddCommGroup M] [Module 𝕜 M] [Module (𝓤 𝕜 (VirasoroAlgebra 𝕜)) M] (c : 𝕜) : Prop

A Virasoro module where the central generator C acts by the scalar c.

Equations

• VirasoroProject.HasCentralCharge 𝕜 M c = VirasoroProject.HasCentralValue 𝕜 (VirasoroProject.VirasoroAlgebra 𝕜) M (VirasoroProject.VirasoroAlgebra.cgen 𝕜) c

theorem VirasoroProject.HasCentralCharge.cgen_smul (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (M : Type u_2) [AddCommGroup M] [Module 𝕜 M] [Module (𝓤 𝕜 (VirasoroAlgebra 𝕜)) M] {c : 𝕜} [HasCentralCharge 𝕜 M c] (v : M) : (ιUEA 𝕜) (VirasoroAlgebra.cgen 𝕜) • v = c • v

noncomputable def VirasoroProject.virasoroTri (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : TriangularDecomposition 𝕜 (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.

Equations

• One or more equations did not get rendered due to their size.

theorem VirasoroProject.virasoroTri_cartan (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : (virasoroTri 𝕜).cartan = Submodule.span 𝕜 {VirasoroAlgebra.cgen 𝕜, VirasoroAlgebra.lgen 𝕜 0}

theorem VirasoroProject.virasoroTri_upper (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : (virasoroTri 𝕜).upper = Submodule.span 𝕜 ((fun (n : ℤ) => VirasoroAlgebra.lgen 𝕜 n) '' {n : ℤ | 0 < n})

theorem VirasoroProject.virasoroTri_lower (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : (virasoroTri 𝕜).lower = Submodule.span 𝕜 ((fun (n : ℤ) => VirasoroAlgebra.lgen 𝕜 n) '' {n : ℤ | n < 0})

noncomputable def VirasoroProject.virasoroTriCartanBasis (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : Module.Basis (↑{none, some 0}) 𝕜 ↥(virasoroTri 𝕜).cartan

The basis of the Cartan part of the Virasoro triangular decomposition.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def VirasoroProject.VirasoroAlgebra.hw (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (c h : 𝕜) : ↥(virasoroTri 𝕜).cartan →ₗ[𝕜] 𝕜

The highest weight of Virasoro algebra determined by the central charge c (C-eigenvalue) and conformal weight h (L₀-eigenvalue).

Equations

• VirasoroProject.VirasoroAlgebra.hw 𝕜 c h = ((VirasoroProject.virasoroTriCartanBasis 𝕜).constr 𝕜) fun (i : ↑{none, some 0}) => if ↑i = none then c else h

noncomputable def VirasoroProject.virasoroTriCgen (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : ↥((virasoroTri 𝕜).part 0)

The Virasoro generator C as an element of the Cartan subalgebra.

Equations

• VirasoroProject.virasoroTriCgen 𝕜 = ⟨VirasoroProject.VirasoroAlgebra.cgen 𝕜, ⋯⟩

noncomputable def VirasoroProject.virasoroTriLzero (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : ↥((virasoroTri 𝕜).part 0)

The Virasoro generator L₀ as an element of the Cartan subalgebra.

Equations

• VirasoroProject.virasoroTriLzero 𝕜 = ⟨VirasoroProject.VirasoroAlgebra.lgen 𝕜 0, ⋯⟩

@[simp]

theorem VirasoroProject.virasoroTri_cgen_val (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : ↑(virasoroTriCgen 𝕜) = VirasoroAlgebra.cgen 𝕜

@[simp]

theorem VirasoroProject.virasoroTri_lzero_val (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : ↑(virasoroTriLzero 𝕜) = VirasoroAlgebra.lgen 𝕜 0

theorem VirasoroProject.virasoroTri_cartan_basis_none_eq_cgen (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : (virasoroTriCartanBasis 𝕜) ⟨none, ⋯⟩ = virasoroTriCgen 𝕜

theorem VirasoroProject.virasoroTri_cartan_basis_some_eq_lzero (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : (virasoroTriCartanBasis 𝕜) ⟨some 0, ⋯⟩ = virasoroTriLzero 𝕜

theorem VirasoroProject.virasoroTri_cgen_mem_cartan (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : VirasoroAlgebra.cgen 𝕜 ∈ (virasoroTri 𝕜).cartan

theorem VirasoroProject.virasoroTri_lgen_zero_mem_cartan (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : VirasoroAlgebra.lgen 𝕜 0 ∈ (virasoroTri 𝕜).cartan

theorem VirasoroProject.virasoroTri_lgen_pos_mem_upper (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] {n : ℤ} (n_pos : 0 < n) : VirasoroAlgebra.lgen 𝕜 n ∈ (virasoroTri 𝕜).upper

theorem VirasoroProject.VirasoroAlgebra.hw_apply_cgen (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (c h : 𝕜) : (hw 𝕜 c h) (virasoroTriCgen 𝕜) = c

theorem VirasoroProject.VirasoroAlgebra.hw_apply_lzero (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (c h : 𝕜) : (hw 𝕜 c h) (virasoroTriLzero 𝕜) = h

@[reducible, inline]

abbrev VirasoroProject.VirasoroVerma (𝕜 : 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.

Equations

• VirasoroProject.VirasoroVerma 𝕜 c h = VirasoroProject.TriangularDecomposition.VermaHW (VirasoroProject.VirasoroAlgebra.hw 𝕜 c h)

@[reducible, inline]

noncomputable abbrev VirasoroProject.VirasoroVerma.hwVec (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (c h : 𝕜) : TriangularDecomposition.VermaHW (VirasoroAlgebra.hw 𝕜 c h)

The highest weight vector in the Verma module for the Virasoso algebra with central charge c and conformal weight h.

Equations

• VirasoroProject.VirasoroVerma.hwVec 𝕜 c h = VirasoroProject.TriangularDecomposition.VermaHW.hwVec (VirasoroProject.VirasoroAlgebra.hw 𝕜 c h)

theorem VirasoroProject.VirasoroVerma.hwVec_cyclic (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (c h : 𝕜) : 𝓤 𝕜 (VirasoroAlgebra 𝕜) ∙ hwVec 𝕜 c h = ⊤

theorem VirasoroProject.VirasoroVerma.lgen_pos_hwVec (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (c h : 𝕜) {n : ℤ} (n_pos : 0 < n) : (ιUEA 𝕜) (VirasoroAlgebra.lgen 𝕜 n) • hwVec 𝕜 c h = 0

theorem VirasoroProject.VirasoroVerma.lgen_zero_hwVec (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (c h : 𝕜) : (ιUEA 𝕜) (VirasoroAlgebra.lgen 𝕜 0) • hwVec 𝕜 c h = h • hwVec 𝕜 c h

theorem VirasoroProject.VirasoroVerma.cgen_hwVec (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (c h : 𝕜) : (ιUEA 𝕜) (VirasoroAlgebra.cgen 𝕜) • hwVec 𝕜 c h = c • hwVec 𝕜 c h

theorem VirasoroProject.VirasoroVerma.cgen_smul (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (c h : 𝕜) (v : VirasoroVerma 𝕜 c h) : (ιUEA 𝕜) (VirasoroAlgebra.cgen 𝕜) • v = c • v

instance VirasoroProject.instHasCentralChargeVirasoroVerma (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (c h : 𝕜) : HasCentralCharge 𝕜 (VirasoroVerma 𝕜 c h) c

The Virasoro Verma module with central charge c and conformal weight h has central charge c.

noncomputable def VirasoroProject.VirasoroVerma.universalMap (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] {c h : 𝕜} (M : Type u_2) [AddCommGroup M] [Module (𝓤 𝕜 (VirasoroAlgebra 𝕜)) M] {hwv : M} (hwv_c : (ιUEA 𝕜) (VirasoroAlgebra.cgen 𝕜) • hwv = (algebraMap 𝕜 (𝓤 𝕜 (VirasoroAlgebra 𝕜))) c • hwv) (hwv_lzero : (ιUEA 𝕜) (VirasoroAlgebra.lgen 𝕜 0) • hwv = (algebraMap 𝕜 (𝓤 𝕜 (VirasoroAlgebra 𝕜))) h • hwv) (hwv_lpos : ∀ n > 0, (ιUEA 𝕜) (VirasoroAlgebra.lgen 𝕜 n) • hwv = 0) : VirasoroVerma 𝕜 c h →ₗ[𝓤 𝕜 (VirasoroAlgebra 𝕜)] M

The universal map from a Virasoro Verma module to any module with a vector of the given central charge, conformal weight, and positive-mode annihilation.

Equations

• VirasoroProject.VirasoroVerma.universalMap 𝕜 M hwv_c hwv_lzero hwv_lpos = VirasoroProject.TriangularDecomposition.VermaHW.universalMap (VirasoroProject.VirasoroAlgebra.hw 𝕜 c h) M ⋯ ⋯

theorem VirasoroProject.VirasoroVerma.universalMap_hwVec (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (c h : 𝕜) (M : Type u_2) [AddCommGroup M] [Module (𝓤 𝕜 (VirasoroAlgebra 𝕜)) M] {hwv : M} (hwv_c : (ιUEA 𝕜) (VirasoroAlgebra.cgen 𝕜) • hwv = (algebraMap 𝕜 (𝓤 𝕜 (VirasoroAlgebra 𝕜))) c • hwv) (hwv_lzero : (ιUEA 𝕜) (VirasoroAlgebra.lgen 𝕜 0) • hwv = (algebraMap 𝕜 (𝓤 𝕜 (VirasoroAlgebra 𝕜))) h • hwv) (hwv_lpos : ∀ n > 0, (ιUEA 𝕜) (VirasoroAlgebra.lgen 𝕜 n) • hwv = 0) : (universalMap 𝕜 M hwv_c hwv_lzero hwv_lpos) (hwVec 𝕜 c h) = hwv