TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

The column monomial basis of the higher-level Fock module

Statement

Work in the conventions of The higher-level wedge-tensor Fock module and The Fock-space convention dictionary for finite type-A quantum modules with source parameter $s$ .

(1) For a finite interval $[k, r]$ , the normally ordered wedges $v_{i_{1}} \land \dots \land v_{i_{d}}$ , $i_{1} > \dots > i_{d}$ , $i_{a} \in [k, r]$ , form an integral basis of the fundamental wedge $Λ^{d} V$ , where the wedge is the antisymmetrized tensor word with coefficients $(- s)^{ℓ (w)}$ over the symmetric group; the span is primitive over $Z [s^{\pm 1}]$ . This does not assert that the antisymmetrizer embedding into the raw tensor power is based in the library's lower $q_{0}$ chart.

(2) The column monomials $M_{A}$ , $A \in {C o l}^{Λ}$ , form a basis of the higher-level Fock module $F (Λ)$ on every finite cut, with the weights $w t (A)$ of the Definition.

(3) Let a finite interval $[k, r] \subseteq I^{+}$ be a cut containing all entries of a given monomial (upper cut), and $k - 1 < k$ a further lower residue; the lower-cut embedding $ι_{k}$ appends the common bottom entry $k - 1$ to each of the $l$ columns, $ι_{k} (M_{A}) = M_{A ⊔ (k - 1)^{l}}$ . The embeddings are injective, compatible with the monomial action, and their compatible direct limit over shrinking lower cuts and growing upper cuts is the full bounded or semi-infinite Fock module of the Definition.

(4) Every generator acts by finitely many box moves and shifts weight spaces; each fixed-weight space of $F (Λ)$ is finite dimensional. A merely lower-bounded infinite interval need not give finite-dimensional fundamental factors; all finite-Cartan statements are applied on finite cuts.

Facts & Assumptions

Given: A finite cut $[k, r]$ of the consecutive residue set $I^{+}$ , a level $l$ and dominant weight $Λ = Λ_{m_{1}} + \dots + Λ_{m_{l}}$ with $m_{1} \geq \dots \geq m_{l}$ , the fundamental wedge $Λ^{d} V$ of the natural module with basis $v_{i}$ , and the column monomials $M_{A}$ of The higher-level wedge-tensor Fock module.

[F1]

Dictionary and Fock conventions (The Fock-space convention dictionary for finite type-A quantum modules, The higher-level wedge-tensor Fock module): the source generators act by $D_{a} v_{b} = s^{δ_{a b}} v_{b}$ , $E_{a} v_{b} = δ_{a + 1, b} v_{a}$ , $F_{a} v_{b} = δ_{a, b} v_{a + 1}$ ; the fundamental factors are the integrable highest weight modules $V (Λ_{m_{j}})$ with highest weight vectors the ground wedges; weights are computed by $w t (A)$ .

[F2]

Integrability and tensor products (Tensor products of integrable weight modules and of their crystal lattices, The integrable quantum highest weight module exists and is unique): integrable highest weight modules exist, are generated from their highest weight vectors by divided lowering powers, and tensor products of integrable modules are integrable.

[F3]

Crystal and lattice suppliers (The Kashiwara lattices $L (λ)$ and $L (\infty)$ and their generating sets, Crystal lattices, crystal bases and their crystals, The tensor product crystal $B_{1} \otimes B_{2}$ and its two-case convention, The crystal basis of a tensor product and the two-case operator rule, Uniqueness: crystal bases of integrable modules decompose into highest weight crystals): crystal bases, tensor rules and highest-weight decompositions in the library normalization.

Proof

technique · direct

1.1F1algebra

The ordered-word lattice for one fundamental factor. Define the exterior quotient by $v_{a} \otimes v_{a} = 0$ and $v_{b} \otimes v_{a} = - s^{- 1} v_{a} \otimes v_{b}$ for $b > a$ . Thus sorting an ascending adjacent pair into descending order contributes $- s$ , not a positive scalar. The coproduct sends a repeated-letter relation under $E_{a}$ or $F_{a}$ to the corresponding signed adjacent relation; on distinct letters the same two-term computation preserves that relation. Hence the quotient is a module. Sorting distinct letters has scalar $(- s)^{ℓ (w)}$ ; commutation and braid moves preserve the number of inversions, and repeated-letter words vanish. The quotient therefore has one independent ordered generator for each distinct-letter orbit.

2.1F1step 1.1algebra

The integral basis and primitive antisymmetrizer. The quotient sorting relations have Laurent-unit coefficients and disjoint permutation orbits, giving a free ordered-word lattice. In the tensor lattice the alternating word of a descending tuple is the sum over permutations with coefficients $(- s)^{ℓ (w)}$ , with ordered coefficient one. Different tuples have disjoint supports; their span is a direct summand by taking the ordered coefficients and is therefore primitive. A coproduct replacement on the alternating sum cancels if it creates a repeated letter, and otherwise gives the alternating word of the replaced tuple with coefficient one; the two adjacent terms are exactly the cancellation checked in step 1.1. Thus sending an ordered quotient vector to its alternating word is an integral module isomorphism onto this span. No raw tensor-chart basedness is inferred.

3.1F1F2F3step 2.1construct

The wedge is the fundamental module with its own lattice, bar and crystal. On ordered wedges the generators act by replacing a single entry: $E_{a} v_{b} = δ_{a + 1, b} v_{a}$ and $F_{a} v_{b} = δ_{a, b} v_{a + 1}$ on letters, extended multiplicatively to a wedge; an attempted replacement producing a repeated letter gives $0$ . The top wedge is annihilated by all $E_{a}$ and is the highest weight vector; divided lowering powers reach every ordered wedge, so the wedge is generated as the integrable highest weight module $V (Λ_{m})$ with highest weight $Λ_{m} = \sum$ of its ground letters, and the ordered-wedge lattice is its divided-power lattice with the induced bar involution and crystal chart.

4.1F1F2step 3.1algebra

The tensor basis. The tensor product of fundamental factors has as integral basis the tensor products of their ordered-wedge bases, i.e. precisely the column monomials $M_{A}$ with one wedge per column; by [F2] the tensor product is integrable and its weight is the sum of the factor weights, which is $w t (A)$ as computed in The higher-level wedge-tensor Fock module. This proves (1) and (2) on a finite cut.

5.1F1step 4.1construct

The lower-cut embeddings. Appending the same entry $k - 1$ below every column defines a linear map on the span of monomials; since the appended letters are smaller than every letter of the cut, the image is again a span of ordered wedges, so $ι_{k}$ is injective and intertwines the common-root generator action: the appended letter is never moved by a generator whose residue lies in the cut, for the common root subalgebra. No assertion says the new boundary generator acts by zero: it may move the appended letter when the next letter is absent. The embeddings for decreasing cuts are compatible, and every semi-infinite tableau differs from the ground state in finitely many positions, hence belongs to the image of some lower cut and to some upper cut.

6.1F1F2F3step 5.1∎

Direct limit and finiteness. The compatible system of the maps of step 5.1 with upper cuts containing all entries of the monomials gives the full Fock module as a direct limit; generators act by finitely many box moves because each generator replaces one letter in one factor, hence shifts the weight by a root and changes only finitely many entries; a fixed weight fixes the multiset difference from the common ground tail, so only finitely many tableaux occur and the weight space is finite dimensional. All finite-Cartan suppliers of [F2], [F3] are applied on the finite cuts, where every module involved is finite dimensional; no finite-dimensionality is claimed for fundamental factors on a merely lower-bounded infinite interval.

Depends on

Used by

Dependency tree · two levels

47 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Jonathan Brundan and Alexander Kleshchev, The degenerate analogue of Ariki's categorification theorem, Math. Z. 266 (2010) 877-919 (complete 44-page arXiv article) (standard reference, not scraped)
Jonathan Brundan, Dual canonical bases and Kazhdan-Lusztig polynomials, J. Algebra 306 (2006) 17-46 (complete 29-page arXiv v2 article) (standard reference, not scraped)