Roadmap.txt

Outline for vertex algebras in Lean

Part I: Foundational requirements (add as necessary)

Power series:
For vertex algebras over a commutative ring R, we need power series in an R-module M lying in M[[z_1^{\pm 1}, \ldots, z_n^{\pm 1}]].
We may be able to make this work with iterated Hahn series.
For twisted modules, we need fractional powers (only used when suitable fractions and roots of unity lie in R).
For intertwining operators, we need "arbitrary powers" and logarithms.  Over C, "arbitrary" just means complex.

Operations:
For locality, we need multiplication by multivariable polynomials, in particular, (x-y)^N.
Isolating terms, e.g., y^n coefficient of an element of M[[x,y]][x^{-1}][\log x] as an element of M((x))[\log x]
Divided-power derivatives: z^{-n-1} coefficient of \partial^{(k)}A(z) is (-1)^k \binom{n}{k} A_{n-k}.
Pass between End(V)[[z^{\pm 1}]] + bounded-below condition and Hom(V, V((z))), and more generally between Hom(U,V){z} and Hom(U,V{z})
  (I guess currying is more or less automatic in Lean? Intertwining operators can be types of the form U \to V \to W{z} )
Composition of fields: Need a common space for comparing A(z)B(w) and B(w)A(z)
Residue products (do we need this for non-integral values?)
Some proofs that locality + derivative rule imply Borcherds use Laurent expansions of rational functions in 3 variables.

Cautions:
log series don't play well with divided power derivatives when ℚ is not contained in the coefficient ring, e.g., \partial^{(2)} (x^a log x) gets a 2 in the denominator.
This has not been a problem so far, since no one has worked with log intertwining operators over rings other than ℂ.
It might be interesting to see what kind of non-semisimple fusion structures exist over finite fields, but
maybe Lean is not the first place to try.

Part II: Suggestions (may need work)

New method: composition of fields A(x)B(y) lies in HahnSeries where exponents have lex ordering.  We get an automatic R((y))((x)) scalar multiplication action, which lets us expand (x-y)^{-n} A(x)B(y) in the natural domain, i.e., |x|>|y|.

Also, scalar multiplication makes it easy to say that order n locality implies order n+1 locality - just need (x-y) (x-y)^n A(x)B(y) = (x-y)^(n+1) A(x)B(y).  It's extremely cumbersome if we do it in terms of coefficients.

Need: expansions of rational functions like (x-y)^r (x-z)^s (y-z)^t as Hahn series for Matsuo-Nagatomo treatment of Cauchy-Jacobi.

Given an action of an additive monoid G on S, we have an action of the monoid ring of finitely supported maps from G to R.  Note: the coefficients are given by the sum in the formula (a.m)_k = \sum_{ij=k} a_i m_j, and if ij=k for fixed i and infinitely many j, this is infinite!!!  To fix this, we require that for each k \in S, act^{-1}(k) of G \times S has finite fibers over G.  See implementations of Algebra/Lie and Algebra/MonoidAlgebra.  (This may be too general)

Laurent power series - We consider the case where G and S are compatibly ordered. (I think this just means g < h implies g+s < h+s.)  In this case, we define a Laurent series to be a formal series whose support is bounded below in each G-congruence class.  We show that Laurent series are closed under the monoid algebra action.  (We only need ((x^{1/n})) in most cases.)

Part III: Field calculus

Field with variable z: R-module map from M to M((z)) [Li calls this a weak vertex operator].

Current draft implementation:

abbrev VertexOperator (R : Type*) (V : Type*) [CommRing R] [AddCommGroup V]
    [Module R V] := V →ₗ[R] LaurentSeries V

but maybe I want to make compositional and scalar infrastructure using the more general:

abbrev HetVertexOperator (Γ : Type*) (R : Type*) (V : Type*) (W : Type*) [PartialOrder Γ]
[CommRing R] [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W] := V →ₗ[R] HahnSeries Γ W

Old version:

structure FieldSeries : [Semiring R] [AddCommMonoid V] [Module R V] where
  coef: ℤ → Module.End R V
  truncation : ∀ v, ∃ N, ∀ n, N ≤ n → coef n v = 0.

Basic to do:

Define identity field I(z).  

Maybe don't define algebra of not-necessarily local fields.  Problem: without locality, the power series made of residue products is not necessarily a field.  What is Kac's definition of field algebra?  Just Y(u_n v,z) = Y(u,z)_n Y(v,z).

Theorem: \partial^{(k)}A(z)_n B(z) = (-1)^k\binom{n}{k}A(z)_{n-k}B(z)

Theorem: \partial^{(k)}(A(z)_nB(z)) = \sum \partial^{(i)}A(z)_n\partial^{(k-i)}B(z)

Theorem: A(z)_nI(z) = \partial^{(-n-1)}A(z) for n < 0 and 0 for n \geq 0.  I(z)_nA(z) = \delta_{n,-1}A(z).

Locality: Compare (z-w)^N A(z)B(w) with (z-w)^N B(w)A(z).
Make a map "multiplication by z-w", and consider its "eventual kernel".

Operator product expansion.

Cauchy-Jacobi identity - proof in Matsuo-Nagatomo uses expansions of rational functions.  Is there a proof by multi-index induction?

Borcherds identity for residue products - follows from Cauchy-Jacobi.

Vertex rng, non-unital vertex alg : Borcherds is equivalent to (locality or commutator formula) and (associativity or weak associativity)
-- maybe don't make these into a class - just define a notion of state-field correspondence Y, and define and compare properties of it.

Creativity with respect to a vector: A(z) vac has no singular part - preserved under residue products.

Vertex algebra: extends AddCommGroupWithOne V.  All Y(u,z) are creative with respect to 1, satisfy locality and associativity.

Basic properties with identity, Hasse-Schmidt derivations, translation-equivariance Y(T^(i)u,z) = \partial^{(i)}Y(u,z).

translation-covariance exp(yT)A(z)exp(-yT) = A(y+z) - preserved under residue products

Can replace locality or commutator with skew-symmetry.  Goddard's axiomatization (local + translation-covariance), Lian-Zuckerman axiomatization.

Part IV: Wish list - results I'd like to see

Goddard's uniqueness.

Explicit expansion of a_r b_s c (from Lepowsky-Li).

Reconstruction theorem - follows from Goddard.

Commutative rings with derivation are the same as commutative vertex algebras.  Manipulations with center and idempotents.  Commutants are vertex subalgebras.

Lie algebra structure on V_1/TV_0, special: tensoring with C[z,z^{-1}] to get Lie algebra of coefficients.  Enveloping topological associative algebra.

Standard examples: Heisenberg, Lattice, Affine - Heisenberg and affine need a treatment of fields from loop Lie algebras and induced modules.  Lattices need a theory of double covers, and possibly intertwining operators (do we want a construction of simple current extensions?)

Virasoro, conformal structure, Segal-Sugawara.

Vertex superalgebras, free fermions (first: super vector spaces and super modules).  Conway moonshine?  Boson-Fermion correspondence?

Cofiniteness conditions.  PBW-type bases.

Modules, intertwining operators, abelian intertwining algebra?

Preparation for moonshine: A_1^{24} Niemeier lattice (uses Golay code), Leech lattice, (simplicity of Co_1 needs analysis of norm 8 frames).  Distinguished S_4 action on N(A_1^{24}) vertex algebra.

Moonshine module (use triality to avoid some twisted operator manipulations - probably can't avoid all when defining multiplication), finiteness and simplicity of monster, no-ghost theorem, monster Lie algebra, complete replicability.

Ising, Miyamoto involutions.

Complex-analytic properties - differential equations following Huang and Miyamoto, associativity of C_1 fusion, Modularity following Zhu, DLM, Pseudo-trace properties of Miyamoto.

Hauptmodul criteria, monstrous moonshine, generalized moonshine.

Conformal blocks in genus zero - identification with intertwining operators following Zhu and Arike.

Conformal blocks in higher genus - analysis following damiolini-gibney-tarasca

Moduli of fs log-smooth curves (with branched G-covers and formal coordinates at marked points)

Verlinde formula, Modular tensor structure, regularity of fixed points, cyclic orbifolds.

Self-dual integral form of moonshine.

W-algebras?  Geometric Langlands questions?