The Virasoro algebra

This file defines the Virasoro algebra, an infinite-dimensional Lie algebra which is the unique one-dimensional central extension of the Witt algebra.

(In two-dimensional conformal field theory (CFT), the Virasoro algebra describes the effects of infinitesimal conformal transformations on the state space of the theory, or equivalently on its space of local fields.)

Main definitions

• VirasoroAlgebra: The Virasoro algebra.
• VirasoroAlgebra.lgen: The (commonly used) elements Lₙ, n ∈ ℤ, of the Virasoro algebra.
• VirasoroAlgebra.cgen: The (commonly used) central element C of the Virasoro algebra.
• VirasoroAlgebra.basisLC: The basis of the Virasoro algebra consisting of Lₙ (n ∈ ℤ) and C.
• VirasoroAlgebra.ofCentral and VirasoroAlgebra.toWittAlgebra: The maps in the short exact sequence 0 ⟶ 𝕜 ⟶ VirasoroAlgebra ⟶ WittAlgebra ⟶ 0.

Main statements

• VirasoroAlgebra.instLieAlgebra: The Virasoro algebra is a Lie algebra.
• VirasoroAlgebra.isCentralExtension: The Virasoro algebra is a cetral extension of the Witt algebra.

Implementation notes

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

Tags

Virasoro algebra

The Virasoro algebra

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

The Virasoro algebra.

Equations

• VirasoroProject.VirasoroAlgebra 𝕜 = (VirasoroProject.WittAlgebra.virasoroCocycle 𝕜).CentralExtension

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

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

The Virasoro algebra is a Lie ring.

Equations

• VirasoroProject.VirasoroAlgebra.instLieRing 𝕜 = VirasoroProject.LieTwoCocycle.CentralExtension.instLieRing (VirasoroProject.WittAlgebra.virasoroCocycle 𝕜)

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

The Virasoro algebra is a Lie algebra.

Equations

• VirasoroProject.VirasoroAlgebra.instLieAlgebra 𝕜 = VirasoroProject.LieTwoCocycle.CentralExtension.instLieAlgebra (VirasoroProject.WittAlgebra.virasoroCocycle 𝕜)

noncomputable def VirasoroProject.VirasoroAlgebra.toWittAlgebra {𝕜 : Type u_1} [Field 𝕜] [CharZero 𝕜] : VirasoroAlgebra 𝕜 →ₗ⁅𝕜⁆ WittAlgebra 𝕜

The projection from Virasoro algebra to Witt algebra.

Equations

• VirasoroProject.VirasoroAlgebra.toWittAlgebra = VirasoroProject.LieTwoCocycle.CentralExtension.proj (VirasoroProject.WittAlgebra.virasoroCocycle 𝕜)

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

The embedding of central elements to Virasoro algebra.

Equations

• VirasoroProject.VirasoroAlgebra.ofCentral 𝕜 = VirasoroProject.LieTwoCocycle.CentralExtension.emb (VirasoroProject.WittAlgebra.virasoroCocycle 𝕜)

theorem VirasoroProject.VirasoroAlgebra.bracket_def' (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (X Y : VirasoroAlgebra 𝕜) : ⁅X, Y⁆ = (⁅toWittAlgebra X, toWittAlgebra Y⁆, ((WittAlgebra.virasoroCocycle 𝕜) (toWittAlgebra X)) (toWittAlgebra Y))

@[simp]

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

@[simp]

theorem VirasoroProject.VirasoroAlgebra.bracket_snd (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (X Y : VirasoroAlgebra 𝕜) : ⁅X, Y⁆.2 = ((WittAlgebra.virasoroCocycle 𝕜) (toWittAlgebra X)) (toWittAlgebra Y)

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def VirasoroProject.VirasoroAlgebra.lgen (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (n : ℤ) : VirasoroAlgebra 𝕜

The (commonly used) Lₙ elements of the Virasoro algebra, for n ∈ ℤ.

Equations

• VirasoroProject.VirasoroAlgebra.lgen 𝕜 n = ((VirasoroProject.WittAlgebra.lgen 𝕜) n, 0)

noncomputable def VirasoroProject.VirasoroAlgebra.cgen (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : VirasoroAlgebra 𝕜

The (commonly used) C central element of the Virasoro algebra.

Equations

• VirasoroProject.VirasoroAlgebra.cgen 𝕜 = (VirasoroProject.VirasoroAlgebra.ofCentral 𝕜) 1

theorem VirasoroProject.VirasoroAlgebra.cgen_eq_ofCentral_one (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : cgen 𝕜 = (ofCentral 𝕜) 1

theorem VirasoroProject.VirasoroAlgebra.cgen_eq' (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : cgen 𝕜 = (0, 1)

theorem VirasoroProject.VirasoroAlgebra.lgen_eq' (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (n : ℤ) : lgen 𝕜 n = ((WittAlgebra.lgen 𝕜) n, 0)

@[simp]

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

@[simp]

theorem VirasoroProject.VirasoroAlgebra.toWittAlgebra_cgen (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : toWittAlgebra (cgen 𝕜) = 0

@[simp]

theorem VirasoroProject.VirasoroAlgebra.toWittAlgebra_lgen (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (n : ℤ) : toWittAlgebra (lgen 𝕜 n) = (WittAlgebra.lgen 𝕜) n

@[simp]

theorem VirasoroProject.VirasoroAlgebra.cgen_bracket (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (Z : VirasoroAlgebra 𝕜) : ⁅cgen 𝕜, Z⁆ = 0

@[simp]

theorem VirasoroProject.VirasoroAlgebra.bracket_cgen (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (Z : VirasoroAlgebra 𝕜) : ⁅Z, cgen 𝕜⁆ = 0

@[simp]

theorem VirasoroProject.VirasoroAlgebra.lgen_bracket (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (n m : ℤ) : ⁅lgen 𝕜 n, lgen 𝕜 m⁆ = (↑n - ↑m) • lgen 𝕜 (n + m) + if n + m = 0 then ((↑n ^ 3 - ↑n) / 12) • cgen 𝕜 else 0

theorem VirasoroProject.VirasoroAlgebra.lgen_bracket' (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (n m : ℤ) : ⁅lgen 𝕜 n, lgen 𝕜 m⁆ = (↑n - ↑m) • lgen 𝕜 (n + m) + if n + m = 0 then ((↑n - 1) * ↑n * (↑n + 1) / 12) • cgen 𝕜 else 0

noncomputable def VirasoroProject.VirasoroAlgebra.lsection (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : WittAlgebra 𝕜 →ₗ[𝕜] VirasoroAlgebra 𝕜

A section of the standard projection from the Virasoro algebra to the Witt algebra.

Equations

• VirasoroProject.VirasoroAlgebra.lsection 𝕜 = VirasoroProject.LieTwoCocycle.CentralExtension.stdSection (VirasoroProject.WittAlgebra.virasoroCocycle 𝕜)

@[simp]

theorem VirasoroProject.VirasoroAlgebra.lsection_lgen (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (n : ℤ) : (lsection 𝕜) ((WittAlgebra.lgen 𝕜) n) = lgen 𝕜 n

noncomputable def VirasoroProject.VirasoroAlgebra.basisLC (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : Module.Basis (Option ℤ) 𝕜 (VirasoroAlgebra 𝕜)

The most commonly used basis of the Virasoro algebra, consisting of Lₙ (n ∈ ℤ) and the central element C. (Lean notation: lgen _ n and cgen _, respectively.)

Equations

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

@[simp]

theorem VirasoroProject.VirasoroAlgebra.basisLC_some (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (n : ℤ) : (basisLC 𝕜) (some n) = lgen 𝕜 n

@[simp]

theorem VirasoroProject.VirasoroAlgebra.basisLC_none (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : (basisLC 𝕜) none = cgen 𝕜