LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge 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 finite spherical Hecke algebra is semisimple with nondegenerate trace form

Statement

The finite Hecke algebra $H = e_{B} C [G] e_{B}$ of $G = {GL}_{n} (F_{q})$ is a semisimple finite-dimensional $C$ -algebra of dimension $n!$ , and its trace form $(x, y) \mapsto tr (L_{x y})$ is nondegenerate. Consequently $H$ is isomorphic to a product of matrix algebras, and every finite-dimensional semisimple representation is determined up to isomorphism by the multiplicities of its simple modules. No choice principle is used.

Facts & Assumptions

Given: $G = {GL}_{n} (F_{q})$ with Borel $B$ , the idempotent $e_{B}$ , the finite Hecke algebra $H = e_{B} C [G] e_{B}$ with its trace form $(\cdot, \cdot)$ and standard basis $T_{w}$ , $w \in S_{n}$ .

[F1]

$H$ is a corner of the group algebra, a unital finite-dimensional $C$ -algebra, and it is semisimple (The finite Hecke algebra as a convolution corner and its endomorphism interpretation).

[F2]

The elements $T_{w} = q^{ℓ (w)} e_{B} \dot{w} e_{B}$ , $w \in S_{n}$ , form a $C$ -basis of $H$ , so $\dim_{C} H = n!$ (The Bruhat double-coset basis of the finite Hecke algebra).

[F3]

For any finite-dimensional associative unital $C$ -algebra $A$ the trace form $(a, b) = tr (L_{a b})$ is symmetric and associative, it is nondegenerate if and only if $A$ is semisimple, and a nonzero semisimple such $A$ is isomorphic to $\prod_{i = 1}^{r} M_{d_{i}} (C)$ with simple left modules the natural $d_{i}$ -dimensional modules of the factors (The trace form detects semisimplicity over the complex numbers).

[F4]

A left $R$ -module is semisimple when it is an internal direct sum of simple submodules (Semisimple modules as direct sums of simple modules).

[F5]

For $R = \prod_{i = 1}^{r} M_{n_{i}} (C)$ every simple left $R$ -module is supported on exactly one factor and is isomorphic to that factor's column module $C^{n_{i}}$ , and these column modules give all simple isomorphism classes, one for each factor (Simple modules over a product of matrix rings over division rings).

Proof

technique · direct

1.1F1F2

$H = e_{B} C [G] e_{B}$ is closed under multiplication because $e_{B}^{2} = e_{B}$ , and it contains $e_{B}$ , which acts as its identity; it is finite-dimensional over $C$ , and it is semisimple by [F1]. By [F2] its standard basis has $n!$ elements, so $\dim_{C} H = n!$ .

1.2F3

The trace form $(\cdot, \cdot)$ of $H$ is the symmetric associative bilinear form $(x, y) = tr (L_{x y})$ of [F3], with $L_{c}$ the left multiplication operator on the finite-dimensional $C$ -vector space $H$ .

1.3F3F5

Since $H$ is semisimple, the characterization of [F3] gives that $(\cdot, \cdot)$ is nondegenerate, and the structure statement of [F3] gives an isomorphism $H ≅ \prod_{i = 1}^{r} M_{d_{i}} (C)$ for some $r \geq 1$ and $d_{i} \geq 1$ ; by [F5] the simple left $H$ -modules are exactly the column modules $V_{i} = C^{d_{i}}$ of the factors, one isomorphism class per factor.

2.1F3F4F5step 1.3algebra

Let $M$ be a finite-dimensional semisimple left $H$ -module. By [F4] $M$ is an internal direct sum of simple submodules, each isomorphic to some $V_{i}$ by step 1.3, so $M ≅ ⨁_{i} V_{i}^{m_{i}}$ for multiplicities $m_{i} \geq 0$ . Writing $e_{i} \in H$ for the central idempotent of the $i$ -th matrix factor one has $M = ⨁_{i} e_{i} M$ and each $e_{i} M$ is a module for the factor $M_{d_{i}} (C)$ whose simple submodules are copies of $V_{i}$ , so $e_{i} M ≅ V_{i}^{m_{i}}$ and $m_{i} = \dim_{C} (e_{i} M) / d_{i}$ is determined by $M$ ; conversely the displayed isomorphism shows that $(m_{1}, \dots, m_{r})$ determines $M$ up to isomorphism. Thus the simple modules are a complete set of invariants of the semisimple representations.

3.1step 1.1step 1.3step 2.1∎

Steps 1.1 and 1.3 give the semisimplicity, the dimension $n!$ , the nondegeneracy of the trace form and the product-of-matrix-algebras structure of $H$ , and step 2.1 gives the invariant statement; all objects are finite-dimensional over $C$ and no selection or choice principle is used.

Depends on

Used by

The q=2 torus boundary Example
Group algebra and finite-field specializations of the generic Hecke algebra Proposition
Tits deformation for the type-A Hecke algebra Theorem

Dependency tree · two levels

26 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

Ivan Losev, Lecture 8: Representations of GL_n(F_q) - Section 2.1: 'this algebra is manifestly semisimple'; Section 2.3, semisimplicity of $H_{\mathbb C,q}(n)$, PDF pp. 4-5 (standard reference, not scraped)
Jay Taylor, Finite Reductive Groups - Proposition 5.16 ($H_1\cong\mathbb C W^F$ and $H_q\cong H(G,B)$ are both semisimple), printed pp. 44-45 (standard reference, not scraped)
Olivier Dudas and Jean Michel, Lectures on Finite Reductive Groups and Their Representations - Section 11.1 (the corner of the semisimple group algebra), printed pp. 45-46 (standard reference, not scraped)