VirasoroProject

8.2. Charged Fock spaces (Heisenberg Verma modules)🔗

Definition8.2.1
Statement uses 2
Statement dependency previews
Preview
Definition 6.4
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

Triangular decomposition of the Heisenberg algebra. A triangular decomposition

\begin{aligned} \hei = \hei^0 \oplus \hei^+ \oplus \hei^- \end{aligned}

of \hei is defined so that \hei^0 is spanned by J_0, K \in \hei, \hei^+ is spanned by J_k for k > 0, and \hei^- is spanned by J_k for k < 0.

(Without further comment, for the Heisenberg algebra we always use this triangular decomposition.)

Lean code for Definition8.2.1●1 definition
  • defdefined in VirasoroProject/FockSpace.lean
    complete
    def VirasoroProject.heisenbergTri.{u_1} (𝕜 : Type u_1) [Field 𝕜]
  [CharZero 𝕜] :
  VirasoroProject.TriangularDecomposition 𝕜
    (VirasoroProject.HeisenbergAlgebra 𝕜)
    def VirasoroProject.heisenbergTri.{u_1}
  (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] :
  VirasoroProject.TriangularDecomposition
    𝕜
    (VirasoroProject.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`.
Definition8.2.2
Statement uses 2
Statement dependency previews
Preview
Definition 7.2.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

Charged Fock space (Heisenberg Verma module). Let \alpha \in \bbk. The charged Fock space of charge \alpha is the Verma module \Verma^{\eta} associated to the linear functional \eta \colon \hei^0 \to \bbk with

\begin{aligned} \eta(J_0) = \alpha, \quad \eta(K) = 1 . \end{aligned}

We denote the charged Fock space by \FockSpace^{\alpha}. The highest weight vector \VermaHWV^{\eta} is (also) called the vacuum vector of the charged Fock space, and we denote it by \FockVacuum^{\alpha}.

Lean code for Definition8.2.2●1 definition
  • abbrevdefined in VirasoroProject/FockSpace.lean
    complete
    abbrev VirasoroProject.ChargedFockSpace.{u_1} (𝕜 : Type u_1) [Field 𝕜]
  [CharZero 𝕜] (α : 𝕜) : Type u_1
    abbrev VirasoroProject.ChargedFockSpace.{u_1}
  (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜]
  (α : 𝕜) : Type u_1
    The charged Fock space with charge `α`.
Lemma8.2.3
uses 1used by 1✓L∃∀N

Eventual commutation in the Heisenberg universal enveloping algebra. Let a \in \UEA(\hei) be an arbitrary element of the universal enveloping algebra of the Heisenberg algebra \hei. Then there exists a k_0=k_0(a) \in \bZ such that for all k \ge k_0 we have

\begin{aligned} J_k a = a J_k . \end{aligned}

Lean code for Lemma8.2.3●1 theorem
  • theoremdefined in VirasoroProject/FockSpace.lean
    complete
    theorem VirasoroProject.HeisenbergAlgebra.uea_eventually_commute_jgen.{u_1}
  (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜]
  (a : 𝓤 𝕜 (VirasoroProject.HeisenbergAlgebra 𝕜)) :
  ∀ᶠ (k : ℤ) in Filter.atTop,
    Commute ((ιUEA 𝕜) (VirasoroProject.HeisenbergAlgebra.jgen 𝕜 k)) a
    theorem VirasoroProject.HeisenbergAlgebra.uea_eventually_commute_jgen.{u_1}
  (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜]
  (a :
    𝓤 𝕜
      (VirasoroProject.HeisenbergAlgebra
        𝕜)) :
  ∀ᶠ (k : ℤ) in Filter.atTop,
    Commute
      ((ιUEA 𝕜)
        (VirasoroProject.HeisenbergAlgebra.jgen
          𝕜 k))
      a
Proof for Lemma 8.2.3
uses 0

Clear by the induction principle of the universal enveloping algebra and Lie brackets of the Heisenberg algebra basis elements.

Lemma8.2.4
uses 1used by 1✓L∃∀N

Local truncation condition for the charged Fock space. Let \alpha \in \bbk and let v \in \FockSpace^{\alpha} be a vector in the charged Fock space with charge \alpha. Then there exists a k_0 \in \bZ such that for all k \ge k_0 we have

\begin{aligned} J_k \, v = 0 . \end{aligned}

(In other words, the charged Fock space satisfies the local truncation condition \tagHeiTrunc{} needed for the Sugawara construction.)

Lean code for Lemma8.2.4●1 theorem
  • theoremdefined in VirasoroProject/FockSpace.lean
    complete
    theorem VirasoroProject.ChargedFockSpace.eventually_jgen_smul_eq_zero.{u_1}
  (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜)
  (v : VirasoroProject.ChargedFockSpace 𝕜 α) :
  ∀ᶠ (k : ℤ) in Filter.atTop,
    (ιUEA 𝕜) (VirasoroProject.HeisenbergAlgebra.jgen 𝕜 k) • v = 0
    theorem VirasoroProject.ChargedFockSpace.eventually_jgen_smul_eq_zero.{u_1}
  (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜]
  (α : 𝕜)
  (v :
    VirasoroProject.ChargedFockSpace 𝕜
      α) :
  ∀ᶠ (k : ℤ) in Filter.atTop,
    (ιUEA 𝕜)
          (VirasoroProject.HeisenbergAlgebra.jgen
            𝕜 k) •
        v =
      0
Proof for Lemma 8.2.4
uses 1

Straightforward by Lemma 8.2.3 and the properties of the highest weight vector (cyclicity and annihilation by the upper part).

Definition8.2.5
Statement uses 2
Statement dependency previews
Preview
Theorem 8.1.11
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

Virasoro action on the charged Fock space. The charged Fock space of charge \alpha becomes a representation of the Virasoro algebra \vir with central charge c = 1 via the Sugawara construction (Theorem 8.1.11).

Lean code for Definition8.2.5●2 definitions
  • defdefined in VirasoroProject/FockSpaceSugawara.lean
    complete
    def VirasoroProject.ChargedFockSpace.sugawaraRepresentation.{u_1}
  (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) :
  LieAlgebra.Representation 𝕜 𝕜 (VirasoroProject.VirasoroAlgebra 𝕜)
    (VirasoroProject.ChargedFockSpace 𝕜 α)
    def VirasoroProject.ChargedFockSpace.sugawaraRepresentation.{u_1}
  (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜]
  (α : 𝕜) :
  LieAlgebra.Representation 𝕜 𝕜
    (VirasoroProject.VirasoroAlgebra 𝕜)
    (VirasoroProject.ChargedFockSpace 𝕜 α)
    **Virasoro algebra representation on Fock space by basic bosonic Sugawara construction (c=1)**:
  • defdefined in VirasoroProject/FockSpaceSugawara.lean
    complete
    def VirasoroProject.ChargedFockSpace.instModuleUniversalEnvelopingAlgebraVirasoroAlgebra.{u_1}
  (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) :
  Module (𝓤 𝕜 (VirasoroProject.VirasoroAlgebra 𝕜))
    (VirasoroProject.ChargedFockSpace 𝕜 α)
    def VirasoroProject.ChargedFockSpace.instModuleUniversalEnvelopingAlgebraVirasoroAlgebra.{u_1}
  (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜]
  (α : 𝕜) :
  Module
    (𝓤 𝕜
      (VirasoroProject.VirasoroAlgebra 𝕜))
    (VirasoroProject.ChargedFockSpace 𝕜 α)
Lemma8.2.6
Statement uses 2
Statement dependency previews
Preview
Definition 7.3.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

The vacuum of the charged Fock space is a highest weight vector. The vacuum vector \FockVacuum^{\alpha} of the charged Fock space of charge \alpha \in \bbk satisfies

\begin{aligned} L_0 \, \FockVacuum^{\alpha} = \frac{\alpha^2}{2} \, \FockVacuum^{\alpha} \qquad \text{and} \qquad L_n \, \FockVacuum^{\alpha} = 0 \text{ for all } n > 0 . \end{aligned}

In particular (by the universal property of Verma modules) there exists a Virasoro-module map

\begin{aligned} \Verma^{c=1,h=\alpha^2/2} \to \FockSpace^{\alpha} \end{aligned}

such that \VermaHWV^{c=1,h=\alpha^2/2} \mapsto \FockVacuum^{\alpha}.

Lean code for Lemma8.2.6●3 declarations
  • theoremdefined in VirasoroProject/FockSpaceSugawara.lean
    complete
    theorem VirasoroProject.ChargedFockSpace.sugawaraRepresentation_lgen_zero_apply_vacuum.{u_1}
  (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) :
  ((VirasoroProject.ChargedFockSpace.sugawaraRepresentation 𝕜 α)
        (VirasoroProject.VirasoroAlgebra.lgen 𝕜 0))
      (VirasoroProject.ChargedFockSpace.vacuum 𝕜 α) =
    (α ^ 2 / 2) • VirasoroProject.ChargedFockSpace.vacuum 𝕜 α
    theorem VirasoroProject.ChargedFockSpace.sugawaraRepresentation_lgen_zero_apply_vacuum.{u_1}
  (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜]
  (α : 𝕜) :
  ((VirasoroProject.ChargedFockSpace.sugawaraRepresentation
          𝕜 α)
        (VirasoroProject.VirasoroAlgebra.lgen
          𝕜 0))
      (VirasoroProject.ChargedFockSpace.vacuum
        𝕜 α) =
    (α ^ 2 / 2) •
      VirasoroProject.ChargedFockSpace.vacuum
        𝕜 α
    The vacuum in the Fock space of charge α has L₀-eigenvalue α²/2.
  • theoremdefined in VirasoroProject/FockSpaceSugawara.lean
    complete
    theorem VirasoroProject.ChargedFockSpace.sugawaraRepresentation_lgen_pos_apply_vacuum.{u_1}
  (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) {n : ℤ}
  (n_pos : 0 < n) :
  ((VirasoroProject.ChargedFockSpace.sugawaraRepresentation 𝕜 α)
        (VirasoroProject.VirasoroAlgebra.lgen 𝕜 n))
      (VirasoroProject.ChargedFockSpace.vacuum 𝕜 α) =
    0
    theorem VirasoroProject.ChargedFockSpace.sugawaraRepresentation_lgen_pos_apply_vacuum.{u_1}
  (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜]
  (α : 𝕜) {n : ℤ} (n_pos : 0 < n) :
  ((VirasoroProject.ChargedFockSpace.sugawaraRepresentation
          𝕜 α)
        (VirasoroProject.VirasoroAlgebra.lgen
          𝕜 n))
      (VirasoroProject.ChargedFockSpace.vacuum
        𝕜 α) =
    0
    The vacuum in the Fock space of charge α is annihilated by Lₙ for n > 0.
  • defdefined in VirasoroProject/FockSpaceSugawara.lean
    complete
    def VirasoroProject.ChargedFockSpace.virasoroVermaToChargedFockSpace.{u_1}
  (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (α : 𝕜) :
  VirasoroProject.VirasoroVerma 𝕜 1
      (α ^ 2 / 2) →ₗ[𝓤 𝕜 (VirasoroProject.VirasoroAlgebra 𝕜)]
    VirasoroProject.ChargedFockSpace 𝕜 α
    def VirasoroProject.ChargedFockSpace.virasoroVermaToChargedFockSpace.{u_1}
  (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜]
  (α : 𝕜) :
  VirasoroProject.VirasoroVerma 𝕜 1
      (α ^ 2 /
        2) →ₗ[𝓤 𝕜
      (VirasoroProject.VirasoroAlgebra 𝕜)]
    VirasoroProject.ChargedFockSpace 𝕜 α
    A Virasoro module map from the Verma module with `c = 1` and `h = α^2 / 2`
to the charged Fock space of charge `α`.
Proof for Lemma 8.2.6
uses 1

Calculation.