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][mason2017]
• [A. Matsuo, K. Nagatomo, On axioms for a vertex algebra and locality of quantum fields][matsuo1997]

@[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.

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

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

def VertexOperator.ncoeff {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] : VertexOperator R V →ₗ[R] ℤ → Module.End R V

The coefficient of a vertex operator under normalized indexing.

theorem VertexOperator.ncoeff_apply {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (A : VertexOperator R V) (n : ℤ) : ncoeff A 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).

@[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 = ncoeff A (-n - 1)

@[deprecated map_add (since := "2025-08-30")]

theorem VertexOperator.ncoeff_add {M : Type u_4} {N : Type u_5} {F : Type u_9} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] (f : F) (x y : M) : f (x + y) = f x + f y

Alias of map_add.

@[deprecated map_smul (since := "2025-08-30")]

theorem VertexOperator.ncoeff_smul {F : Type u_8} {M : Type u_9} {X : Type u_10} {Y : Type u_11} [SMul M X] [SMul M Y] [FunLike F X Y] [MulActionHomClass F M X Y] (f : F) (c : M) (x : X) : f (c • x) = c • f x

Alias of map_smul.

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) : (ncoeff A 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), BddBelow (Function.support fun (y : ℤ) => (f y) x)) : VertexOperator R V

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

@[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), BddBelow (Function.support fun (y : ℤ) => (f y) x)) (x : V) (n : ℤ) : ((HahnModule.of R).symm ((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), BddBelow (Function.support fun (y : ℤ) => (f y) x)) (n : ℤ) : ncoeff (of_coeff f hf) n = f (-n - 1)