English
The composite of two heterogeneous vertex operators, as a single heterogeneous vertex operator, with index in Lex(Prod Γ' Γ).
Русский
Сложение двух гетерогенных вершинных операторов в виде одного гетерогенного вершинного оператора с индексом в Lex(Prod Γ' Γ).
LaTeX
$$$\mathrm{comp}: HVertexOperator(Γ) \to HVertexOperator(\mathrm{Lex}(\mathrm{Prod}(Γ',Γ)))$$$
Lean4
/-- 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 [HahnSeries.ofIterate]
map_smul' := by
intro r x
ext g
simp [HahnSeries.ofIterate]
