The bosonic Sugawara construction

This file contains the basic bosonic Sugawara construction.

Main definitions

• VirasoroAlgebra.representationOfCentralChargeOfL: A variant of the construction (LieAlgebra.representationOfBasis) of a representation of a Lie algebra from operators corresponding to a basis, for the special case of the Virasoro algebra: a representation is constructed from operators corresponding to the lgen Virasoro generators satisfying commutation relations with a given central charge c.
• VirasoroProject.sugawaraRepresentation: Any representation of the Heisenberg algebra where the Heisenberg modes act in a locally truncated fashion can be made into a representation of the Virasoro algebra with central charge c = 1 by the (basic) bosonic Sugawara construction.

Main statements

• VirasoroProject.commutator_sugawaraGen: Given operators A(k), k ∈ ℤ, satisfying Heisengerg algebra commutation relations and acting in a locally truncated way, the Sugawara operators Lₙ = 1/2 • ∑ k, :A(n-k)A(k): for n ∈ ℤ satisfy the commutation relations of the Virasoro generators (here the normal ordered product :A(n-k)A(k): is the composition of A(n-k) and A(k) in an order depending on the indices n-k and k).
• VirasoroProject.sugawaraRepresentation_lgen_apply: In VirasoroProject.sugawaraRepresentation, the Virasoro generators lgen _ n, n ∈ ℤ, act by the Sugawara formula Lₙ = 1/2 • ∑ k ≥ 0, A(n-k) ∘ A(k) + 1/2 • ∑ k < 0, A(k) ∘ A(n-k).
• VirasoroProject.sugawaraRepresentation_cgen_apply: In VirasoroProject.sugawaraRepresentation, the central charge is c = 1, i.e., the Virasoro generator cgen _ acts as 1 • id.

Tags

Sugawara construction, Virasoro algebra, Heisenberg algebra, bosonic Fock space

def VirasoroProject.pairNO {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] (heiOper : ℤ → V →ₗ[𝕜] V) (k l : ℤ) : V →ₗ[𝕜] V

Normal ordered pair of two operators: pairNO k l equals (heiOper l) ∘ (heiOper k) if l ≤ k, and (heiOper k) ∘ (heiOper l) otherwise.

Equations

• VirasoroProject.pairNO heiOper k l = if l ≤ k then heiOper l ∘ₗ heiOper k else heiOper k ∘ₗ heiOper l

def VirasoroProject.pairNO' {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] (heiOper : ℤ → V →ₗ[𝕜] V) (k l : ℤ) : V →ₗ[𝕜] V

Alternative normal ordered pair of two operators: pairNO' k l equals (heiOper l) ∘ (heiOper k) if k ≥ 0, and (heiOper k) ∘ (heiOper l) otherwise.

Equations

• VirasoroProject.pairNO' heiOper k l = if 0 ≤ k then heiOper l ∘ₗ heiOper k else heiOper k ∘ₗ heiOper l

theorem VirasoroProject.pairNO_apply_eq_zero {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] (A : ℤ → V →ₗ[𝕜] V) {v : V} {N : ℤ} (A_trunc : ∀ n ≥ N, (A n) v = 0) {k l : ℤ} (h : N ≤ max k l) : (pairNO A k l) v = 0

theorem VirasoroProject.heiComm_of_add_ne_zero {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] (heiOper : ℤ → V →ₗ[𝕜] V) (heiComm : ∀ (k l : ℤ), (heiOper k).commutator (heiOper l) = if k + l = 0 then ↑k • 1 else 0) {k l : ℤ} (hkl : k + l ≠ 0) : heiOper k ∘ₗ heiOper l = heiOper l ∘ₗ heiOper k

heiOper k and heiOper l commute unless k = l.

theorem VirasoroProject.heiOper_pairNO_eq_pairNO' {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] {heiOper : ℤ → V →ₗ[𝕜] V} (heiComm : ∀ (k l : ℤ), (heiOper k).commutator (heiOper l) = if k + l = 0 then ↑k • 1 else 0) (k l : ℤ) : pairNO heiOper k l = pairNO' heiOper k l

The two definitions of normal ordered pairs coincide.

theorem VirasoroProject.finite_support_smul_pairNO_heiOper_apply {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] {heiOper : ℤ → V →ₗ[𝕜] V} (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) {𝕂 : Type u_3} [SMulZeroClass 𝕂 V] (n m : ℤ) (a : ℤ → 𝕂) (v : V) : (Function.support fun (k : ℤ) => a k • (pairNO heiOper (m - k) (n + k)) v).Finite

theorem VirasoroProject.finite_support_pairNO_heiOper_apply {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] {heiOper : ℤ → V →ₗ[𝕜] V} (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) (n m : ℤ) (v : V) : (Function.support fun (k : ℤ) => (pairNO heiOper (m - k) (n + k)) v).Finite

theorem VirasoroProject.finite_support_smul_pairNO'_heiOper_apply {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] {heiOper : ℤ → V →ₗ[𝕜] V} (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) (heiComm : ∀ (k l : ℤ), (heiOper k).commutator (heiOper l) = if k + l = 0 then ↑k • 1 else 0) {𝕂 : Type u_3} [SMulZeroClass 𝕂 V] (n m : ℤ) (a : ℤ → 𝕂) (v : V) : (Function.support fun (k : ℤ) => a k • (pairNO' heiOper (m - k) (n + k)) v).Finite

theorem VirasoroProject.finite_support_smul_pairNO_heiOper_apply₀ {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] {heiOper : ℤ → V →ₗ[𝕜] V} (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) {𝕂 : Type u_3} [SMulZeroClass 𝕂 V] (s : ℤ) (a : ℤ → 𝕂) (v : V) : (Function.support fun (k : ℤ) => a k • (pairNO heiOper (s - k) k) v).Finite

theorem VirasoroProject.finite_support_pairNO_heiOper_apply₀ {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] {heiOper : ℤ → V →ₗ[𝕜] V} (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) (s : ℤ) (v : V) : (Function.support fun (k : ℤ) => (pairNO heiOper (s - k) k) v).Finite

theorem VirasoroProject.finite_support_pairNO'_heiOper_apply {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] {heiOper : ℤ → V →ₗ[𝕜] V} (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) (heiComm : ∀ (k l : ℤ), (heiOper k).commutator (heiOper l) = if k + l = 0 then ↑k • 1 else 0) (n m : ℤ) (v : V) : (Function.support fun (k : ℤ) => (pairNO' heiOper (m - k) (n + k)) v).Finite

theorem VirasoroProject.finite_support_smul_pairNO'_heiOper_apply₀ {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] {heiOper : ℤ → V →ₗ[𝕜] V} (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) (heiComm : ∀ (k l : ℤ), (heiOper k).commutator (heiOper l) = if k + l = 0 then ↑k • 1 else 0) {𝕂 : Type u_3} [SMulZeroClass 𝕂 V] (s : ℤ) (a : ℤ → 𝕂) (v : V) : (Function.support fun (k : ℤ) => a k • (pairNO' heiOper (s - k) k) v).Finite

theorem VirasoroProject.finite_support_pairNO'_heiOper_apply₀ {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] {heiOper : ℤ → V →ₗ[𝕜] V} (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) (heiComm : ∀ (k l : ℤ), (heiOper k).commutator (heiOper l) = if k + l = 0 then ↑k • 1 else 0) (s : ℤ) (v : V) : (Function.support fun (k : ℤ) => (pairNO' heiOper (s - k) k) v).Finite

theorem VirasoroProject.heiOper_pairNO_symm {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] (heiOper : ℤ → V →ₗ[𝕜] V) (k l : ℤ) : pairNO heiOper k l = pairNO heiOper l k

pairNO k l is symmetric in k and l.

theorem VirasoroProject.heiOper_pairNO'_symm {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] (heiOper : ℤ → V →ₗ[𝕜] V) (heiComm : ∀ (k l : ℤ), (heiOper k).commutator (heiOper l) = if k + l = 0 then ↑k • 1 else 0) (k l : ℤ) : pairNO' heiOper k l = pairNO' heiOper l k

pairNO' k l is symmetric in k and l.

theorem VirasoroProject.heiPairNO_trunc_atTop_sub {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] (heiOper : ℤ → V →ₗ[𝕜] V) (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) (n : ℤ) (v : V) : ∀ᶠ (k : ℤ) in Filter.atTop, (pairNO heiOper (n - k) k) v = 0

theorem VirasoroProject.heiPairNO_trunc_atBot_sub {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] (heiOper : ℤ → V →ₗ[𝕜] V) (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) (n : ℤ) (v : V) : ∀ᶠ (k : ℤ) in Filter.atBot, (pairNO heiOper (n - k) k) v = 0

theorem VirasoroProject.heiPairNO_trunc_cofinite_sub {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] (heiOper : ℤ → V →ₗ[𝕜] V) (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) (n : ℤ) (v : V) : ∀ᶠ (k : ℤ) in Filter.cofinite, (pairNO heiOper (n - k) k) v = 0

noncomputable def VirasoroProject.sugawaraGenAux {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] (heiOper : ℤ → V →ₗ[𝕜] V) (n : ℤ) (v : V) : V

The basic bosonic Sugawara generators (an auxiliary definition).

Equations

• VirasoroProject.sugawaraGenAux heiOper n v = 2⁻¹ • ∑ᶠ (k : ℤ), (VirasoroProject.pairNO heiOper (n - k) k) v

theorem VirasoroProject.sugawaraGenAux_def {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] (heiOper : ℤ → V →ₗ[𝕜] V) (n : ℤ) (v : V) : sugawaraGenAux heiOper n v = 2⁻¹ • ∑ᶠ (k : ℤ), (pairNO heiOper (n - k) k) v

theorem VirasoroProject.sugawaraGenAux_comp_apply {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] (heiOper : ℤ → V →ₗ[𝕜] V) (A : V →ₗ[𝕜] V) (n : ℤ) (v : V) : sugawaraGenAux heiOper n (A v) = 2⁻¹ • ∑ᶠ (k : ℤ), (pairNO heiOper (n - k) k) (A v)

theorem VirasoroProject.comp_sugawaraGenAux_apply {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] {heiOper : ℤ → V →ₗ[𝕜] V} (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) (A : V →ₗ[𝕜] V) (n : ℤ) (v : V) : A (sugawaraGenAux heiOper n v) = 2⁻¹ • ∑ᶠ (k : ℤ), A ((pairNO heiOper (n - k) k) v)

theorem VirasoroProject.sugawaraGenAux_add {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] {heiOper : ℤ → V →ₗ[𝕜] V} (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) (n : ℤ) (v w : V) : sugawaraGenAux heiOper n (v + w) = sugawaraGenAux heiOper n v + sugawaraGenAux heiOper n w

theorem VirasoroProject.sugawaraGenAux_smul {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] (heiOper : ℤ → V →ₗ[𝕜] V) (n : ℤ) (c : 𝕜) (v : V) : sugawaraGenAux heiOper n (c • v) = c • sugawaraGenAux heiOper n v

noncomputable def VirasoroProject.sugawaraGen {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] {heiOper : ℤ → V →ₗ[𝕜] V} (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) (n : ℤ) : V →ₗ[𝕜] V

The basic bosonic Sugawara generators (as linear operators).

Equations

• VirasoroProject.sugawaraGen heiTrunc n = { toFun := VirasoroProject.sugawaraGenAux heiOper n, map_add' := ⋯, map_smul' := ⋯ }

theorem VirasoroProject.sugawaraGen_apply {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] {heiOper : ℤ → V →ₗ[𝕜] V} (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) (n : ℤ) (v : V) : (sugawaraGen heiTrunc n) v = 2⁻¹ • ∑ᶠ (k : ℤ), (pairNO heiOper (n - k) k) v

theorem VirasoroProject.sugawaraGen_apply_eq_finsum_shift {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] {heiOper : ℤ → V →ₗ[𝕜] V} (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) (n s : ℤ) (v : V) : (sugawaraGen heiTrunc n) v = 2⁻¹ • ∑ᶠ (k : ℤ), (pairNO heiOper (n - (k + s)) (k + s)) v

theorem VirasoroProject.commutator_sugawaraGen_apply_eq_finsum_commutator_apply {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] {heiOper : ℤ → V →ₗ[𝕜] V} (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) (n : ℤ) (A : V →ₗ[𝕜] V) (v : V) : ((sugawaraGen heiTrunc n).commutator A) v = 2⁻¹ • ∑ᶠ (k : ℤ), ((pairNO heiOper (n - k) k).commutator A) v

theorem VirasoroProject.sugawaraGen_commutator_apply_eq_finsum_commutator_apply {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] {heiOper : ℤ → V →ₗ[𝕜] V} (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) (n : ℤ) (A : V →ₗ[𝕜] V) (v : V) : (A.commutator (sugawaraGen heiTrunc n)) v = 2⁻¹ • ∑ᶠ (k : ℤ), (A.commutator (pairNO heiOper (n - k) k)) v

theorem VirasoroProject.commutator_heiPair_heiGen {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] {heiOper : ℤ → V →ₗ[𝕜] V} (heiComm : ∀ (k l : ℤ), (heiOper k).commutator (heiOper l) = if k + l = 0 then ↑k • 1 else 0) (l k m : ℤ) : (heiOper l * heiOper k).commutator (heiOper m) = (-↑m * ((if k + m = 0 then 1 else 0) + if l + m = 0 then 1 else 0)) • heiOper (k + l + m)

[(heiOper l) ∘ (heiOper k), (heiOper m)] = -m * (δ[k+m=0] + δ[l+m=0]) • heiOper (k + l + m)

theorem VirasoroProject.commutator_heiPairNO_heiGen {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] {heiOper : ℤ → V →ₗ[𝕜] V} (heiComm : ∀ (k l : ℤ), (heiOper k).commutator (heiOper l) = if k + l = 0 then ↑k • 1 else 0) (l k m : ℤ) : (pairNO heiOper l k).commutator (heiOper m) = (-↑m * ((if k + m = 0 then 1 else 0) + if l + m = 0 then 1 else 0)) • heiOper (k + l + m)

[:(heiOper l)(heiOper k):, (heiOper m)] = -m * (δ[k+m=0] + δ[l+m=0]) • heiOper (k + l + m)

theorem VirasoroProject.commutator_sugawaraGen_heiOper {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] {heiOper : ℤ → V →ₗ[𝕜] V} (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) (heiComm : ∀ (k l : ℤ), (heiOper k).commutator (heiOper l) = if k + l = 0 then ↑k • 1 else 0) [CharZero 𝕜] (n m : ℤ) : (sugawaraGen heiTrunc n).commutator (heiOper m) = -m • heiOper (n + m)

[L(n), J(m)] = -m • J(n+m)

theorem VirasoroProject.commutator_sugawaraGen_heiOperPair {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] {heiOper : ℤ → V →ₗ[𝕜] V} (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) (heiComm : ∀ (k l : ℤ), (heiOper k).commutator (heiOper l) = if k + l = 0 then ↑k • 1 else 0) [CharZero 𝕜] (n m k : ℤ) : (sugawaraGen heiTrunc n).commutator (heiOper (m - k) * heiOper k) = -k • (heiOper (m - k) * heiOper (n + k)) - (m - k) • (heiOper (n + m - k) * heiOper k)

[L(n), J(m-k)J(k)] = -k • J(m-k)J(n+k) - (m-k) • J(n+m-k)J(k)

theorem VirasoroProject.commutator_sugawaraGen_heiPairNO' {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] {heiOper : ℤ → V →ₗ[𝕜] V} (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) (heiComm : ∀ (k l : ℤ), (heiOper k).commutator (heiOper l) = if k + l = 0 then ↑k • 1 else 0) [CharZero 𝕜] (n m k : ℤ) : (sugawaraGen heiTrunc n).commutator (pairNO' heiOper k (m - k)) = -k • (pairNO' heiOper (n + k) (m - k) + if 0 ≤ k ∧ k < -n ∧ n + m = 0 then -(n + k) • 1 else 0 + if k < 0 ∧ -n ≤ k ∧ n + m = 0 then (n + k) • 1 else 0) - (m - k) • pairNO' heiOper k (n + m - k)

[L(n), :J(m-k)J(k):] = -k • :J(m-k)J(n+k): - (m-k) • :J(n+m-k)J(k): + extra terms • 1

theorem VirasoroProject.commutator_sugawaraGen_heiPairNO'_apply {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] {heiOper : ℤ → V →ₗ[𝕜] V} (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) (heiComm : ∀ (k l : ℤ), (heiOper k).commutator (heiOper l) = if k + l = 0 then ↑k • 1 else 0) [CharZero 𝕜] (n m k : ℤ) (v : V) : ((sugawaraGen heiTrunc n).commutator (pairNO' heiOper k (m - k))) v = -k • ((pairNO' heiOper (n + k) (m - k)) v + if 0 ≤ k ∧ k < -n ∧ n + m = 0 then -(n + k) • v else 0 + if k < 0 ∧ -n ≤ k ∧ n + m = 0 then (n + k) • v else 0) - (m - k) • (pairNO' heiOper k (n + m - k)) v

[L(n), :J(m-k)J(k):] v = -k • :J(m-k)J(n+k): v - (m-k) • :J(n+m-k)J(k): v + extra terms • v

theorem VirasoroProject.commutator_sugawaraGen {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] (heiOper : ℤ → V →ₗ[𝕜] V) (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) (heiComm : ∀ (k l : ℤ), (heiOper k).commutator (heiOper l) = if k + l = 0 then ↑k • 1 else 0) [CharZero 𝕜] (n m : ℤ) : (sugawaraGen heiTrunc n).commutator (sugawaraGen heiTrunc m) = (n - m) • sugawaraGen heiTrunc (n + m) + if n + m = 0 then ((↑n ^ 3 - ↑n) / 12) • 1 else 0

[L(n), L(m)] = (n-m) • L(n+m) + (n^3 - n) / 12 * δ[n+m,0] • 1

noncomputable def VirasoroProject.VirasoroAlgebra.representationOfCentralChargeOfL {𝕂 : Type u_3} [Field 𝕂] [CharZero 𝕂] {V : Type u_4} [AddCommGroup V] [Module 𝕂 V] (c : 𝕂) {lOper : ℤ → V →ₗ[𝕂] V} (lComm : ∀ (n m : ℤ), (lOper n).commutator (lOper m) = (n - m) • lOper (n + m) + if n + m = 0 then (c / 12 * (↑n ^ 3 - ↑n)) • 1 else 0) : LieAlgebra.Representation 𝕂 𝕂 (VirasoroAlgebra 𝕂) V

Construct a representation of Virasoro algebra from a central charge value c and a collection (Lₙ), n ∈ ℤ, of operators satisfying the commutation relations of Virasoro generators with that central charge.

Equations

• VirasoroProject.VirasoroAlgebra.representationOfCentralChargeOfL c lComm = LieAlgebra.representationOfBasis (VirasoroProject.VirasoroAlgebra.basisLC 𝕂) ⋯

theorem VirasoroProject.VirasoroAlgebra.representationOfCentralChargeOfL_cgen {𝕂 : Type u_3} [Field 𝕂] [CharZero 𝕂] {V : Type u_4} [AddCommGroup V] [Module 𝕂 V] (c : 𝕂) {lOper : ℤ → V →ₗ[𝕂] V} (lComm : ∀ (n m : ℤ), (lOper n).commutator (lOper m) = (n - m) • lOper (n + m) + if n + m = 0 then (c / 12 * (↑n ^ 3 - ↑n)) • 1 else 0) : (representationOfCentralChargeOfL c lComm) (cgen 𝕂) = c • 1

theorem VirasoroProject.VirasoroAlgebra.representationOfCentralChargeOfL_lgen {𝕂 : Type u_3} [Field 𝕂] [CharZero 𝕂] {V : Type u_4} [AddCommGroup V] [Module 𝕂 V] (c : 𝕂) {lOper : ℤ → V →ₗ[𝕂] V} (lComm : ∀ (n m : ℤ), (lOper n).commutator (lOper m) = (n - m) • lOper (n + m) + if n + m = 0 then (c / 12 * (↑n ^ 3 - ↑n)) • 1 else 0) (n : ℤ) : (representationOfCentralChargeOfL c lComm) (lgen 𝕂 n) = lOper n

noncomputable def VirasoroProject.sugawaraRepresentation {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] {heiOper : ℤ → V →ₗ[𝕜] V} (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) (heiComm : ∀ (k l : ℤ), (heiOper k).commutator (heiOper l) = if k + l = 0 then ↑k • 1 else 0) [CharZero 𝕜] : VirasoroAlgebra 𝕜 →ₗ⁅𝕜⁆ V →ₗ[𝕜] V

The basic bosonic Sugawara representation of Virasoro algebra (c=1): On a vector space with a representation of the Heisenberg algebra that acts locally truncatedly, we get a representation of the Virasoro algebra with central charge 1 by the Sugawara construction.

Equations

• VirasoroProject.sugawaraRepresentation heiTrunc heiComm = VirasoroProject.VirasoroAlgebra.representationOfCentralChargeOfL 1 ⋯

theorem VirasoroProject.sugawaraRepresentation_cgen {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] (heiOper : ℤ → V →ₗ[𝕜] V) (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) (heiComm : ∀ (k l : ℤ), (heiOper k).commutator (heiOper l) = if k + l = 0 then ↑k • 1 else 0) [CharZero 𝕜] : (sugawaraRepresentation heiTrunc heiComm) (VirasoroAlgebra.cgen 𝕜) = 1

The central element C of the Virasoro algebra acts as 1 on the representation obtained by the basic bosonic Sugawara construction.

theorem VirasoroProject.sugawaraRepresentation_lgen_apply' {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] (heiOper : ℤ → V →ₗ[𝕜] V) (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) (heiComm : ∀ (k l : ℤ), (heiOper k).commutator (heiOper l) = if k + l = 0 then ↑k • 1 else 0) [CharZero 𝕜] (n : ℤ) (v : V) : ((sugawaraRepresentation heiTrunc heiComm) (VirasoroAlgebra.lgen 𝕜 n)) v = 2⁻¹ • ∑ᶠ (k : ℤ), (pairNO heiOper (n - k) k) v

The formula for the action of the Virasoro generator Lₙ on the representation obtained by the basic bosonic Sugawara construction.

theorem VirasoroProject.sugawaraRepresentation_lgen_apply {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] (heiOper : ℤ → V →ₗ[𝕜] V) (heiTrunc : ∀ (v : V), ∀ᶠ (l : ℤ) in Filter.atTop, (heiOper l) v = 0) (heiComm : ∀ (k l : ℤ), (heiOper k).commutator (heiOper l) = if k + l = 0 then ↑k • 1 else 0) [CharZero 𝕜] (n : ℤ) (v : V) : ((sugawaraRepresentation heiTrunc heiComm) (VirasoroAlgebra.lgen 𝕜 n)) v = 2⁻¹ • (∑ᶠ (k : ℤ) (_ : k ≥ 0), (heiOper (n - k) ∘ₗ heiOper k) v + ∑ᶠ (k : ℤ) (_ : k < 0), (heiOper k ∘ₗ heiOper (n - k)) v)

The formula for the action of the Virasoro generator Lₙ on the representation obtained by the basic bosonic Sugawara construction.

noncomputable def VirasoroProject.sugawaraRepresentationOfRepresentationHeisenbergAlgebra {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] [CharZero 𝕜] (α : LieAlgebra.Representation 𝕜 𝕜 (HeisenbergAlgebra 𝕜) V) (hα : ∀ (v : V), ∀ᶠ (k : ℤ) in Filter.atTop, (α (HeisenbergAlgebra.jgen 𝕜 k)) v = 0) (hαc : α (HeisenbergAlgebra.kgen 𝕜) = 1) : LieAlgebra.Representation 𝕜 𝕜 (VirasoroAlgebra 𝕜) V

The basic bosonic Sugawara representation of Virasoro algebra (c=1): On a vector space with a representation of the Heisenberg algebra that 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.sugawaraRepresentationOfRepresentationHeisenbergAlgebra α hα hαc = VirasoroProject.sugawaraRepresentation hα ⋯