The 2-cohomology of the Witt algebra is generated by the Virasoro cocycle

In this file it is proven that the 2-cohomology of the Witt algebra with scalar coefficients is one-dimensional and generated by the Virasoro cocycle.

Main statements

• WittAlgebra.exists_add_bdry_eq_smul_virasoroCocycle: Any Witt algebra 2-cocycle can be modified by a coboundary to make it proportional to the Virasoro cocycle.
• WittAlgebra.rank_lieTwoCohomology_eq_one: This is (the result of) the calculation of the dimension of the 2-cohomology of the Witt algebra, dim H²(WittAlgebra, 𝕜) = 1.

Tags

Witt algebra, Lie algebra cohomology

noncomputable def VirasoroProject.WittAlgebra.normalizingCochain {𝕜 : Type u_1} [Field 𝕜] [CharZero 𝕜] (γ : LieTwoCocycle 𝕜 (WittAlgebra 𝕜) 𝕜) : LieOneCochain 𝕜 (WittAlgebra 𝕜) 𝕜

A 1-cochain of the Witt algebra, which is used to make a 2-cocycle proportional to the Virasoro cocycle by the addition of the corresponding coboundary.

Equations

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

theorem VirasoroProject.WittAlgebra.normalizingCochain_apply_lgen_zero {𝕜 : Type u_1} [Field 𝕜] [CharZero 𝕜] (γ : LieTwoCocycle 𝕜 (WittAlgebra 𝕜) 𝕜) : (normalizingCochain γ) ((lgen 𝕜) 0) = -2⁻¹ * (γ ((lgen 𝕜) 1)) ((lgen 𝕜) (-1))

theorem VirasoroProject.WittAlgebra.normalizingCochain_apply_lgen {𝕜 : Type u_1} [Field 𝕜] [CharZero 𝕜] (γ : LieTwoCocycle 𝕜 (WittAlgebra 𝕜) 𝕜) (n : ℤ) (hn : n ≠ 0) : (normalizingCochain γ) ((lgen 𝕜) n) = 1 / ↑n * (γ ((lgen 𝕜) 0)) ((lgen 𝕜) n)

theorem VirasoroProject.WittAlgebra.add_bdry_normalizingCochain_apply_lgen_one {𝕜 : Type u_1} [Field 𝕜] [CharZero 𝕜] (γ : LieTwoCocycle 𝕜 (WittAlgebra 𝕜) 𝕜) : ((γ + (normalizingCochain γ).bdry) ((lgen 𝕜) 1)) ((lgen 𝕜) (-1)) = 0

theorem VirasoroProject.WittAlgebra.add_bdry_normalizingCochain_apply_lgen_zero {𝕜 : Type u_1} [Field 𝕜] [CharZero 𝕜] (γ : LieTwoCocycle 𝕜 (WittAlgebra 𝕜) 𝕜) (n : ℤ) (hn : n ≠ 0) : ((γ + (normalizingCochain γ).bdry) ((lgen 𝕜) 0)) ((lgen 𝕜) n) = 0

theorem VirasoroProject.WittAlgebra.add_lieTwoCocycle_apply_lgen_lgen_lgen_eq_zero {𝕜 : Type u_1} [Field 𝕜] [CharZero 𝕜] (γ : LieTwoCocycle 𝕜 (WittAlgebra 𝕜) 𝕜) (n m k : ℤ) : (↑m - ↑k) * (γ ((lgen 𝕜) n)) ((lgen 𝕜) (m + k)) + (↑k - ↑n) * (γ ((lgen 𝕜) m)) ((lgen 𝕜) (n + k)) + (↑n - ↑m) * (γ ((lgen 𝕜) k)) ((lgen 𝕜) (n + m)) = 0

The 2-cocycle equation in the standard basis ℓₙ of the Witt algebra: 0 = (m-k) * γ(n,m+k) + (k-n) * γ(m,n+k) + (n-m) * γ(k,n+m).

theorem VirasoroProject.WittAlgebra.lieTwoCocycle_apply_lgen_lgen_eq_zero_of_add_ne_zero {𝕜 : Type u_1} [Field 𝕜] [CharZero 𝕜] (γ : LieTwoCocycle 𝕜 (WittAlgebra 𝕜) 𝕜) {n m : ℤ} (ne_zero : n + m ≠ 0) (hγ : (γ ((lgen 𝕜) 0)) ((lgen 𝕜) (n + m)) = 0) : (γ ((lgen 𝕜) n)) ((lgen 𝕜) m) = 0

theorem VirasoroProject.WittAlgebra.exists_add_bdry_eq_smul_virasoroCocycle {𝕜 : Type u_1} [Field 𝕜] [CharZero 𝕜] (γ : LieTwoCocycle 𝕜 (WittAlgebra 𝕜) 𝕜) : ∃ (r : 𝕜), γ + (normalizingCochain γ).bdry = r • virasoroCocycle 𝕜

theorem VirasoroProject.WittAlgebra.rank_lieTwoCohomology_eq_one (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : Module.rank 𝕜 (LieTwoCohomology 𝕜 (WittAlgebra 𝕜) 𝕜) = 1

The Lie algebra 2-cohomology of the Witt algebra is one-dimensional, dim H²(WittAlgebra, 𝕜) = 1.