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
: AnR
-linear map from anR
-moduleV
toHahnModule Γ W
.- The coefficient function as an
R
-linear map.
Main results #
- Ext
TODO #
- Composition of heterogeneous vertex operators - values are Hahn series on lex order product (needs PR#10781).
HahnSeries Γ R
-module structure onHVertexOperator Γ R V W
(needs PR#10846). This means we can consider products of the form(X-Y)^n A(X)B(Y)
for all integersn
, where(X-Y)^n
is expanded asX^n(1-Y/X)^n
inR((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)
Instances For
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 : Γ)
:
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' := ⋯ }
Instances For
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' := ⋯ }