ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-27

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 Hecke quadratic relation from the Soergel square

Example

Fix $n \geq 2$ and a simple reflection $s_{i}$ , and let $A = Z [v, v^{- 1}]$ with $q = v^{- 2}$ , $H_{n}$ the type-A Hecke algebra with normalized generators $H_{i} = v (T_{i} + 1)$ , and $Φ : K_{0}^{s p l i t} ({S B i m}_{n}) \to H_{S_{n}}$ the algebra isomorphism of The split Grothendieck group of the Soergel category is the type-A Hecke algebra. Then:

The class identity. Taking split classes of the rank-one square $B_{i} \otimes_{R} B_{i} ≅ B_{i} (1) \oplus B_{i} (- 1)$ gives $[B_{i}]^{2} = [B_{i} \otimes_{R} B_{i}] = [B_{i} (1)] + [B_{i} (- 1)] = v [B_{i}] + v^{- 1} [B_{i}] = (v + v^{- 1}) [B_{i}]$ in $K_{0}^{s p l i t} ({S B i m}_{n})$ , and applying $Φ$ gives $H_{i}^{2} = (v + v^{- 1}) H_{i}$ in $H_{S_{n}}$ .
The standard quadratic relation. Substituting $H_{i} = v (T_{i} + 1)$ into $H_{i}^{2} = (v + v^{- 1}) H_{i}$ and cancelling the unit $v$ gives $v (T_{i} + 1)^{2} = (v + v^{- 1}) (T_{i} + 1)$ , which expands to $v T_{i}^{2} + (v - v^{- 1}) T_{i} - v^{- 1} = 0$ and, after multiplying by $v^{- 1}$ , to $T_{i}^{2} + (1 - v^{- 2}) T_{i} - v^{- 2} = 0, i.e. (T_{i} - v^{- 2}) (T_{i} + 1) = 0.$ This is exactly the quadratic relation $T_{i}^{2} = (q - 1) T_{i} + q$ of the Hecke algebra in the normalization of The type-A Hecke algebra in Soergel normalization.
Equivalence of the two forms. Conversely, $(T_{i} - v^{- 2}) (T_{i} + 1) = 0$ multiplied by $v^{2}$ reads $v^{2} T_{i}^{2} + (v^{2} - 1) T_{i} - 1 = 0$ , and $H_{i}^{2} - (v + v^{- 1}) H_{i} = v^{2} (T_{i} + 1)^{2} - (v^{2} + 1) (T_{i} + 1) = v^{2} T_{i}^{2} + (v^{2} - 1) T_{i} - 1,$ so the single-generator identities $H_{i}^{2} = (v + v^{- 1}) H_{i}$ and $(T_{i} - v^{- 2}) (T_{i} + 1) = 0$ are equivalent over $A$ .

Facts & Assumptions

Given: The type-A Soergel category ${S B i m}_{n}$ with its split Grothendieck ring, the Hecke algebra $H_{n}$ over $A = Z [v, v^{- 1}]$ with $q = v^{- 2}$ , a simple reflection $s_{i}$ , and the isomorphism $Φ$ of $Z [v, v^{- 1}]$ -algebras with $Φ ([B_{i}]) = H_{i}$ and $Φ (v X) = v Φ (X)$ .

[F1]

The rank-one square: for a simple reflection $s_{i}$ there is a degree-zero isomorphism of graded bimodules $B_{i} \otimes_{R} B_{i} ≅ B_{i} (1) \oplus B_{i} (- 1)$ , the summands being free of rank two on each side (The rank-one Soergel bimodule square splits).

[F2]

In the split Grothendieck ring the product is $[X] [Y] = [X \otimes Y]$ , the shift satisfies $v [X] = [X (1)] = [X {- 1}]$ and $v^{- 1} [X] = [X (- 1)]$ , and the unit is $[R]$ (Split Grothendieck rings of the type-A Soergel categories).

[F3]

There is an isomorphism of $Z [v, v^{- 1}]$ -algebras $Φ : K_{0}^{s p l i t} ({S B i m}_{n}) \to H_{S_{n}}$ with $Φ ([B_{i}]) = H_{i} = v (T_{i} + 1)$ and $Φ (v X) = v Φ (X)$ , and the classes satisfy $[B_{i}]^{2} = (v + v^{- 1}) [B_{i}]$ (The split Grothendieck group of the Soergel category is the type-A Hecke algebra).

[F4]

$H_{n}$ is presented by the generators $T_{i}$ with $T_{i}^{2} = (q - 1) T_{i} + q$ , equivalently $(T_{i} - q) (T_{i} + 1) = 0$ , where $q = v^{- 2}$ ; the normalized generators satisfy $H_{i} = v (T_{i} + 1)$ , $H_{i}^{2} = (v + v^{- 1}) H_{i}$ and $T_{i} = v^{- 1} H_{i} - 1$ , and $v$ is a unit of the Laurent ring $A$ (The type-A Hecke algebra in Soergel normalization).

Proof

1.1

The class identity: by [F1] the bimodules $B_{i} \otimes_{R} B_{i}$ and $B_{i} (1) \oplus B_{i} (- 1)$ are isomorphic, so their classes in $K_{0}^{s p l i t} ({S B i m}_{n})$ coincide; the product and shift rules of [F2] turn this into $[B_{i}]^{2} = [B_{i} \otimes_{R} B_{i}] = [B_{i} (1)] + [B_{i} (- 1)] = v [B_{i}] + v^{- 1} [B_{i}]$ , and [F2] also gives $v [B_{i}] + v^{- 1} [B_{i}] = (v + v^{- 1}) [B_{i}]$ , an identity in the ring.

F1F2

2.1

The Hecke form: applying the algebra homomorphism $Φ$ of [F3], which is $Z [v, v^{- 1}]$ -linear and satisfies $Φ ([B_{i}]) = H_{i}$ , to the identity of step 1.1 gives $H_{i}^{2} = Φ ([B_{i}]^{2}) = Φ ((v + v^{- 1}) [B_{i}]) = (v + v^{- 1}) H_{i}$ in $H_{S_{n}}$ .

F3step 1.1

3.1

The translation: by [F4] $H_{i} = v (T_{i} + 1)$ and $T_{i} = v^{- 1} H_{i} - 1$ , so squaring $H_{i} = v (T_{i} + 1)$ and substituting the relation of step 2.1 gives $v^{2} (T_{i} + 1)^{2} = H_{i}^{2} = (v + v^{- 1}) H_{i} = (v + v^{- 1}) v (T_{i} + 1)$ ; multiplying both sides by the unit $v^{- 1}$ gives $v (T_{i} + 1)^{2} = (v + v^{- 1}) (T_{i} + 1)$ .

F4step 2.1

4.1

The expansion: expanding $v (T_{i} + 1)^{2} = v (T_{i}^{2} + 2 T_{i} + 1)$ and collecting terms in the identity of step 3.1 gives $v T_{i}^{2} + (2 v - v - v^{- 1}) T_{i} + (v - v - v^{- 1}) = 0$ , that is $v T_{i}^{2} + (v - v^{- 1}) T_{i} - v^{- 1} = 0$ ; multiplying by the unit $v^{- 1}$ gives $T_{i}^{2} + (1 - v^{- 2}) T_{i} - v^{- 2} = 0$ .

F4step 3.1

5.1

The factorisation: with $q = v^{- 2}$ , expanding the product $(T_{i} - q) (T_{i} + 1) = T_{i}^{2} + (1 - q) T_{i} - q$ shows that the relation of step 4.1 is exactly $(T_{i} - v^{- 2}) (T_{i} + 1) = 0$ , which is the quadratic relation $T_{i}^{2} = (q - 1) T_{i} + q$ of [F4].

F4step 4.1

6.1

The converse: if $(T_{i} - v^{- 2}) (T_{i} + 1) = 0$ , then $T_{i}^{2} + (1 - v^{- 2}) T_{i} - v^{- 2} = 0$ and multiplication by $v^{2}$ gives $v^{2} T_{i}^{2} + (v^{2} - 1) T_{i} - 1 = 0$ ; expanding the difference in the Hecke algebra gives $H_{i}^{2} - (v + v^{- 1}) H_{i} = v^{2} (T_{i} + 1)^{2} - (v^{2} + 1) (T_{i} + 1) = v^{2} (T_{i}^{2} + 2 T_{i} + 1) - (v^{2} + 1) T_{i} - (v^{2} + 1) = v^{2} T_{i}^{2} + (v^{2} - 1) T_{i} - 1 = 0$ , so $H_{i}^{2} = (v + v^{- 1}) H_{i}$ ; the two single-generator relations are therefore equivalent under $H_{i} = v (T_{i} + 1)$ , with $v$ a unit of $A$ used in both directions.

F4step 5.1

7.1

Conclusion: the rank-one square produces $[B_{i}]^{2} = (v + v^{- 1}) [B_{i}]$ in $K_{0}^{s p l i t} ({S B i m}_{n})$ and, through the isomorphism $Φ$ , the Hecke identity $H_{i}^{2} = (v + v^{- 1}) H_{i}$ ; rewriting $H_{i} = v (T_{i} + 1)$ expands this into $T_{i}^{2} + (1 - v^{- 2}) T_{i} - v^{- 2} = 0$ , that is $(T_{i} - v^{- 2}) (T_{i} + 1) = 0$ , which is the quadratic relation of the Hecke algebra in the standard generators, and the two displayed forms are equivalent by steps 3.1, 4.1, 5.1 and 6.1. Only identities between elements of $A$ and of $H_{n}$ are manipulated, so no choice principle is used. ∎

F3F4step 1.1step 6.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 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

Elias–Williamson, Soergel Calculus, §1.4 and §§3.4–3.5, PDF pp. 8–9, 24–27 (standard reference, not scraped)
Libedinsky, Gentle Introduction to Soergel Bimodules I, §4, PDF pp. 21–26 (standard reference, not scraped)