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).
• heisenbergTri: The triangular decomposition of the Heisenberg algebra whose positive (resp. negative) part is spanned by Jₖ with k positive (resp. negative) and the Cartan subalgebra is spanned by J₀ and the central element K.
• HeisenbergAlgebra.hw α: The (highest) weight of the Heisenberg algebra specified by the value α of the charge (J₀-eigenvalue); the central element K is by convention normalized to have value 1.
• ChargedFockSpace α: The charged Fock space representation of the Heisenberg algebra with charge (J₀-eigenvalue) α.
• ChargedFockSpace.vacuum: The vacuum vector (highest weight vector) of the charged Fock space.
• 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

• ChargedFockSpace.vacuum_cyclic: The charged Fock space is generated by its vacuum 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.
• ChargedFockSpace.jgen_pos_vacuum: The highest weight vector of a Virasoro Verma module is annihilated Jₖ for k > 0.
• ChargedFockSpace.jgen_zero_smul: The Heisenberg generator J₀ acts as scalar α (the charge) on the charged Fock space.
• ChargedFockSpace.kgen_smul: The central element K acts as scalar 1 in the charged Fock space.
• ChargedFockSpace.eventually_jgen_smul_eq_zero: The charged Fock space satisfies the local truncation condition (which is needed, e.g., for the Sugawara construction).

Implementation notes

The charged Fock space is defined as a Verma module for the Heisenberg Lie algebra (with an appropriate triangular decomposition).

Tags

Heisenberg algebra, Fock space

@[reducible, inline]

abbrev VirasoroProject.HasUnitCentral (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (M : Type u_2) [AddCommGroup M] [Module 𝕜 M] [Module (𝓤 𝕜 (HeisenbergAlgebra 𝕜)) M] : Prop

A Heisenberg module where the central generator K acts by the scalar 1.

Equations

• VirasoroProject.HasUnitCentral 𝕜 M = VirasoroProject.HasCentralValue 𝕜 (VirasoroProject.HeisenbergAlgebra 𝕜) M (VirasoroProject.HeisenbergAlgebra.kgen 𝕜) 1

theorem VirasoroProject.HasUnitCentral.kgen_smul (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (M : Type u_2) [AddCommGroup M] [Module 𝕜 M] [Module (𝓤 𝕜 (HeisenbergAlgebra 𝕜)) M] [HasUnitCentral 𝕜 M] (v : M) : (ιUEA 𝕜) (HeisenbergAlgebra.kgen 𝕜) • v = v

@[reducible, inline]

abbrev VirasoroProject.HasCharge (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (M : Type u_2) [AddCommGroup M] [Module 𝕜 M] [Module (𝓤 𝕜 (HeisenbergAlgebra 𝕜)) M] (α : 𝕜) : Prop

A Heisenberg module where J₀ acts by the charge α.

Equations

• VirasoroProject.HasCharge 𝕜 M α = VirasoroProject.HasCentralValue 𝕜 (VirasoroProject.HeisenbergAlgebra 𝕜) M (VirasoroProject.HeisenbergAlgebra.jgen 𝕜 0) α

theorem VirasoroProject.HasCharge.jgen_zero_smul (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (M : Type u_2) [AddCommGroup M] [Module 𝕜 M] [Module (𝓤 𝕜 (HeisenbergAlgebra 𝕜)) M] {α : 𝕜} [HasCharge 𝕜 M α] (v : M) : (ιUEA 𝕜) (HeisenbergAlgebra.jgen 𝕜 0) • v = α • v

noncomputable def VirasoroProject.heisenbergTri (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : TriangularDecomposition 𝕜 (HeisenbergAlgebra 𝕜)

The triangular decomposition of the Heisenberg algebra with upper and lower (essentially nilpotent) parts spanned by the Jₖ with positive and negative k, respectively, and the Cartan subalgebra spanned by J₀ and the central element K.

Equations

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

theorem VirasoroProject.heisenbergTri_cartan (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : (heisenbergTri 𝕜).cartan = Submodule.span 𝕜 {HeisenbergAlgebra.kgen 𝕜, HeisenbergAlgebra.jgen 𝕜 0}

theorem VirasoroProject.heisenbergTri_upper (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : (heisenbergTri 𝕜).upper = Submodule.span 𝕜 ((fun (n : ℤ) => HeisenbergAlgebra.jgen 𝕜 n) '' {n : ℤ | 0 < n})

theorem VirasoroProject.heisenbergTri_lower (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : (heisenbergTri 𝕜).lower = Submodule.span 𝕜 ((fun (n : ℤ) => HeisenbergAlgebra.jgen 𝕜 n) '' {n : ℤ | n < 0})

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

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

Equations

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

noncomputable def VirasoroProject.HeisenbergAlgebra.hw (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) : ↥(heisenbergTri 𝕜).cartan →ₗ[𝕜] 𝕜

The highest weight of Heisenberg algebra determined by charge α (J₀-eigenvalue). The K-eigenvalue is by convention normalized to 1 by default.

Equations

• VirasoroProject.HeisenbergAlgebra.hw 𝕜 α = ((VirasoroProject.heisenbergTriCartanBasis 𝕜).constr 𝕜) fun (i : ↑{none, some 0}) => if ↑i = none then 1 else α

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

The Heisenberg generator K as an element of the Cartan subalgebra.

Equations

• VirasoroProject.heisenbergTriKgen 𝕜 = ⟨VirasoroProject.HeisenbergAlgebra.kgen 𝕜, ⋯⟩

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

The Heisenberg generator J₀ as an element of the Cartan subalgebra.

Equations

• VirasoroProject.heisenbergTriJzero 𝕜 = ⟨VirasoroProject.HeisenbergAlgebra.jgen 𝕜 0, ⋯⟩

@[simp]

theorem VirasoroProject.heisenbergTri_kgen_val (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : ↑(heisenbergTriKgen 𝕜) = HeisenbergAlgebra.kgen 𝕜

@[simp]

theorem VirasoroProject.heisenbergTri_jzero_val (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : ↑(heisenbergTriJzero 𝕜) = HeisenbergAlgebra.jgen 𝕜 0

theorem VirasoroProject.heisenbergTri_cartan_basis_none_eq_kgen (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : (heisenbergTriCartanBasis 𝕜) ⟨none, ⋯⟩ = heisenbergTriKgen 𝕜

theorem VirasoroProject.heisenbergTri_cartan_basis_some_eq_jzero (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : (heisenbergTriCartanBasis 𝕜) ⟨some 0, ⋯⟩ = heisenbergTriJzero 𝕜

theorem VirasoroProject.heisenbergTri_kgen_mem_cartan (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : HeisenbergAlgebra.kgen 𝕜 ∈ (heisenbergTri 𝕜).cartan

theorem VirasoroProject.heisenbergTri_jgen_zero_mem_cartan (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : HeisenbergAlgebra.jgen 𝕜 0 ∈ (heisenbergTri 𝕜).cartan

theorem VirasoroProject.heisenbergTri_jgen_pos_mem_upper (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] {n : ℤ} (n_pos : 0 < n) : HeisenbergAlgebra.jgen 𝕜 n ∈ (heisenbergTri 𝕜).upper

theorem VirasoroProject.HeisenbergAlgebra.hw_apply_kgen (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) : (hw 𝕜 α) (heisenbergTriKgen 𝕜) = 1

theorem VirasoroProject.HeisenbergAlgebra.hw_apply_jzero (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) : (hw 𝕜 α) (heisenbergTriJzero 𝕜) = α

@[reducible, inline]

abbrev VirasoroProject.ChargedFockSpace (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) : Type u_1

The charged Fock space with charge α.

Equations

• VirasoroProject.ChargedFockSpace 𝕜 α = VirasoroProject.TriangularDecomposition.VermaHW (VirasoroProject.HeisenbergAlgebra.hw 𝕜 α)

@[reducible, inline]

noncomputable abbrev VirasoroProject.ChargedFockSpace.vacuum (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) : TriangularDecomposition.VermaHW (HeisenbergAlgebra.hw 𝕜 α)

The vacuum vector in the charged Fock space with charge α.

Equations

• VirasoroProject.ChargedFockSpace.vacuum 𝕜 α = VirasoroProject.TriangularDecomposition.VermaHW.hwVec (VirasoroProject.HeisenbergAlgebra.hw 𝕜 α)

theorem VirasoroProject.ChargedFockSpace.vacuum_cyclic (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) : 𝓤 𝕜 (HeisenbergAlgebra 𝕜) ∙ vacuum 𝕜 α = ⊤

theorem VirasoroProject.ChargedFockSpace.jgen_pos_vacuum (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) {k : ℤ} (k_pos : 0 < k) : (ιUEA 𝕜) (HeisenbergAlgebra.jgen 𝕜 k) • vacuum 𝕜 α = 0

Jₖ • vacuum(α) = 0 for k > 0

theorem VirasoroProject.ChargedFockSpace.jgen_zero_vacuum (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) : (ιUEA 𝕜) (HeisenbergAlgebra.jgen 𝕜 0) • vacuum 𝕜 α = α • vacuum 𝕜 α

theorem VirasoroProject.ChargedFockSpace.kgen_vacuum (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) : (ιUEA 𝕜) (HeisenbergAlgebra.kgen 𝕜) • vacuum 𝕜 α = vacuum 𝕜 α

theorem VirasoroProject.ChargedFockSpace.kgen_smul (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) (v : ChargedFockSpace 𝕜 α) : (ιUEA 𝕜) (HeisenbergAlgebra.kgen 𝕜) • v = v

J₀ • v = α • v for all v in ChargedFockSpace 𝕜 α

theorem VirasoroProject.ChargedFockSpace.jgen_zero_smul (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) (v : ChargedFockSpace 𝕜 α) : (ιUEA 𝕜) (HeisenbergAlgebra.jgen 𝕜 0) • v = α • v

J₀ • v = α • v for all v in ChargedFockSpace 𝕜 α

instance VirasoroProject.instHasUnitCentralChargedFockSpace (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) : HasUnitCentral 𝕜 (ChargedFockSpace 𝕜 α)

The charged Fock space with charge α has K action by unit scalar.

instance VirasoroProject.instHasChargeChargedFockSpace (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) : HasCharge 𝕜 (ChargedFockSpace 𝕜 α) α

The charged Fock space with charge α has charge α.

theorem VirasoroProject.HeisenbergAlgebra.ueaEventually_commute_jgen (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (a : 𝓤 𝕜 (HeisenbergAlgebra 𝕜)) : ∀ᶠ (k : ℤ) in Filter.atTop, Commute ((ιUEA 𝕜) (jgen 𝕜 k)) a

theorem VirasoroProject.ChargedFockSpace.eventually_jgen_smul_eq_zero (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) (v : ChargedFockSpace 𝕜 α) : ∀ᶠ (k : ℤ) in Filter.atTop, (ιUEA 𝕜) (HeisenbergAlgebra.jgen 𝕜 k) • v = 0