Theorems · Definition · nonassociative algebras

HVertexOperator.of_coeff

{Γ : Type u_1} →
  [inst : PartialOrder Γ] →
    {R : Type u_2} →
      {V : Type u_3} →
        {W : Type u_4} →
          [inst_1 : CommRing R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : Module R V] →
                [inst_4 : AddCommGroup W] →
                  [inst_5 : Module R W] →
                    (f : Γ → V →ₗ[R] W) →
                      (∀ (x : V), (Function.support fun x_1 => (f x_1) x).IsPWO) → HVertexOperator Γ R V W

Given a coefficient function valued in linear maps satisfying a partially well-ordered support condition, we produce a heterogeneous vertex operator.

Defined in

Mathlib.Algebra.Vertex.HVertexOperator

Cited by

3 results in Mathlib

Foundations

Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PartialOrderCommRingAddCommGroupModuleAddCommGroupModule