TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

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 A1 Nakajima Hecke correspondence gives the fundamental sl2 action

Statement

Use A one-vertex framed quiver variety and its Hecke correspondence and The A1 Nakajima varieties and the Hecke correspondence are points. Let $e_{v}$ be the fundamental class of $L (v, 1)$ in $H_{0} (L (v, 1); C)$ , for $v = 0, 1$ . Define $F$ by the $P_{0, 1}$ correspondence only from the $v = 0$ summand to the $v = 1$ summand, and extend it by zero on $v = 1$ . Define $E$ by the reverse correspondence, with Nakajima's sign $(- 1)^{(d (0, 1) - d (1, 1)) / 2}$ , only from $v = 1$ to $v = 0$ , and extend it by zero on $v = 0$ , where $d (v, 1) = \dim_{C} M (v, 1)$ . The preceding lemma says both dimensions are zero, so this coefficient is $1$ . Let $H$ act on the $v$ -summand by $1 - 2 v$ . Then $E e_{0} = 0, E e_{1} = e_{0}, F e_{0} = e_{1}, F e_{1} = 0, H e_{0} = e_{0}, H e_{1} = - e_{1} .$ These operators define the standard two-dimensional representation of ${s l}_{2} (C)$ , the trace-zero $2 \times 2$ matrices with commutator bracket.

Facts & Assumptions

Given: The framed $A_{1}$ data, its correspondence, and the point classes specified in the Statement.

[F1]

A one-vertex framed quiver variety and its Hecke correspondence: when $P_{0, 1}$ and both spaces are points and the projections are identities, its fundamental-class correspondence map sends the source point class to the target point class; the reverse map uses the same rule.

[F2]

The A1 Nakajima varieties and the Hecke correspondence are points: $L (0, 1)$ , $L (1, 1)$ and $P_{0, 1}$ are points, and each projection of $P_{0, 1}$ is the identity map.

[F4]

Singular homology satisfies dimension and arbitrary additivity: $H_{0} ({*}; C) ≅ C$ .

Proof

1.1givenF1F2F4algebra

By [F2] and [F4], each summand is one-dimensional with its point class as basis, and each point has complex dimension zero. The projections of $P_{0, 1}$ are identities; hence [F1]'s point correspondence rule sends $e_{0}$ to $e_{1}$ and its reverse sends $e_{1}$ to $e_{0}$ . The reverse sign is $(- 1)^{(0 - 0) / 2} = 1$ ; extending the maps by zero on the other summands gives the stated actions.

2.1F1step 1.1algebra

On $e_{0}$ , $E F e_{0} = e_{0}$ and $F E e_{0} = 0$ ; on $e_{1}$ , $E F e_{1} = 0$ and $F E e_{1} = e_{1}$ . Thus $[E, F]$ has eigenvalues $1, - 1$ on $e_{0}, e_{1}$ , respectively, which are the specified $H$ -weights, so $[E, F] = H$ .

2.2F1step 1.1algebra

On $e_{0}$ , $[H, E] e_{0} = H (0) - E (e_{0}) = 0 = 2 E e_{0}$ ; on $e_{1}$ , $[H, E] e_{1} = H (e_{0}) - E (- e_{1}) = 2 e_{0} = 2 E e_{1}$ . Hence $[H, E] = 2 E$ .

3.1F1step 1.1algebra∎

On $e_{1}$ , $[H, F] e_{1} = H (0) - F (- e_{1}) = 0 = - 2 F e_{1}$ ; on $e_{0}$ , $[H, F] e_{0} = H (e_{1}) - F (e_{0}) = - 2 e_{1} = - 2 F e_{0}$ . Hence $[H, F] = - 2 F$ . In the ordered basis $(e_{0}, e_{1})$ these actions are $E = (\begin{matrix} 0 & 1 \\ 0 & 0 \end{matrix})$ , $F = (\begin{matrix} 0 & 0 \\ 1 & 0 \end{matrix})$ , and $H = (\begin{matrix} 1 & 0 \\ 0 & - 1 \end{matrix})$ ; their brackets just verified are the defining brackets of the trace-zero matrix Lie algebra, so the action is its standard representation.

Depends on

Used by

The A1 Nakajima correspondence in the fundamental sl2 representation Example

Dependency tree · two levels

15 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

Hiraku Nakajima, Introduction to quiver varieties—for ring and representation theorists, §§4.2, 4.4–4.5 (standard reference, not scraped)