Documentation

Mathlib.Algebra.Vertex.HVertexOperator

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 #

Main results #

TODO #

References #

@[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
Instances For
    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.
    Instances For
      @[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) :
      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] :
      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) :

      Given a coefficient function valued in linear maps satisfying a partially well-ordered support condition, we produce a heterogeneous vertex operator.

      Equations
      Instances For
        @[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) :

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

        Equations
        Instances For
          @[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) :
          @[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) :
          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
          Instances For
            @[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) :
            @[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