The Virasoro 2-cocycle of the Witt algebra

This file defines the 2-cocycle of the Witt algebra with coefficients in ground field 𝕜, which defines the (unique) one-dimenensional central extension known as the Virasoro algebra. It is proven that the Virasoro cocycle is nontrivial, and in particular the cohomology of the Witt algebra in degree two does not vanish.

Main definitions

• WittAlgebra.virasoroCocycle: The 2-cocycle which defines the Virasoro algebra as a central extension of the Witt algebra and whose cohomology class generates H²(WittAlgebra, 𝕜).

Main statements

• WittAlgebra.cohomologyClass_virasoroCocycle_ne_zero: The cohomology class of the Virasoro cocycle is nonzero.
• WittAlgebra.nontrivial_lieTwoCohomology: The Witt algebra cohomology in degree two is nontrivial, H²(WittAlgebra, 𝕜) ≠ 0.

Tags

Witt algebra, Virasoro algebra, Lie algebra cohomology

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

A bilinear map version of the Virasoro cocycle. (Defining formula: γ (lgen n) (lgen m) = (n^3 - n) / 12 * δ[n+m,0].)

Equations

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

theorem VirasoroProject.WittAlgebra.virasoroCocycleBilin_apply_lgen_lgen (𝕜 : Type u_1) [Field 𝕜] (n m : ℤ) : ((virasoroCocycleBilin 𝕜) ((lgen 𝕜) n)) ((lgen 𝕜) m) = if n + m = 0 then (↑n ^ 3 - ↑n) / 12 else 0

theorem VirasoroProject.WittAlgebra.virasoroCocycleBilin_apply_lgen_lgen' (𝕜 : Type u_1) [Field 𝕜] (n m : ℤ) : ((virasoroCocycleBilin 𝕜) ((lgen 𝕜) n)) ((lgen 𝕜) m) = if n + m = 0 then (↑n - 1) * ↑n * (↑n + 1) / 12 else 0

theorem VirasoroProject.WittAlgebra.virasoroCocycleBilin_eq_neg_flip (𝕜 : Type u_1) [Field 𝕜] : virasoroCocycleBilin 𝕜 = -(virasoroCocycleBilin 𝕜).flip

theorem VirasoroProject.WittAlgebra.virasoroCocycleBracketCyclic_eq_zero (𝕜 : Type u_1) [Field 𝕜] : cyclicTripleSumHom (bracket 𝕜) (virasoroCocycleBilin 𝕜) = 0

An auxiliary for of the Leibniz identity of the Virasoro cocycle WittAlgebra.

noncomputable def VirasoroProject.WittAlgebra.virasoroCocycle (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : LieTwoCocycle 𝕜 (WittAlgebra 𝕜) 𝕜

The Virasoro cocycle.

Equations

• VirasoroProject.WittAlgebra.virasoroCocycle 𝕜 = { toBilin := VirasoroProject.WittAlgebra.virasoroCocycleBilin 𝕜, self' := ⋯, leibniz' := ⋯ }

theorem VirasoroProject.WittAlgebra.virasoroCocycle_apply_lgen_lgen (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] (n m : ℤ) : ((virasoroCocycle 𝕜) ((lgen 𝕜) n)) ((lgen 𝕜) m) = if n + m = 0 then (↑n ^ 3 - ↑n) / 12 else 0

theorem VirasoroProject.WittAlgebra.bdry_lgen_lgen_neg_eq {𝕜 : Type u_1} [Field 𝕜] [CharZero 𝕜] (β : LieOneCochain 𝕜 (WittAlgebra 𝕜) 𝕜) (n : ℤ) : (β.bdry ((lgen 𝕜) n)) ((lgen 𝕜) (-n)) = 2 * ↑n * β ((lgen 𝕜) 0)

theorem VirasoroProject.WittAlgebra.cohomologyClass_virasoroCocycle_ne_zero (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : (virasoroCocycle 𝕜).cohomologyClass ≠ 0

The Virasoro cocycle is cohomologically nontrivial.

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

The Witt algebra 2-cohomology H²(WittAlgebra, 𝕜) is nontrivial.