Documentation

Mathlib.Algebra.Vertex.VertexOperator

Vertex operators #

In this file we introduce vertex operators as linear maps to Laurent series.

Definitions #

TODO #

References #

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

Equations
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
def VertexOperator.ncoeff {V : Type u_2} {R : Type u_3} [CommRing R] [AddCommGroup V] [Module R V] (A : VertexOperator R V) (n : ) :

The coefficient of a vertex operator under normalized indexing.

Equations

In the literature, the nth normalized coefficient of a vertex operator A is written as either Aₙ or A(n).

Equations
  • One or more equations did not get rendered due to their size.
@[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 : ) :
@[simp]
theorem VertexOperator.ncoeff_add {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (A B : VertexOperator R V) (n : ) :
(A + B).ncoeff n = A.ncoeff n + B.ncoeff n
@[simp]
theorem VertexOperator.ncoeff_smul {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (A : VertexOperator R V) (r : R) (n : ) :
(r A).ncoeff n = r A.ncoeff n
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) :
(A.ncoeff 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) :
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), ∃ (n : ), m < n, (f m) x = 0) :

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

Equations
@[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), ∃ (n : ), m < n, (f m) x = 0) (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), ∃ (n : ), m < n, (f m) x = 0) (n : ) :
(of_coeff f hf).ncoeff n = f (-n - 1)