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
Instances For
    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
    theorem VertexOperator.ext_iff {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] {A B : VertexOperator R V} :
    A = B ∀ (v : V), A v = B v
    def VertexOperator.ncoeff {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] :

    The coefficient of a vertex operator under normalized indexing.

    Equations
    Instances For
      theorem VertexOperator.ncoeff_apply {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] (A : VertexOperator R V) (n : ) :

      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.
      Instances For
        @[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 : ) :
        @[deprecated map_add (since := "2025-08-30")]
        theorem VertexOperator.ncoeff_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 VertexOperator.ncoeff_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.

        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) :
        (ncoeff A 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
        Instances For
          @[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 : ) :
          ncoeff (of_coeff f hf) n = f (-n - 1)