Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Ordered monomial basis of a symmetric algebra

Statement

Let B be a supplied basis of V equipped with a supplied total order. The commutative monomials

b1⋯bn(b1≤⋯≤bn),

including the empty monomial 1, form a basis of S(V).

Facts & Assumptions

Given: A vector space V with a specified basis B and a specified total order on B.

[L2]

Linear maps V→A into commutative unital algebras extend uniquely to S(V) (Universal property of the symmetric algebra).

Proof

technique · constructive
1.1givenconstruct

Let P be the vector space freely spanned by the finite weakly increasing words in B, including the empty word. Multiply two basis words by sorting their concatenation. Totality of the supplied order makes the sorted word unique; this multiplication is commutative and associative, and the empty word is its unit.

2.1step 1.1L1L2construct

By [L1], sending b∈B to the one-letter word b extends uniquely to a linear map j:V→P. By [L2], it extends to a unital algebra map α:S(V)→P.

2.2step 1.1constructalgebra

Send each ordered word b1⋯bn in the basis of P to the product of the images of its letters in S(V), and send the empty word to 1. Extending linearly gives an algebra map β:P→S(V) because multiplication in S(V) is commutative and the product of two word images is the image of their sorted concatenation.

3.1step 2.1step 2.2L2

The composite αβ fixes every word-basis element of P, while βα fixes every generator from V and hence all of S(V) by [L2]. Thus α and β are inverse isomorphisms.

4.1step 3.1discharge-construct: step 1.1∎

Consequently the stated ordered words are a basis of S(V). The construction uses only the supplied basis and order, and when B is empty the empty word is the sole basis element.

Depends on

Dependency tree · 2 levels

Sources