Vertex operators

In this file we introduce heterogeneous vertex operators using Hahn series. When R = ℂ, V = W, and Γ = ℤ, then this is the usual notion of meromorphic left-moving 2D field. The notion we use here allows us to consider composites and scalar-multiply by multivariable Laurent series.

Definitions

• HVertexOperator : An R-linear map from an R-module V to HahnModule Γ W.
• The coefficient function as an R-linear map.

Main results

• Ext

To do:

• Composition of heterogeneous vertex operators - values are Hahn series on lex order product (needs PR#10781).
• HahnSeries Γ R-module structure on HVertexOperator Γ R V W (needs PR#10846). This means we can consider products of the form (X-Y)^n A(X)B(Y) for all integers n, where (X-Y)^n is expanded as X^n(1-Y/X)^n in R((X))((Y)).
• more API to make ext comparisons easier.
• formal variable API, e.g., like the T function for Laurent polynomials.

References

• [R. Borcherds, Vertex Algebras, Kac-Moody Algebras, and the Monster][borcherds1986vertex]

@[reducible, inline]

abbrev HVertexOperator (Γ : Type u_5) [PartialOrder Γ] (R : Type u_6) [CommRing R] (V : Type u_7) (W : Type u_8) [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W] : Type (max u_7 u_8 u_5)

A heterogeneous Γ-vertex operator over a commutator ring R is an R-linear map from an R-module V to Γ-Hahn series with coefficients in an R-module W.

Equations

• HVertexOperator Γ R V W = (V →ₗ[R] HahnModule Γ R W)

theorem VertexAlg.HetVertexOperator.ext {Γ : Type u_1} [PartialOrder Γ] {R : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing R] [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W] (A : HVertexOperator Γ R V W) (B : HVertexOperator Γ R V W) (h : ∀ (v : V), A v = B v) : A = B

@[simp]

theorem VertexAlg.coeff_apply {Γ : Type u_1} [PartialOrder Γ] {R : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing R] [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W] (A : HVertexOperator Γ R V W) (n : Γ) (x : V) : (VertexAlg.coeff A n) x = (A x).coeff n

def VertexAlg.coeff {Γ : Type u_1} [PartialOrder Γ] {R : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing R] [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W] (A : HVertexOperator Γ R V W) (n : Γ) : V →ₗ[R] W

The coefficient of a heterogeneous vertex operator, viewed as a formal power series with coefficients in linear maps.

Equations

• VertexAlg.coeff A n = { toFun := fun (x : V) => (A x).coeff n, map_add' := ⋯, map_smul' := ⋯ }

theorem VertexAlg.coeff_isPWOsupport {Γ : Type u_1} [PartialOrder Γ] {R : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing R] [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W] (A : HVertexOperator Γ R V W) (v : V) : (Function.support (A v).coeff).IsPWO

theorem VertexAlg.coeff_inj {Γ : Type u_1} [PartialOrder Γ] {R : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing R] [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W] : Function.Injective VertexAlg.coeff

@[simp]

theorem VertexAlg.HetVertexOperator.of_coeff_apply_coeff {Γ : Type u_1} [PartialOrder Γ] {R : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing R] [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W] (f : Γ → V →ₗ[R] W) (hf : ∀ (x : V), (Function.support fun (x_1 : Γ) => (f x_1) x).IsPWO) (x : V) (g : Γ) : ((VertexAlg.HetVertexOperator.of_coeff f hf) x).coeff g = (f g) x

def VertexAlg.HetVertexOperator.of_coeff {Γ : Type u_1} [PartialOrder Γ] {R : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing R] [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W] (f : Γ → V →ₗ[R] W) (hf : ∀ (x : V), (Function.support fun (x_1 : Γ) => (f x_1) x).IsPWO) : HVertexOperator Γ R V W

Given a coefficient function valued in linear maps satisfying a partially well-ordered support condition, we produce a heterogeneous vertex operator.

Equations

• VertexAlg.HetVertexOperator.of_coeff f hf = { toFun := fun (x : V) => { coeff := fun (g : Γ) => (f g) x, isPWO_support' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }