6. Heisenberg algebra
In this section we assume that \bbk is a field of characteristic zero.
Heisenberg cocycle.
Let \gLie be the vector space with basis (j_k)_{k \in \bZ} over \bbk,
considered as an abelian Lie algebra.
The bilinear map {\gamma}_{\hei} \colon \gLie \times \gLie \to \bbk
given on basis elements by
\begin{aligned}
{\gamma}_{\hei}(j_k, j_l) = k \, \delta_{k+l,0}
\end{aligned}
is a Lie algebra 2-cocycle, {\gamma}_{\hei} \in C^2(\gLie,\bbk).
We call {\gamma}_{\hei} the Heisenberg cocycle.
Lean code for Definition6.1●1 definition
Associated Lean declarations
-
defdefined in VirasoroProject/HeisenbergAlgebra.leancomplete
def VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle.{u_1} (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : VirasoroProject.LieTwoCocycle 𝕜 (VirasoroProject.AbelianLieAlgebraOn ℤ 𝕜) 𝕜
def VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle.{u_1} (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : VirasoroProject.LieTwoCocycle 𝕜 (VirasoroProject.AbelianLieAlgebraOn ℤ 𝕜) 𝕜
The Heisenberg cocycle.
The Heisenberg cocyle is nontrivial.
The cohomology class [{\gamma}_{\hei}] \in H^2(\gLie,\bbk)
of the Heisenberg cocycle is nonzero.
Lean code for Lemma6.2●1 theorem
Associated Lean declarations
-
theoremdefined in VirasoroProject/HeisenbergAlgebra.leancomplete
theorem VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle_ne_zero.{u_1} (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle 𝕜 ≠ 0
theorem VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle_ne_zero.{u_1} (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle 𝕜 ≠ 0
…
Heisenberg algebra.
Let \bbk be a field of characteristic zero.
The Heisenberg algebra \hei is the Lie algebra over \bbk
obtained as the central extension of the abelian Lie algebra \gLie
with basis (j_k)_{k \in \bZ},
corresponding to the Heisenberg cocycle {\gamma}_{\hei} \in C^2(\gLie,\bbk).
Lean code for Definition6.3●3 declarations
Associated Lean declarations
-
defdefined in VirasoroProject/HeisenbergAlgebra.leancomplete
def VirasoroProject.HeisenbergAlgebra.{u_1} (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : Type u_1
def VirasoroProject.HeisenbergAlgebra.{u_1} (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : Type u_1
The Heisenberg algebra.
-
defdefined in VirasoroProject/HeisenbergAlgebra.leancomplete
def VirasoroProject.HeisenbergAlgebra.instLieAlgebra.{u_1} (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : LieAlgebra 𝕜 (VirasoroProject.HeisenbergAlgebra 𝕜)
def VirasoroProject.HeisenbergAlgebra.instLieAlgebra.{u_1} (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : LieAlgebra 𝕜 (VirasoroProject.HeisenbergAlgebra 𝕜)
The Heisenberg algebra is a Lie algebra.
-
theoremdefined in VirasoroProject/HeisenbergAlgebra.leancomplete
theorem VirasoroProject.HeisenbergAlgebra.isCentralExtension.{u_1} (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : VirasoroProject.LieAlgebra.IsCentralExtension (VirasoroProject.HeisenbergAlgebra.ofCentral 𝕜) VirasoroProject.HeisenbergAlgebra.toAbelianLieAlgebraOn
theorem VirasoroProject.HeisenbergAlgebra.isCentralExtension.{u_1} (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : VirasoroProject.LieAlgebra.IsCentralExtension (VirasoroProject.HeisenbergAlgebra.ofCentral 𝕜) VirasoroProject.HeisenbergAlgebra.toAbelianLieAlgebraOn
The Heisenberg algebra is a central extension of the Witt algebra.
From the definition of the Heisenberg algebra and the Heisenberg cocycle,
Definition 6.3 and Definition 6.1,
we directly obtain that \hei has a basis of the following form.
The standard basis of the Heisenberg algebra.
The Heisenberg algebra \hei has a basis consisting of (J_k)_{k \in \bZ}
and K, with Lie brackets determined by the following
\begin{aligned}
[J_k, J_l] = k \, \delta_{k+l,0} \, K , \quad
[K, J_k] = 0 , \quad
[K, K] = 0 ,
\end{aligned}
for k,l \in \bZ.
Lean code for Definition6.4●1 definition
Associated Lean declarations
-
defdefined in VirasoroProject/HeisenbergAlgebra.leancomplete
def VirasoroProject.HeisenbergAlgebra.basisJK.{u_1} (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : Module.Basis (Option ℤ) 𝕜 (VirasoroProject.HeisenbergAlgebra 𝕜)
def VirasoroProject.HeisenbergAlgebra.basisJK.{u_1} (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : Module.Basis (Option ℤ) 𝕜 (VirasoroProject.HeisenbergAlgebra 𝕜)
The most commonly used basis of the Heisenberg algebra, consisting of `Jₖ` (`k ∈ ℤ`) and the central element `K`. (Lean notation: `jgen _ k` and `kgen _`, respectively.)