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

• HahnSeries Γ R-module structure on HVertexOperator Γ R V W (needs https://github.com/leanprover-community/mathlib4/pull/19062. 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)).
• 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] (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

• A.coeff n = { toFun := fun (v : V) => ((HahnModule.of R).symm (A v)).coeff n, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem HVertexOperator.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 : Γ) (v : V) : (A.coeff 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₂ ↔ a₁.coeff = a₂.coeff

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' := ⋯ }

@[simp]

theorem HVertexOperator.coeff_add {Γ : 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).coeff = A.coeff + B.coeff

@[simp]

theorem HVertexOperator.coeff_smul {Γ : 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) (r : R) : (r • A).coeff = r • A.coeff

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 ((B.coeff 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 ((B.coeff 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 (Γ' × Γ)) : (A.comp B).coeff g = A.coeff (ofLex g).2 ∘ₗ B.coeff (ofLex g).1