Update Roadmap.txt

Moved things into sections, made requirements more explicit.

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.