English
Given a coefficient function f: Γ → V → W with a partial well-ordered support condition hf, the construction of an operator from these coefficients, called of_coeff f hf, yields a heterogeneous vertex operator whose coeff map is exactly f.
Русский
Дано f: Γ → V → W и hf, задающее частично упорядоченную опорность, отображение of_coeff f hf восстанавливает исходный коэффициентный функционал.
LaTeX
$$$\text{of_coeff}: (f:Γ\to V\to W) \to (hf: \forall x, (\text{support}(f·x)).IsPWO) \to HVertexOperator(\Gamma,R,V,W)$$$
Lean4
/-- 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 ext; simp
