ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck pass

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 degenerate affine Hecke relations on two tensor factors

Example

Take $g = {g l}_{2} (C)$ , the natural module $V = C^{2}$ with basis $v_{1}, v_{2}$ , the module $M = V$ and $d = 2$ , so that the Arakawa-Suzuki construction acts on $M \otimes V^{\otimes 2} = V^{\otimes 3}$ . Write $P_{a b}$ for the operator that permutes the tensor factors in positions $a, b \in {0, 1, 2}$ of $V^{\otimes 3}$ . Then $x_{1} = P_{01}$ , $s_{1} = P_{12}$ and $x_{2} = P_{02} + P_{12}$ .

The example verifies on the eight-element tensor basis all relations of the degenerate affine Hecke presentation in this smallest nontrivial case: $s_{1}^{2} = 1$ , $[x_{1}, x_{2}] = 0$ , $s_{1} x_{2} - x_{1} s_{1} = 1$ and $x_{2} s_{1} - s_{1} x_{1} = 1$ . It also records two points that are easy to misread: on $v_{1} \otimes v_{2} \otimes v_{1}$ the two sides of the cross relation differ by exactly the original vector, and the commutator $[s_{1}, x_{2}]$ is not the identity, because the affine cross relation has $x_{1}$ , not $x_{2}$ , on its other side.

Facts & Assumptions

Given: The natural ${g l}_{2}$ -module $V = C^{2}$ with basis $v_{1}, v_{2}$ , the tensor space $V^{\otimes 3}$ with its eight basis words, and the place permutations $P_{a b}$ .

[F1]

In the Arakawa-Suzuki construction with $M = V$ and $d = 2$ the operator $Ω$ on two tensor slots is the flip, and $x_{j} = Ω_{0 j} + \sum_{k < j} P_{k j}$ ; hence $x_{1} = P_{01}$ , $s_{1} = P_{12}$ and $x_{2} = P_{02} + P_{12}$ , and each $P_{a b}$ is an involution (Arakawa-Suzuki Casimir operators on tensor functors, The degenerate affine Hecke algebra).

[F2]

In general the Casimir and place permutation operators satisfy all Coxeter, commutation and affine cross relations, in particular $s_{i}^{2} = 1$ , $[x_{i}, x_{j}] = 0$ , $s_{i} x_{i + 1} - x_{i} s_{i} = 1$ and $x_{i + 1} s_{i} - s_{i} x_{i} = 1$ (The Casimir and place-permutation operators satisfy the degenerate affine Hecke relations).

Proof

technique · direct

Given: The operators $x_{1} = P_{01}$ , $s_{1} = P_{12}$ and $x_{2} = P_{02} + P_{12}$ on $V^{\otimes 3}$ acting on the eight basis words $w_{0} \otimes w_{1} \otimes w_{2}$ , $w_{i} \in {v_{1}, v_{2}}$ .

1.1F1algebra

The permutation identities. Since $P_{a b}$ exchanges two tensor positions it is an involution, $P_{a b}^{2} = 1$ ; and evaluating on the eight words gives the two braid-type identities used below, $P_{12} P_{02} = P_{01} P_{12}$ and $P_{02} P_{12} = P_{12} P_{01}$ , together with their transposes $P_{01} P_{02} = P_{12} P_{01}$ and $P_{02} P_{01} = P_{01} P_{12}$ (both sides of each identity send a word to the same word).

2.1F1step 1.1algebra

The four relations. First $s_{1}^{2} = P_{12}^{2} = 1$ . Next, $[x_{1}, x_{2}] = P_{01} P_{02} - P_{02} P_{01} + P_{01} P_{12} - P_{12} P_{01}$ , and the identities $P_{01} P_{02} = P_{12} P_{01}$ , $P_{02} P_{01} = P_{01} P_{12}$ of step 1.1 cancel the four 3-cycle terms pairwise. Finally $s_{1} x_{2} - x_{1} s_{1} = P_{12} P_{02} + P_{12}^{2} - P_{01} P_{12} = P_{01} P_{12} + 1 - P_{01} P_{12} = 1$ and, symmetrically, $x_{2} s_{1} - s_{1} x_{1} = P_{02} P_{12} + P_{12}^{2} - P_{12} P_{01} = P_{12} P_{01} + 1 - P_{12} P_{01} = 1$ . Hence all degenerate affine Hecke relations of [F2] hold in this specialization.

3.1F1step 2.1algebra

The explicit vector. For $v_{1} \otimes v_{2} \otimes v_{1}$ : $s_{1}$ sends it to $v_{1} \otimes v_{1} \otimes v_{2}$ , which $x_{1} = P_{01}$ fixes, so $x_{1} s_{1} (v_{1} \otimes v_{2} \otimes v_{1}) = v_{1} \otimes v_{1} \otimes v_{2}$ ; and $x_{2} = P_{02} + P_{12}$ sends it to $v_{1} \otimes v_{2} \otimes v_{1} + v_{1} \otimes v_{1} \otimes v_{2}$ , which $s_{1}$ sends to $v_{1} \otimes v_{1} \otimes v_{2} + v_{1} \otimes v_{2} \otimes v_{1}$ . Hence $(s_{1} x_{2} - x_{1} s_{1}) (v_{1} \otimes v_{2} \otimes v_{1}) = v_{1} \otimes v_{2} \otimes v_{1}$ , the identity action on this vector.

4.1F1step 3.1algebra∎

The commutator caveat. On the same vector, $x_{2} s_{1} (v_{1} \otimes v_{2} \otimes v_{1}) = v_{2} \otimes v_{1} \otimes v_{1} + v_{1} \otimes v_{2} \otimes v_{1}$ and $s_{1} x_{1} (v_{1} \otimes v_{2} \otimes v_{1}) = v_{2} \otimes v_{1} \otimes v_{1}$ , so $(x_{2} s_{1} - s_{1} x_{1}) (v_{1} \otimes v_{2} \otimes v_{1}) = v_{1} \otimes v_{2} \otimes v_{1}$ , while $[s_{1}, x_{2}] (v_{1} \otimes v_{2} \otimes v_{1}) = v_{1} \otimes v_{1} \otimes v_{2} - v_{2} \otimes v_{1} \otimes v_{1}$ , which has no component along $v_{1} \otimes v_{2} \otimes v_{1}$ . So $[s_{1}, x_{2}] \neq 1$ : the affine cross relation relates $s_{1} x_{2}$ to $x_{1} s_{1}$ , not to $x_{2} s_{1}$ .

Remarks

The braid-type identities are the only input: once they are checked on the eight words, the two nontrivial relations follow by cancellation of the 3-cycle terms, so the example is a finite verification of the normalization used by the Arakawa-Suzuki action.
The distinction recorded in step 4.1 is not a defect: $[s_{1}, x_{2}] = - 1$ is false as well; the correct affine relations are $s_{1} x_{2} - x_{1} s_{1} = 1$ and $x_{2} s_{1} - s_{1} x_{1} = 1$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

31 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.