English
For a heterogeneous vertex operator A and a vector v, the support of the coefficient function ((of R).symm (A v)).coeff is partially well-ordered (IsPWO).
Русский
Для оператора A и вектора v опорка функции коэффициентов ((of R).symm (A v)).coeff является частично упорядоченной по поддержке (IsPWO).
LaTeX
$$$\text{Supp}(((\mathrm{of}\ R).symm (A v)).\mathrm{coeff}) \;\text{IsPWO}$$$
Lean4
/-- The coefficients of a heterogeneous vertex operator, viewed as a linear map to formal power
series with coefficients in linear maps. -/
@[simps]
def coeff : HVertexOperator Γ R V W →ₗ[R] Γ → V →ₗ[R] W
where
toFun A
n :=
{ toFun v := ((of R).symm (A v)).coeff n
map_add' u v := by simp
map_smul' r v := by simp }
map_add' _ _ := by ext; simp
map_smul' _ _ := by ext; simp
