English
The coefficients of a heterogeneous vertex operator form a linear map from HVertexOperator Γ R V W to Γ → (V → W); concretely, coeff assigns to each A ∈ HVertexOperator a family of linear maps indexed by Γ, mapping V to W.
Русский
Коэффициенты гетерогенного вершинного оператора образуют линейное отображение from HVertexOperator(Γ,R,V,W) в Γ → (V → W); то есть coeff сопоставляет каждому A ∈ HVertexOperator семейство линейных отображений, индексируемых по Γ, отображающее V в W.
LaTeX
$$$\operatorname{coeff}: HVertexOperator(\Gamma,R,V,W) \to_{\mathbb{R}} \Gamma \to (V \to_{\mathbb{R}} W)$$$
Lean4
/-- 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)
