Heisenberg algebra

This file defines the Heisenberg algebra, as the one-dimensional central extension of a countably infinite dimensional abelian Lie algebra associated to a nontrivial 2-cocycle.

(The construction is mathematically boring, but the interesting part is the relation with Virasoro algebra: suitable positive energy representations of the Heisenberg algebra can be made into representations of the Virasoro algebra by a Sugawara construction.)

Main definitions

• HeisenbergAlgebra: The Heisenberg algebra.
• HeisenbergAlgebra.jgen: The (commonly used) elements Jₖ, k ∈ ℤ, of the Heisenberg algebra.
• HeisenbergAlgebra.kgen: The central element K of the Heisenberg algebra (commonly set to 1 in representations).
• HeisenbergAlgebra.basisJK: The basis of the Heisenberg algebra consisting of Jₖ (k ∈ ℤ) and K.

Main statements

• HeisenbergAlgebra.instLieAlgebra: The Heisenberg algebra is a Lie algebra.

Implementation notes

The Heisenberg algebra is defined as a central extension of an infinite-dimensional abelian Lie algebra. (A more direct definition based on defining a Lie bracket on a countably infinite dimensional vector space would also be possible.)

Tags

Heisenberg algebra

Abelian Lie algebra with a given basis

def VirasoroProject.AbelianLieAlgebraOn (ι : Type u_1) (𝕜 : Type u_2) [CommRing 𝕜] : Type (max u_2 u_1)

An auxiliary construction of an abelian Lie algebra with a given index set for a basis.

Equations

• VirasoroProject.AbelianLieAlgebraOn ι 𝕜 = (ι →₀ 𝕜)

@[implicit_reducible]

noncomputable instance VirasoroProject.instAddCommGroupAbelianLieAlgebraOn (ι : Type u_1) (𝕜 : Type u_2) [CommRing 𝕜] : AddCommGroup (AbelianLieAlgebraOn ι 𝕜)

Equations

• VirasoroProject.instAddCommGroupAbelianLieAlgebraOn ι 𝕜 = Finsupp.instAddCommGroup

@[implicit_reducible]

noncomputable instance VirasoroProject.instModuleAbelianLieAlgebraOn (ι : Type u_1) (𝕜 : Type u_2) [CommRing 𝕜] : Module 𝕜 (AbelianLieAlgebraOn ι 𝕜)

Equations

• VirasoroProject.instModuleAbelianLieAlgebraOn ι 𝕜 = Finsupp.module ι 𝕜

noncomputable def VirasoroProject.AbelianLieAlgebraOn.jgen {ι : Type u_1} (𝕜 : Type u_2) [CommRing 𝕜] : Module.Basis ι 𝕜 (AbelianLieAlgebraOn ι 𝕜)

The basis of jᵢ generators of the abelian Lie algebra (indices i : ι).

Equations

• VirasoroProject.AbelianLieAlgebraOn.jgen 𝕜 = Finsupp.basisFun ι 𝕜

theorem VirasoroProject.AbelianLieAlgebraOn.jgen_eq_single {ι : Type u_1} (𝕜 : Type u_2) [CommRing 𝕜] (i : ι) : (jgen 𝕜) i = Finsupp.single i 1

@[implicit_reducible]

noncomputable instance VirasoroProject.AbelianLieAlgebraOn.instLieRing {ι : Type u_1} (𝕜 : Type u_2) [CommRing 𝕜] : LieRing (AbelianLieAlgebraOn ι 𝕜)

The Lie ring structure on the Witt algebra WittAlgebra.

Equations

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

@[simp]

theorem VirasoroProject.AbelianLieAlgebraOn.lie_def {ι : Type u_1} (𝕜 : Type u_2) [CommRing 𝕜] (X Y : AbelianLieAlgebraOn ι 𝕜) : ⁅X, Y⁆ = 0

@[implicit_reducible]

noncomputable instance VirasoroProject.AbelianLieAlgebraOn.instLieAlgebra {ι : Type u_1} (𝕜 : Type u_2) [CommRing 𝕜] : LieAlgebra 𝕜 (AbelianLieAlgebraOn ι 𝕜)

The Lie algebra structure on the Witt algebra WittAlgebra.

Equations

• VirasoroProject.AbelianLieAlgebraOn.instLieAlgebra 𝕜 = { toModule := VirasoroProject.instModuleAbelianLieAlgebraOn ι 𝕜, lie_smul := ⋯ }

instance VirasoroProject.AbelianLieAlgebraOn.instIsLieAbelian {ι : Type u_1} (𝕜 : Type u_2) [CommRing 𝕜] : IsLieAbelian (AbelianLieAlgebraOn ι 𝕜)

The 2-cocycle defining the Heisenberg algebra as central extension

noncomputable def VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycleBilin (𝕜 : Type u_1) [Field 𝕜] : AbelianLieAlgebraOn ℤ 𝕜 →ₗ[𝕜] AbelianLieAlgebraOn ℤ 𝕜 →ₗ[𝕜] 𝕜

A bilinear map version of the Heisenberg cocycle. (Defining equation: γ (jgen k) (jgen l) = k * δ[k+l,0].)

Equations

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

theorem VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycleBilin_apply_jgen_jgen (𝕜 : Type u_1) [Field 𝕜] (k l : ℤ) : ((heisenbergCocycleBilin 𝕜) ((jgen 𝕜) k)) ((jgen 𝕜) l) = ↑(if k + l = 0 then k else 0)

theorem VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycleBilin_eq_neg_flip (𝕜 : Type u_1) [Field 𝕜] : heisenbergCocycleBilin 𝕜 = -(heisenbergCocycleBilin 𝕜).flip

noncomputable def VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : LieTwoCocycle 𝕜 (AbelianLieAlgebraOn ℤ 𝕜) 𝕜

The Heisenberg cocycle.

Equations

• VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle 𝕜 = { toBilin := VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycleBilin 𝕜, self' := ⋯, leibniz' := ⋯ }

theorem VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle_apply_jgen_jgen (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (k l : ℤ) : ((heisenbergCocycle 𝕜) ((jgen 𝕜) k)) ((jgen 𝕜) l) = ↑(if k + l = 0 then k else 0)

theorem VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle_ne_zero (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : heisenbergCocycle 𝕜 ≠ 0

theorem VirasoroProject.AbelianLieAlgebraOn.cohomologyClass_heisenbergCocycle_ne_zero (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : (heisenbergCocycle 𝕜).cohomologyClass ≠ 0

The Heisenberg cocycle is cohomologically nontrivial.

theorem VirasoroProject.AbelianLieAlgebraOn.nontrivial_lieTwoCohomology (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : Nontrivial (LieTwoCohomology 𝕜 (AbelianLieAlgebraOn ℤ 𝕜) 𝕜)

The abelian Lie algebra 2-cohomology H²(AbelianLieAlgebraOn ℤ 𝕜, 𝕜) is nontrivial.

The Heisenberg (Lie) algebra

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

The Heisenberg algebra.

Equations

• VirasoroProject.HeisenbergAlgebra 𝕜 = (VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle 𝕜).CentralExtension

theorem VirasoroProject.HeisenbergAlgebra.ext' (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] {X Y : HeisenbergAlgebra 𝕜} (h₁ : X.1 = Y.1) (h₂ : X.2 = Y.2) : X = Y

@[implicit_reducible]

noncomputable instance VirasoroProject.HeisenbergAlgebra.instLieRing (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : LieRing (HeisenbergAlgebra 𝕜)

The Heisenberg algebra is a Lie ring.

Equations

• VirasoroProject.HeisenbergAlgebra.instLieRing 𝕜 = VirasoroProject.LieTwoCocycle.CentralExtension.instLieRing (VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle 𝕜)

@[implicit_reducible]

noncomputable instance VirasoroProject.HeisenbergAlgebra.instLieAlgebra (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : LieAlgebra 𝕜 (HeisenbergAlgebra 𝕜)

The Heisenberg algebra is a Lie algebra.

Equations

• VirasoroProject.HeisenbergAlgebra.instLieAlgebra 𝕜 = VirasoroProject.LieTwoCocycle.CentralExtension.instLieAlgebra (VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle 𝕜)

noncomputable def VirasoroProject.HeisenbergAlgebra.toAbelianLieAlgebraOn {𝕜 : Type u_1} [Field 𝕜] [CharZero 𝕜] : HeisenbergAlgebra 𝕜 →ₗ⁅𝕜⁆ AbelianLieAlgebraOn ℤ 𝕜

The projection from Heisenberg algebra to the original abelian Lie algebra.

Equations

• VirasoroProject.HeisenbergAlgebra.toAbelianLieAlgebraOn = VirasoroProject.LieTwoCocycle.CentralExtension.proj (VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle 𝕜)

noncomputable def VirasoroProject.HeisenbergAlgebra.ofCentral (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : 𝕜 →ₗ⁅𝕜⁆ HeisenbergAlgebra 𝕜

The embedding of central elements to Heisenberg algebra.

Equations

• VirasoroProject.HeisenbergAlgebra.ofCentral 𝕜 = VirasoroProject.LieTwoCocycle.CentralExtension.emb (VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle 𝕜)

theorem VirasoroProject.HeisenbergAlgebra.bracket_def' (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (X Y : HeisenbergAlgebra 𝕜) : ⁅X, Y⁆ = (⁅toAbelianLieAlgebraOn X, toAbelianLieAlgebraOn Y⁆, ((AbelianLieAlgebraOn.heisenbergCocycle 𝕜) (toAbelianLieAlgebraOn X)) (toAbelianLieAlgebraOn Y))

@[simp]

theorem VirasoroProject.HeisenbergAlgebra.bracket_fst (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (X Y : HeisenbergAlgebra 𝕜) : ⁅X, Y⁆.1 = 0

@[simp]

theorem VirasoroProject.HeisenbergAlgebra.bracket_snd (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (X Y : HeisenbergAlgebra 𝕜) : ⁅X, Y⁆.2 = ((AbelianLieAlgebraOn.heisenbergCocycle 𝕜) (toAbelianLieAlgebraOn X)) (toAbelianLieAlgebraOn Y)

theorem VirasoroProject.HeisenbergAlgebra.add_def' (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (X Y : HeisenbergAlgebra 𝕜) : X + Y = (X.1 + Y.1, X.2 + Y.2)

theorem VirasoroProject.HeisenbergAlgebra.smul_def' (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (c : 𝕜) (X : HeisenbergAlgebra 𝕜) : c • X = (c • X.1, c * X.2)

@[simp]

theorem VirasoroProject.HeisenbergAlgebra.add_fst (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (X Y : HeisenbergAlgebra 𝕜) : (X + Y).1 = X.1 + Y.1

@[simp]

theorem VirasoroProject.HeisenbergAlgebra.add_snd (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (X Y : HeisenbergAlgebra 𝕜) : (X + Y).2 = X.2 + Y.2

@[simp]

theorem VirasoroProject.HeisenbergAlgebra.smul_fst (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (c : 𝕜) (X : HeisenbergAlgebra 𝕜) : (c • X).1 = c • X.1

@[simp]

theorem VirasoroProject.HeisenbergAlgebra.smul_snd (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (c : 𝕜) (X : HeisenbergAlgebra 𝕜) : (c • X).2 = c * X.2

theorem VirasoroProject.HeisenbergAlgebra.isCentralExtension (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : LieAlgebra.IsCentralExtension (ofCentral 𝕜) toAbelianLieAlgebraOn

The Heisenberg algebra is a central extension of the Witt algebra.

noncomputable def VirasoroProject.HeisenbergAlgebra.jgen (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (k : ℤ) : HeisenbergAlgebra 𝕜

The (commonly used) Jₖ elements of the Heisenberg algebra, for k ∈ ℤ.

Equations

• VirasoroProject.HeisenbergAlgebra.jgen 𝕜 k = ((VirasoroProject.AbelianLieAlgebraOn.jgen 𝕜) k, 0)

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

The K central element of the Heisenberg algebra, which is commonly set to 1 (in representations).

Equations

• VirasoroProject.HeisenbergAlgebra.kgen 𝕜 = (VirasoroProject.HeisenbergAlgebra.ofCentral 𝕜) 1

theorem VirasoroProject.HeisenbergAlgebra.kgen_eq_ofCentral_one (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : kgen 𝕜 = (ofCentral 𝕜) 1

theorem VirasoroProject.HeisenbergAlgebra.kgen_eq' (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : kgen 𝕜 = (0, 1)

theorem VirasoroProject.HeisenbergAlgebra.jgen_eq' (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (k : ℤ) : jgen 𝕜 k = ((AbelianLieAlgebraOn.jgen 𝕜) k, 0)

@[simp]

theorem VirasoroProject.HeisenbergAlgebra.ofCentral_apply (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (a : 𝕜) : (ofCentral 𝕜) a = a • kgen 𝕜

theorem VirasoroProject.HeisenbergAlgebra.toAbelianLieAlgebraOn_kgen (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : toAbelianLieAlgebraOn (kgen 𝕜) = 0

@[simp]

theorem VirasoroProject.HeisenbergAlgebra.toAbelianLieAlgebraOn_jgen (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (n : ℤ) : toAbelianLieAlgebraOn (jgen 𝕜 n) = (AbelianLieAlgebraOn.jgen 𝕜) n

@[simp]

theorem VirasoroProject.HeisenbergAlgebra.lie_kgen (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (Z : HeisenbergAlgebra 𝕜) : ⁅kgen 𝕜, Z⁆ = 0

@[simp]

theorem VirasoroProject.HeisenbergAlgebra.lie_jgen (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (k l : ℤ) : ⁅jgen 𝕜 k, jgen 𝕜 l⁆ = if k + l = 0 then ↑k • kgen 𝕜 else 0

noncomputable def VirasoroProject.HeisenbergAlgebra.jsection (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : AbelianLieAlgebraOn ℤ 𝕜 →ₗ[𝕜] HeisenbergAlgebra 𝕜

A section of the standard projection from the Heisenberg algebra to the underlying abelian Lie algebra.

Equations

• VirasoroProject.HeisenbergAlgebra.jsection 𝕜 = VirasoroProject.LieTwoCocycle.CentralExtension.stdSection (VirasoroProject.AbelianLieAlgebraOn.heisenbergCocycle 𝕜)

@[simp]

theorem VirasoroProject.HeisenbergAlgebra.jsection_jgen (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (l : ℤ) : (jsection 𝕜) ((AbelianLieAlgebraOn.jgen 𝕜) l) = jgen 𝕜 l

noncomputable def VirasoroProject.HeisenbergAlgebra.basisJK (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : Module.Basis (Option ℤ) 𝕜 (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.)

Equations

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

@[simp]

theorem VirasoroProject.HeisenbergAlgebra.basisJK_some (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (l : ℤ) : (basisJK 𝕜) (some l) = jgen 𝕜 l

@[simp]

theorem VirasoroProject.HeisenbergAlgebra.basisJK_none (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : (basisJK 𝕜) none = kgen 𝕜

@[simp]

theorem VirasoroProject.HeisenbergAlgebra.lie_jgen_zero (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (Z : HeisenbergAlgebra 𝕜) : ⁅jgen 𝕜 0, Z⁆ = 0

J₀ is central