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.
• Composition of heterogeneous vertex operators - values are Hahn series on lex order product.

Main results

• Ext

TODO

• curry for tensor product inputs
• 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 HVertexOperator.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 B : HVertexOperator Γ R V W) (h : ∀ (v : V), A v = B v) : A = B

theorem HVertexOperator.ext_iff {Γ : 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 B : HVertexOperator Γ R V W} : A = B ↔ ∀ (v : V), A v = B v

def HVertexOperator.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] : HVertexOperator Γ R V W →ₗ[R] Γ → V →ₗ[R] W

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

Equations

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

@[simp]

theorem HVertexOperator.coeff_apply_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 : Γ) (v : V) : (coeff A n) v = ((HahnModule.of R).symm (A v)).coeff n

theorem HVertexOperator.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 ((HahnModule.of R).symm (A v)).coeff).IsPWO

theorem HVertexOperator.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 ⇑coeff

theorem HVertexOperator.coeff_inj_iff {Γ : 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₁ a₂ : HVertexOperator Γ R V W} : a₁ = a₂ ↔ coeff a₁ = coeff a₂

def HVertexOperator.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

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

@[simp]

theorem HVertexOperator.of_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] (f : Γ → V →ₗ[R] W) (hf : ∀ (x : V), (Function.support fun (x_1 : Γ) => (f x_1) x).IsPWO) (x : V) : (of_coeff f hf) x = (HahnModule.of R) { coeff := fun (g : Γ) => (f g) x, isPWO_support' := ⋯ }

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

theorem HVertexOperator.coeff_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 HVertexOperator.coeff_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.

@[simp]

theorem HVertexOperator.coeff_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 (g : Γ) => (f g) x).IsPWO) : coeff (of_coeff f hf) = f

@[simp]

theorem HVertexOperator.of_coeff_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) : of_coeff (coeff A) ⋯ = A

def HVertexOperator.compHahnSeries {Γ : Type u_5} {Γ' : Type u_6} [PartialOrder Γ] [PartialOrder Γ'] {R : Type u_7} [CommRing R] {U : Type u_8} {V : Type u_9} {W : Type u_10} [AddCommGroup U] [Module R U] [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W] (A : HVertexOperator Γ R V W) (B : HVertexOperator Γ' R U V) (u : U) : HahnSeries Γ' (HahnSeries Γ W)

The composite of two heterogeneous vertex operators acting on a vector, as an iterated Hahn series.

Equations

• A.compHahnSeries B u = { coeff := fun (g' : Γ') => A ((HVertexOperator.coeff B g') u), isPWO_support' := ⋯ }

@[simp]

theorem HVertexOperator.compHahnSeries_coeff {Γ : Type u_5} {Γ' : Type u_6} [PartialOrder Γ] [PartialOrder Γ'] {R : Type u_7} [CommRing R] {U : Type u_8} {V : Type u_9} {W : Type u_10} [AddCommGroup U] [Module R U] [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W] (A : HVertexOperator Γ R V W) (B : HVertexOperator Γ' R U V) (u : U) (g' : Γ') : (A.compHahnSeries B u).coeff g' = A ((coeff B g') u)

@[simp]

theorem HVertexOperator.compHahnSeries_add {Γ : Type u_5} {Γ' : Type u_6} [PartialOrder Γ] [PartialOrder Γ'] {R : Type u_7} [CommRing R] {U : Type u_8} {V : Type u_9} {W : Type u_10} [AddCommGroup U] [Module R U] [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W] (A : HVertexOperator Γ R V W) (B : HVertexOperator Γ' R U V) (u v : U) : A.compHahnSeries B (u + v) = A.compHahnSeries B u + A.compHahnSeries B v

@[simp]

theorem HVertexOperator.compHahnSeries_smul {Γ : Type u_5} {Γ' : Type u_6} [PartialOrder Γ] [PartialOrder Γ'] {R : Type u_7} [CommRing R] {U : Type u_8} {V : Type u_9} {W : Type u_10} [AddCommGroup U] [Module R U] [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W] (A : HVertexOperator Γ R V W) (B : HVertexOperator Γ' R U V) (r : R) (u : U) : A.compHahnSeries B (r • u) = r • A.compHahnSeries B u

def HVertexOperator.comp {Γ : Type u_5} {Γ' : Type u_6} [PartialOrder Γ] [PartialOrder Γ'] {R : Type u_7} [CommRing R] {U : Type u_8} {V : Type u_9} {W : Type u_10} [AddCommGroup U] [Module R U] [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W] (A : HVertexOperator Γ R V W) (B : HVertexOperator Γ' R U V) : HVertexOperator (Lex (Γ' × Γ)) R U W

The composite of two heterogeneous vertex operators, as a heterogeneous vertex operator.

Equations

• A.comp B = { toFun := fun (u : U) => (HahnModule.of R) (A.compHahnSeries B u).ofIterate, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem HVertexOperator.comp_apply {Γ : Type u_5} {Γ' : Type u_6} [PartialOrder Γ] [PartialOrder Γ'] {R : Type u_7} [CommRing R] {U : Type u_8} {V : Type u_9} {W : Type u_10} [AddCommGroup U] [Module R U] [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W] (A : HVertexOperator Γ R V W) (B : HVertexOperator Γ' R U V) (u : U) : (A.comp B) u = (HahnModule.of R) (A.compHahnSeries B u).ofIterate

@[simp]

theorem HVertexOperator.coeff_comp {Γ : Type u_5} {Γ' : Type u_6} [PartialOrder Γ] [PartialOrder Γ'] {R : Type u_7} [CommRing R] {U : Type u_8} {V : Type u_9} {W : Type u_10} [AddCommGroup U] [Module R U] [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W] (A : HVertexOperator Γ R V W) (B : HVertexOperator Γ' R U V) (g : Lex (Γ' × Γ)) : coeff (A.comp B) g = coeff A (ofLex g).2 ∘ₗ coeff B (ofLex g).1