From 90388b3c92811b0f05f506e231dfa4858d926d02 Mon Sep 17 00:00:00 2001 From: ScottCarnahan <128885296+ScottCarnahan@users.noreply.github.com> Date: Wed, 19 Jul 2023 07:29:59 +0900 Subject: [PATCH] Update Roadmap.txt Moved things into sections, made requirements more explicit. --- Roadmap.txt | 49 ++++++++++++++++++++++++++++++------------------- 1 file changed, 30 insertions(+), 19 deletions(-) diff --git a/Roadmap.txt b/Roadmap.txt index edd2721..3914521 100644 --- a/Roadmap.txt +++ b/Roadmap.txt @@ -1,36 +1,45 @@ Outline for vertex algebras in Lean -Introduce power series in a module M (over a rig R), allow multiple variables, allow shifts by multiplying powers of variables (i.e., allow Laurent polynomial action). More generally, formal power series M[[S]] in a module M with exponents in a set S should just be maps from S to M. +Part I: Foundational requirements (add as necessary) -Look at Lean4 mathlib files. Start with S arbitrary type, [Zero M] then [ZeroMul M], [AddCommMonoid M], [Module R M]. Then use instances to show that FormalSeriesModule inherits those structures. +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}]]. +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. -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. +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?) -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. +Part II: Suggestions (may need work) -Two maps M \to M[[S]] and M \to M[[T]] compose to form maps M \to M[[S \times T]] and M \to M[[T \times S]] by substitution of coefficients. +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. -Specialize to the case S = Z, maybe do something with a variable. +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. Say something about different expansions of m(x-y)^{-n} in M((x))((y)) and M((y))((x)), and how the difference is annihilated by (x-y)^n. -Field with variable z: R-module map from M to M((z)) [Li calls this a weak vertex operator]. -Define identity field. More generally, allow things that look like intertwining operators. Allow operations like taking the y^n coefficient of an element of M[[x,y]][x^{-1}][\log x] as an element of M((x))[\log x] - use preimage of projection to y-exponent set. +Part III: Field calculus -Operations: Addition, taking z^n term, shifting, divided power derivatives, -composition with fields in different variables, residue products +Field with variable z: R-module map from M to M((z)) [Li calls this a weak vertex operator]. +More generally, allow things that look like intertwining operators. +Define identity field I(z). -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). +-- 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)_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: \partial^{(k)}(A(z)_nB(z)) = \sum \partial^{(i)}A(z)_n\partial^{(k-i)}B(z) -Prop: 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). +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: There is some n \geq 0 such that -\sum \binom{n}{2i} z^{2i} w^{n-2i} A(z)B(w) = \sum \binom{n}{2i+1} z^{2i+1} w^{n-2i-1} B(w)A(z). -If we allow -1, then make a map "multiplication by z-w", and consider its "eventual kernel". +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. @@ -40,9 +49,11 @@ Borcherds identity for residue products Vertex rng, non-unital vertex alg : What axiomatizations are equivalent? Just locality + assoc -> can we get Jacobi? -Equivalent definitions of vertex algebra: Jacobi, locality + assoc, locality + translation, locality + weak assoc, weak assoc + skew, assoc + commutator, locality +Equivalent definitions of vertex algebra: Jacobi, locality + assoc, locality + translation, locality + weak assoc, weak assoc + skew, assoc + commutator + +Creativity with respect to a vector - preserved under residue products. (Lian-Zuckerman axiomatization) -Creativity with respect to a vector - preserved under residue products. +Part IV: Wish list - results I'd like to see Basic properties with identity, Hasse-Schmidt derivations. Goddard's uniqueness.