Sugawara construction applied to the charged Fock space

This file equips the charged Fock space representation of the Heisenberg algebra with the structure of a representation of the Virasoro algebra by applying the basic bosonic Sugawara construction.

Main definitions

• sugawaraRepresentationOfModuleUeaHeisenbergAlgebra: A variant of the Sugawara construction where the hypothesis is that the space is a module over the universal enveloping algebra of the Heisenberg algebra with local truncation condition.
• ChargedFockSpace.sugawaraRepresentation: The representation of Virasoro algebra with central charge c=1 on the charged Fock space, obtained by the basic bosonic Sugawara construction.
• ChargedFockSpace.instModuleUEAVirasoroAlgebra: The charged Fock space has the structure of a module over the universal enveloping algebra of the Virasoro algebra, by the basic bosonic Sugawara construction.
• ChargedFockSpace.virasoroVermaToChargedFockSpace: There is a Virasoro-module map from the Virasoro Verma module with central charge c = 1 and highest weight h = α²/2 to the charged Fock space with charge (J₀-eigenvalue) α, mapping the highest weight vector of the Verma module to the vacuum vector of the Fock space.

Main statements

• ChargedFockSpace.sugawaraRepresentation_lgen_zero_apply_vacuum: The vacuum in the charged Fock space is an eigenvector of L₀ with eigenvalue α²/2.
• ChargedFockSpace.sugawaraRepresentation_lgen_pos_apply_vacuum: The vacuum in the charged Fock space is annihilated by Lₙ for n > 0.

Tags

Heisenberg algebra, Fock space, Virasoro algebra, Sugawara construction

noncomputable def VirasoroProject.sugawaraRepresentationOfModuleUeaHeisenbergAlgebra (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] {V : Type u_2} [AddCommGroup V] [Module (𝓤 𝕜 (HeisenbergAlgebra 𝕜)) V] (htrunc : ∀ (v : V), ∀ᶠ (k : ℤ) in Filter.atTop, (ιUEA 𝕜) (HeisenbergAlgebra.jgen 𝕜 k) • v = 0) (hc : ∀ (v : V), (ιUEA 𝕜) (HeisenbergAlgebra.kgen 𝕜) • v = v) : LieAlgebra.Representation 𝕜 𝕜 (VirasoroAlgebra 𝕜) (ModuleOfModuleAlgebra 𝕜 (𝓤 𝕜 (HeisenbergAlgebra 𝕜)) V)

The basic bosonic Sugawara representation of Virasoro algebra (c=1): On a module over the universal enveloping algebra of the Heisenberg algebra in which the Heisenberg algebra acts locally truncatedly (and the central element k acts as 1), we get a representation of the Virasoro algebra with central charge c = 1 by the Sugawara construction.

Equations

• VirasoroProject.sugawaraRepresentationOfModuleUeaHeisenbergAlgebra 𝕜 htrunc hc = VirasoroProject.sugawaraRepresentation ⋯ ⋯

theorem VirasoroProject.sugawaraRepresentation_of_module_uea_heisenbergAlgebra_lgen_apply (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] {V : Type u_2} [AddCommGroup V] [Module (𝓤 𝕜 (HeisenbergAlgebra 𝕜)) V] (htrunc : ∀ (v : V), ∀ᶠ (k : ℤ) in Filter.atTop, (ιUEA 𝕜) (HeisenbergAlgebra.jgen 𝕜 k) • v = 0) (hc : ∀ (v : V), (ιUEA 𝕜) (HeisenbergAlgebra.kgen 𝕜) • v = v) (n : ℤ) (v : ModuleOfModuleAlgebra 𝕜 (𝓤 𝕜 (HeisenbergAlgebra 𝕜)) V) : ((sugawaraRepresentationOfModuleUeaHeisenbergAlgebra 𝕜 htrunc hc) (VirasoroAlgebra.lgen 𝕜 n)) v = 2⁻¹ • (ModuleOfModuleAlgebra.mkAddHom 𝕜 (𝓤 𝕜 (HeisenbergAlgebra 𝕜)) V) (∑ᶠ (k : ℤ) (_ : k ≥ 0), (ιUEA 𝕜) (HeisenbergAlgebra.jgen 𝕜 (n - k)) • (ιUEA 𝕜) (HeisenbergAlgebra.jgen 𝕜 k) • (ModuleOfModuleAlgebra.unMkAddHom 𝕜 (𝓤 𝕜 (HeisenbergAlgebra 𝕜)) V) v + ∑ᶠ (k : ℤ) (_ : k < 0), (ιUEA 𝕜) (HeisenbergAlgebra.jgen 𝕜 k) • (ιUEA 𝕜) (HeisenbergAlgebra.jgen 𝕜 (n - k)) • (ModuleOfModuleAlgebra.unMkAddHom 𝕜 (𝓤 𝕜 (HeisenbergAlgebra 𝕜)) V) v)

theorem VirasoroProject.sugawaraRepresentation_of_module_uea_heisenbergAlgebra_cgen_apply (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] {V : Type u_2} [AddCommGroup V] [Module (𝓤 𝕜 (HeisenbergAlgebra 𝕜)) V] (htrunc : ∀ (v : V), ∀ᶠ (k : ℤ) in Filter.atTop, (ιUEA 𝕜) (HeisenbergAlgebra.jgen 𝕜 k) • v = 0) (hc : ∀ (v : V), (ιUEA 𝕜) (HeisenbergAlgebra.kgen 𝕜) • v = v) (v : ModuleOfModuleAlgebra 𝕜 (𝓤 𝕜 (HeisenbergAlgebra 𝕜)) V) : ((sugawaraRepresentationOfModuleUeaHeisenbergAlgebra 𝕜 htrunc hc) (VirasoroAlgebra.cgen 𝕜)) v = v

noncomputable def VirasoroProject.ChargedFockSpace.sugawaraRepresentation (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) : LieAlgebra.Representation 𝕜 𝕜 (VirasoroAlgebra 𝕜) (ChargedFockSpace 𝕜 α)

Virasoro algebra representation on Fock space by basic bosonic Sugawara construction (c=1):

Equations

• VirasoroProject.ChargedFockSpace.sugawaraRepresentation 𝕜 α = VirasoroProject.sugawaraRepresentationOfModuleUeaHeisenbergAlgebra 𝕜 ⋯ ⋯

theorem VirasoroProject.ChargedFockSpace.sugawaraRepresentation_lgen_apply (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) (n : ℤ) (v : ChargedFockSpace 𝕜 α) : ((sugawaraRepresentation 𝕜 α) (VirasoroAlgebra.lgen 𝕜 n)) v = 2⁻¹ • (∑ᶠ (k : ℤ) (_ : k ≥ 0), (ιUEA 𝕜) (HeisenbergAlgebra.jgen 𝕜 (n - k)) • (ιUEA 𝕜) (HeisenbergAlgebra.jgen 𝕜 k) • v + ∑ᶠ (k : ℤ) (_ : k < 0), (ιUEA 𝕜) (HeisenbergAlgebra.jgen 𝕜 k) • (ιUEA 𝕜) (HeisenbergAlgebra.jgen 𝕜 (n - k)) • v)

The formula for the action of the Virasoro generators in the (basic) Sugawara representation on the charged Fock space.

theorem VirasoroProject.ChargedFockSpace.sugawaraRepresentation_lgen_apply_vacuum (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) (n : ℤ) : ((sugawaraRepresentation 𝕜 α) (VirasoroAlgebra.lgen 𝕜 n)) (vacuum 𝕜 α) = 2⁻¹ • ((ιUEA 𝕜) (HeisenbergAlgebra.jgen 𝕜 n) • (ιUEA 𝕜) (HeisenbergAlgebra.jgen 𝕜 0) • vacuum 𝕜 α + ∑ᶠ (k : ℤ) (_ : k < 0), (ιUEA 𝕜) (HeisenbergAlgebra.jgen 𝕜 k) • (ιUEA 𝕜) (HeisenbergAlgebra.jgen 𝕜 (n - k)) • vacuum 𝕜 α)

theorem VirasoroProject.ChargedFockSpace.sugawaraRepresentation_lgen_nonneg_apply_vacuum (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) {n : ℤ} (n_nn : 0 ≤ n) : ((sugawaraRepresentation 𝕜 α) (VirasoroAlgebra.lgen 𝕜 n)) (vacuum 𝕜 α) = 2⁻¹ • (ιUEA 𝕜) (HeisenbergAlgebra.jgen 𝕜 n) • (ιUEA 𝕜) (HeisenbergAlgebra.jgen 𝕜 0) • vacuum 𝕜 α

theorem VirasoroProject.ChargedFockSpace.sugawaraRepresentation_lgen_zero_apply_vacuum (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) : ((sugawaraRepresentation 𝕜 α) (VirasoroAlgebra.lgen 𝕜 0)) (vacuum 𝕜 α) = (α ^ 2 / 2) • vacuum 𝕜 α

The vacuum in the Fock space of charge α has L₀-eigenvalue α²/2.

theorem VirasoroProject.ChargedFockSpace.sugawaraRepresentation_lgen_pos_apply_vacuum (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) {n : ℤ} (n_pos : 0 < n) : ((sugawaraRepresentation 𝕜 α) (VirasoroAlgebra.lgen 𝕜 n)) (vacuum 𝕜 α) = 0

The vacuum in the Fock space of charge α is annihilated by Lₙ for n > 0.

@[simp]

theorem VirasoroProject.ChargedFockSpace.sugawaraRepresentation_cgen_apply (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) (v : ChargedFockSpace 𝕜 α) : ((sugawaraRepresentation 𝕜 α) (VirasoroAlgebra.cgen 𝕜)) v = v

The central element of the Virasoro algebra acts as the identity on the charged Fock space.

@[implicit_reducible]

noncomputable instance VirasoroProject.ChargedFockSpace.instModuleUEAVirasoroAlgebra (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) : Module (𝓤 𝕜 (VirasoroAlgebra 𝕜)) (ChargedFockSpace 𝕜 α)

Equations

• VirasoroProject.ChargedFockSpace.instModuleUEAVirasoroAlgebra 𝕜 α = (VirasoroProject.ChargedFockSpace.sugawaraRepresentation 𝕜 α).moduleUniversalEnvelopingAlgebra

@[simp]

theorem VirasoroProject.ChargedFockSpace.sugawaraRepresentation_smul_eq (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] {α : 𝕜} (a : 𝓤 𝕜 (VirasoroAlgebra 𝕜)) (v : ChargedFockSpace 𝕜 α) : a • v = (((UniversalEnvelopingAlgebra.lift 𝕜) (sugawaraRepresentation 𝕜 α)) a) v

theorem VirasoroProject.ChargedFockSpace.sugawaraRepresentation_ιUEA_smul_eq (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] {α : 𝕜} (X : VirasoroAlgebra 𝕜) (v : ChargedFockSpace 𝕜 α) : (ιUEA 𝕜) X • v = ((sugawaraRepresentation 𝕜 α) X) v

instance VirasoroProject.ChargedFockSpace.instHasCentralChargeOfNat (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) : HasCentralCharge 𝕜 (ChargedFockSpace 𝕜 α) 1

theorem VirasoroProject.ChargedFockSpace.algebraMap_virasoro_smul_eq (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] {α : 𝕜} (r : 𝕜) (v : ChargedFockSpace 𝕜 α) : (algebraMap 𝕜 (𝓤 𝕜 (VirasoroAlgebra 𝕜))) r • v = r • v

noncomputable def VirasoroProject.ChargedFockSpace.virasoroVermaToChargedFockSpace (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) : VirasoroVerma 𝕜 1 (α ^ 2 / 2) →ₗ[𝓤 𝕜 (VirasoroAlgebra 𝕜)] ChargedFockSpace 𝕜 α

A Virasoro module map from the Verma module with c = 1 and h = α^2 / 2 to the charged Fock space of charge α.

Equations

• VirasoroProject.ChargedFockSpace.virasoroVermaToChargedFockSpace 𝕜 α = VirasoroProject.VirasoroVerma.universalMap 𝕜 (VirasoroProject.ChargedFockSpace 𝕜 α) ⋯ ⋯ ⋯

theorem VirasoroProject.ChargedFockSpace.virasoroVermaToChargedFockSpace_hwVec (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) : (virasoroVermaToChargedFockSpace 𝕜 α) (VirasoroVerma.hwVec 𝕜 1 (α ^ 2 / 2)) = vacuum 𝕜 α