Vertex operators

In this file we introduce vertex operators as linear maps to Laurent series.

Definitions

• VertexOperator is an R-linear map from an R-module V to LaurentSeries V.
• VertexOperator.ncoeff is the coefficient of a vertex operator under normalized indexing.

TODO

• HasseDerivative : A divided-power derivative.
• Locality : A weak form of commutativity.
• Residue products : A family of products on VertexOperator R V parametrized by integers.

References

• G. Mason, Vertex rings and Pierce bundles
• A. Matsuo, K. Nagatomo, On axioms for a vertex algebra and locality of quantum fields

@[reducible, inline]

abbrev VertexOperator (R : Type u_3) (V : Type u_4) [CommRing R] [AddCommGroup V] [Module R V] : Type u_4

A vertex operator over a commutative ring R is an R-linear map from an R-module V to Laurent series with coefficients in V. We write this as a specialization of the heterogeneous case.

Equations

• VertexOperator R V = HVertexOperator ℤ R V V

theorem VertexOperator.ext {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (A B : VertexOperator R V) (h : ∀ (v : V), A v = B v) : A = B

def VertexOperator.ncoeff {V : Type u_2} {R : Type u_3} [CommRing R] [AddCommGroup V] [Module R V] (A : VertexOperator R V) (n : ℤ) : Module.End R V

The coefficient of a vertex operator under normalized indexing.

Equations

• A.ncoeff n = HVertexOperator.coeff A (-n - 1)

def VertexOperator.«term_[[_]]» : Lean.TrailingParserDescr

In the literature, the nth normalized coefficient of a vertex operator A is written as either Aₙ or A(n).

Equations

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

@[simp]

theorem VertexOperator.coeff_eq_ncoeff {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (A : VertexOperator R V) (n : ℤ) : HVertexOperator.coeff A n = A.ncoeff (-n - 1)

@[simp]

theorem VertexOperator.ncoeff_add {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (A B : VertexOperator R V) (n : ℤ) : (A + B).ncoeff n = A.ncoeff n + B.ncoeff n

@[simp]

theorem VertexOperator.ncoeff_smul {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (A : VertexOperator R V) (r : R) (n : ℤ) : (r • A).ncoeff n = r • A.ncoeff n

theorem VertexOperator.ncoeff_eq_zero_of_lt_order {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (A : VertexOperator R V) (n : ℤ) (x : V) (h : -n - 1 < ((HahnModule.of R).symm (A x)).order) : (A.ncoeff n) x = 0

theorem VertexOperator.coeff_eq_zero_of_lt_order {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (A : VertexOperator R V) (n : ℤ) (x : V) (h : n < ((HahnModule.of R).symm (A x)).order) : (HVertexOperator.coeff A n) x = 0

noncomputable def VertexOperator.of_coeff {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (f : ℤ → Module.End R V) (hf : ∀ (x : V), ∃ (n : ℤ), ∀ m < n, (f m) x = 0) : VertexOperator R V

Given an endomorphism-valued function on integers satisfying a pointwise bounded-pole condition, we produce a vertex operator.

Equations

• VertexOperator.of_coeff f hf = HVertexOperator.of_coeff f ⋯

@[simp]

theorem VertexOperator.of_coeff_apply_coeff {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (f : ℤ → Module.End R V) (hf : ∀ (x : V), ∃ (n : ℤ), ∀ m < n, (f m) x = 0) (x : V) (n : ℤ) : ((HahnModule.of R).symm ((VertexOperator.of_coeff f hf) x)).coeff n = (f n) x

@[simp]

theorem VertexOperator.ncoeff_of_coeff {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (f : ℤ → Module.End R V) (hf : ∀ (x : V), ∃ (n : ℤ), ∀ m < n, (f m) x = 0) (n : ℤ) : (VertexOperator.of_coeff f hf).ncoeff n = f (-n - 1)