-
Notifications
You must be signed in to change notification settings - Fork 383
/
Copy pathHVertexOperator.lean
157 lines (127 loc) · 5.7 KB
/
HVertexOperator.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
/-
Copyright (c) 2024 Scott Carnahan. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Carnahan
-/
import Mathlib.RingTheory.HahnSeries.Multiplication
/-!
# 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
* `HVertexOperator` : An `R`-linear map from an `R`-module `V` to `HahnModule Γ W`.
* The coefficient function as an `R`-linear map.
* Composition of heterogeneous vertex operators - values are Hahn series on lex order product.
## Main results
* Ext
## TODO
* `HahnSeries Γ R`-module structure on `HVertexOperator Γ R V W` (needs PR#10846). This means we
can consider products of the form `(X-Y)^n A(X)B(Y)` for all integers `n`, where `(X-Y)^n` is
expanded as `X^n(1-Y/X)^n` in `R((X))((Y))`.
* curry for tensor product inputs
* more API to make ext comparisons easier.
* formal variable API, e.g., like the `T` function for Laurent polynomials.
## References
* [R. Borcherds, *Vertex Algebras, Kac-Moody Algebras, and the Monster*][borcherds1986vertex]
-/
noncomputable section
variable {Γ : Type*} [PartialOrder Γ] {R : Type*} {V W : Type*} [CommRing R]
[AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W]
/-- 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`. -/
abbrev HVertexOperator (Γ : Type*) [PartialOrder Γ] (R : Type*) [CommRing R]
(V : Type*) (W : Type*) [AddCommGroup V] [Module R V] [AddCommGroup W] [Module R W] :=
V →ₗ[R] (HahnModule Γ R W)
namespace HVertexOperator
section Coeff
open HahnModule
@[ext]
theorem ext (A B : HVertexOperator Γ R V W) (h : ∀ v : V, A v = B v) :
A = B := LinearMap.ext h
@[deprecated (since := "2024-06-18")] alias _root_.VertexAlg.HetVertexOperator.ext := ext
/-- The coefficient of a heterogeneous vertex operator, viewed as a formal power series with
coefficients in linear maps. -/
@[simps]
def coeff (A : HVertexOperator Γ R V W) (n : Γ) : V →ₗ[R] W where
toFun v := ((of R).symm (A v)).coeff n
map_add' _ _ := by simp
map_smul' _ _ := by
simp only [map_smul, RingHom.id_apply]
exact rfl
@[deprecated (since := "2024-06-18")] alias _root_.VertexAlg.coeff := coeff
theorem coeff_isPWOsupport (A : HVertexOperator Γ R V W) (v : V) :
((of R).symm (A v)).coeff.support.IsPWO :=
((of R).symm (A v)).isPWO_support'
@[deprecated (since := "2024-06-18")]
alias _root_.VertexAlg.coeff_isPWOsupport := coeff_isPWOsupport
@[ext]
theorem coeff_inj : Function.Injective (coeff : HVertexOperator Γ R V W → Γ → (V →ₗ[R] W)) := by
intro _ _ h
ext v n
exact congrFun (congrArg DFunLike.coe (congrFun h n)) v
@[deprecated (since := "2024-06-18")] alias _root_.VertexAlg.coeff_inj := coeff_inj
/-- Given a coefficient function valued in linear maps satisfying a partially well-ordered support
condition, we produce a heterogeneous vertex operator. -/
@[simps]
def of_coeff (f : Γ → V →ₗ[R] W)
(hf : ∀(x : V), (Function.support (f · x)).IsPWO) : HVertexOperator Γ R V W where
toFun x := (of R) { coeff := fun g => f g x, isPWO_support' := hf x }
map_add' _ _ := by
ext
simp
map_smul' _ _ := by
simp only [map_smul, RingHom.id_apply]
exact rfl
@[deprecated (since := "2024-06-18")] alias _root_.VertexAlg.HetVertexOperator.of_coeff := of_coeff
end Coeff
section Products
variable {Γ Γ' : Type*} [OrderedCancelAddCommMonoid Γ] [OrderedCancelAddCommMonoid Γ'] {R : Type*}
[CommRing R] {U V W : Type*} [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)
open HahnModule
/-- The composite of two heterogeneous vertex operators acting on a vector, as an iterated Hahn
series. -/
@[simps]
def compHahnSeries (u : U) : HahnSeries Γ' (HahnSeries Γ W) where
coeff g' := A (coeff B g' u)
isPWO_support' := by
refine Set.IsPWO.mono (((of R).symm (B u)).isPWO_support') ?_
simp_all only [coeff_apply, Function.support_subset_iff, ne_eq, Function.mem_support]
intro g' hg' hAB
apply hg'
simp_rw [hAB]
simp_all only [map_zero, HahnSeries.zero_coeff, not_true_eq_false]
@[simp]
theorem compHahnSeries_add (u v : U) :
compHahnSeries A B (u + v) = compHahnSeries A B u + compHahnSeries A B v := by
ext
simp only [compHahnSeries_coeff, map_add, coeff_apply, HahnSeries.add_coeff', Pi.add_apply]
rw [← @HahnSeries.add_coeff]
@[simp]
theorem compHahnSeries_smul (r : R) (u : U) :
compHahnSeries A B (r • u) = r • compHahnSeries A B u := by
ext
simp only [compHahnSeries_coeff, LinearMapClass.map_smul, coeff_apply, HahnSeries.smul_coeff]
exact rfl
/-- The composite of two heterogeneous vertex operators, as a heterogeneous vertex operator. -/
@[simps]
def comp : HVertexOperator (Γ' ×ₗ Γ) R U W where
toFun u := HahnModule.of R (HahnSeries.ofIterate (compHahnSeries A B u))
map_add' := by
intro u v
ext g
simp only [HahnSeries.ofIterate, compHahnSeries_add, Equiv.symm_apply_apply,
HahnModule.of_symm_add, HahnSeries.add_coeff', Pi.add_apply]
map_smul' := by
intro r x
ext g
simp only [HahnSeries.ofIterate, compHahnSeries_smul, Equiv.symm_apply_apply, RingHom.id_apply,
HahnSeries.smul_coeff, compHahnSeries_coeff, coeff_apply]
exact rfl
@[simp]
theorem comp_coeff (g : Γ' ×ₗ Γ) :
(comp A B).coeff g = A.coeff (ofLex g).2 ∘ₗ B.coeff (ofLex g).1 := by
rfl
end Products
end HVertexOperator