Witt algebra

This file defines the Witt algebra, an infinite-dimensional Lie algebra. A few assumptions are made of the ground ring 𝕜, mainly that it is of characteristic zero.

Typical interpretations of the Witt algebra are the following:

• In the case that the ground field is the real numbers, 𝕜 = ℝ, the Witt algebra is the Lie algebra of polynomial vector fields on the circle.
• In the case that the ground field is the complex numbers, 𝕜 = ℂ, the Witt algebra is the Lie algebra of meromorphic vector fields on the Riemann sphere with poles only at 0 and ∞.

Main definitions

• WittAlgebra: The Witt algebra.
• WittAlgebra.lgen: The (commonly used) basis {ℓₙ : n ∈ ℤ} of the Witt algebra.

Main statements

• WittAlgebra.instLieAlgebra: The Witt algebra is a Lie algebra.

Implementation notes

We define the Witt algebra based on an explicit basis indexed by the integers ℤ. This should be the most basic implementation.

TODO: Prove that the Witt algebra is isomorphic, e.g., to the Lie algebra of meromorphic vector fields on the Riemann sphere with poles only at 0 and ∞. (This of course needs some amount of differential geometry to be added to Lean.)

Tags

Witt algebra

def VirasoroProject.WittAlgebra (𝕜 : Type u_1) [CommRing 𝕜] : Type u_1

The Witt algebra: an ∞-dimensional Lie algebra (polynomial vector fields on a circle).

Equations

• VirasoroProject.WittAlgebra 𝕜 = (ℤ →₀ 𝕜)

@[implicit_reducible]

noncomputable instance VirasoroProject.instAddCommGroupWittAlgebra (𝕜 : Type u_1) [CommRing 𝕜] : AddCommGroup (WittAlgebra 𝕜)

Equations

• VirasoroProject.instAddCommGroupWittAlgebra 𝕜 = Finsupp.instAddCommGroup

@[implicit_reducible]

noncomputable instance VirasoroProject.instModuleWittAlgebra (𝕜 : Type u_1) [CommRing 𝕜] : Module 𝕜 (WittAlgebra 𝕜)

Equations

• VirasoroProject.instModuleWittAlgebra 𝕜 = Finsupp.module ℤ 𝕜

noncomputable def VirasoroProject.WittAlgebra.lgen (𝕜 : Type u_1) [CommRing 𝕜] : Module.Basis ℤ 𝕜 (WittAlgebra 𝕜)

The basis of ℓₙ generators of the Witt algebra (indices n : ℤ).

Equations

• VirasoroProject.WittAlgebra.lgen 𝕜 = Finsupp.basisFun ℤ 𝕜

theorem VirasoroProject.WittAlgebra.lgen_eq_single (𝕜 : Type u_1) [CommRing 𝕜] (n : ℤ) : (lgen 𝕜) n = Finsupp.single n 1

noncomputable def VirasoroProject.WittAlgebra.bracket (𝕜 : Type u_1) [CommRing 𝕜] : WittAlgebra 𝕜 →ₗ[𝕜] WittAlgebra 𝕜 →ₗ[𝕜] WittAlgebra 𝕜

The Lie bracket for the Witt algebra WittAlgebra as a bilinear map.

Equations

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

@[simp]

theorem VirasoroProject.WittAlgebra.bracket_lgen_lgen' (𝕜 : Type u_1) [CommRing 𝕜] (n m : ℤ) : ((bracket 𝕜) ((lgen 𝕜) n)) ((lgen 𝕜) m) = (↑n - ↑m) • (lgen 𝕜) (n + m)

⁅ℓ(n), ℓ(m)⁆ = (n-m) • ℓ(n+m) in WittAlgebra.

theorem VirasoroProject.WittAlgebra.bracket_eq_neg_flip (𝕜 : Type u_1) [CommRing 𝕜] : bracket 𝕜 = -(bracket 𝕜).flip

theorem VirasoroProject.WittAlgebra.bracket_antisymm {𝕜 : Type u_1} [CommRing 𝕜] (X Y : WittAlgebra 𝕜) : ((bracket 𝕜) X) Y = -((bracket 𝕜) Y) X

Antisymmetry of the Lie bracket of the Witt algebra WittAlgebra.

theorem VirasoroProject.WittAlgebra.bracket_self {𝕜 : Type u_1} [CommRing 𝕜] [CharZero 𝕜] [NoZeroSMulDivisors 𝕜 (WittAlgebra 𝕜)] (X : WittAlgebra 𝕜) : ((bracket 𝕜) X) X = 0

Antisymmetry (⁅X, X⁆ = 0 form) of the Lie bracket of the Witt algebra WittAlgebra.

theorem VirasoroProject.WittAlgebra.bracketCyclic_eq_zero (𝕜 : Type u_1) [CommRing 𝕜] : cyclicTripleSumHom (bracket 𝕜) (bracket 𝕜) = 0

The Jacobi identity of the Lie bracket of the Witt algebra WittAlgebra.

theorem VirasoroProject.WittAlgebra.bracket_leibniz {𝕜 : Type u_1} [CommRing 𝕜] (X Y Z : WittAlgebra 𝕜) : ((bracket 𝕜) X) (((bracket 𝕜) Y) Z) = ((bracket 𝕜) (((bracket 𝕜) X) Y)) Z + ((bracket 𝕜) Y) (((bracket 𝕜) X) Z)

The Leibniz property (Jacobi identity) of the Lie bracket of the Witt algebra WittAlgebra.

@[implicit_reducible]

noncomputable instance VirasoroProject.WittAlgebra.instLieRing {𝕜 : Type u_1} [CommRing 𝕜] [CharZero 𝕜] [NoZeroSMulDivisors 𝕜 (WittAlgebra 𝕜)] : LieRing (WittAlgebra 𝕜)

The Lie ring structure on the Witt algebra WittAlgebra.

Equations

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

@[implicit_reducible]

noncomputable instance VirasoroProject.WittAlgebra.instLieAlgebra {𝕜 : Type u_1} [CommRing 𝕜] [CharZero 𝕜] [NoZeroSMulDivisors 𝕜 (WittAlgebra 𝕜)] : LieAlgebra 𝕜 (WittAlgebra 𝕜)

The Lie algebra structure on the Witt algebra WittAlgebra.

Equations

• VirasoroProject.WittAlgebra.instLieAlgebra = { toModule := VirasoroProject.instModuleWittAlgebra 𝕜, lie_smul := ⋯ }

@[simp]

theorem VirasoroProject.WittAlgebra.bracket_lgen_lgen (𝕜 : Type u_1) [CommRing 𝕜] [CharZero 𝕜] [NoZeroSMulDivisors 𝕜 (WittAlgebra 𝕜)] (n m : ℤ) : ⁅(lgen 𝕜) n, (lgen 𝕜) m⁆ = (↑n - ↑m) • (lgen 𝕜) (n + m)

⁅ℓ(n), ℓ(m)⁆ = (n-m) • ℓ(n+m) in WittAlgebra.