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.

Length-additive products of the standard intertwiners

Statement

For Weyl-sorted $η = (a_{1}^{n_{1}}, \dots, a_{k}^{n_{k}})$ with distinct $a_{r}$ , put $L = \prod_{r} {GL}_{n_{r}} (F_{q})$ and $ρ (l) = \prod_{r} a_{r} (\det l_{r})$ . With the canonical intertwiners $B_{w}$ of Standard intertwining operators for the finite principal series, set $T_{w} = ρ (\dot{w})^{- 1} B_{w}$ for $w \in W_{η}$ . Then $T_{u} T_{v} = T_{u v}$ whenever the intrinsic (equivalently here ambient) lengths add, and the simple $T_{s}$ satisfy all type-A braid and commuting relations. The raw basis also has length-additive products $B_{u} B_{v} = B_{u v}$ in these sorted coordinates. For arbitrary $χ$ , choose the prescribed sorting $η$ and a module isomorphism $J : I (χ) \to I (η)$ from The Weyl stabiliser controls the principal series endomorphisms; transport the normalized basis through $J$ . Its labels and length are transported through the sorting permutation. This does not identify the unsorted raw ambient-length basis with the transported basis. No choice principle is used.

Facts & Assumptions

Given: $n \geq 1$ , a prime power $q$ , $G = {GL}_{n} (F_{q})$ with diagonal torus $T$ and Borel $B$ , a Weyl-sorted character $η = (a_{1}^{n_{1}}, \dots, a_{k}^{n_{k}})$ with distinct characters $a_{r}$ of $F_{q}^{\times}$ , the blocks $n_{1}, \dots, n_{k}$ of $n$ , the standard parabolic $P = L ⋉ U_{P}$ with Levi $L = \prod_{r} {GL}_{n_{r}} (F_{q})$ and unipotent radical $U_{P}$ , the character $ρ (l) = \prod_{r} a_{r} (\det l_{r})$ of $L$ , the principal series module $I (η)$ with its idempotent $e_{η} = e_{η}^{G}$ , and for $w \in W_{η}$ the corner element $Θ_{w^{- 1}} = q^{ℓ (w)} e_{η} {\dot{w}}^{- 1} e_{η}$ and operator $B_{w} = R_{Θ_{w^{- 1}}}$ (Standard intertwining operators for the finite principal series).

[F1]

The Weyl group of $G$ is $W = S_{n}$ with simple transpositions $s_{i}$ and inversion length $ℓ$ ; for the sorted character $η$ the stabiliser is the group of block permutations $W_{η} = \prod_{r} S_{n_{r}}$ (Diagonal torus characters and the Weyl action).

[F2]

The elements $B_{w}$ , $w \in W_{η}$ , form a $C$ -basis of ${End}_{G} (I (η))$ , where the corner multiplication is the multiplication in $C [G]$ and right multiplication turns $e_{η} C [G] e_{η}$ into ${End}_{G} (I (η))$ with reversed products ( $R_{a} R_{b} = R_{b a}$ ) (Standard intertwining operators for the finite principal series, The standard intertwiners form a basis of the principal series endomorphism algebra).

[F3]

For each block $r$ let $e_{r} = ∣ B_{r} ∣^{- 1} \sum_{b \in B_{r}} {\tilde{η}}_{r} (b)^{- 1} b$ and let $e_{B_{r}}$ be the corresponding idempotent for the trivial character. The map $m_{r} : C [{GL}_{n_{r}} (F_{q})] \to C [{GL}_{n_{r}} (F_{q})]$ , $g \mapsto ψ_{r} (g)^{- 1} g$ with $ψ_{r} = a_{r} \circ \det$ , is an algebra automorphism, and $m_{r} (e_{B_{r}}) = e_{r}$ because for upper triangular $b$ one has $ψ_{r} (b) = a_{r} (\det b) = \prod_{i} a_{r} (b_{i i}) = {\tilde{η}}_{r} (b)$ . Multiplicativity of the determinant makes $ψ_{r}$ a character, so $m_{r} (g) m_{r} (h) = ψ_{r} (g h)^{- 1} g h = m_{r} (g h)$ ; the inverse scales $g$ by $ψ_{r} (g)$ . (The group ring $R [G]$ is a unital $R$ -algebra with basis $G$ , and each $g \in G$ is a unit of $R [G]$ , For same-sized finite square matrices over a commutative ring, $\det (A B) = \det (A) \det (B)$ , The determinant of a triangular matrix is the product of its diagonal entries, The principal series module for finite GL_n).

[F4]

For every block $r$ the standard basis elements $T_{x}^{(r)} = q^{ℓ (x)} e_{B_{r}} \dot{x} e_{B_{r}}$ , $x \in S_{n_{r}}$ , of the block Hecke algebra satisfy $T_{x}^{(r)} T_{y}^{(r)} = T_{x y}^{(r)}$ whenever $ℓ (x y) = ℓ (x) + ℓ (y)$ (The Bruhat double-coset basis of the finite Hecke algebra, Length-additive products in the finite Hecke algebra).

[F5]

$\dim_{C} {End}_{G} (I (η)) = ∣ W_{η} ∣$ and $I (χ) ≅ I (w \cdot χ)$ for every $w \in S_{n}$ , so an arbitrary $χ$ is isomorphic to its sorted form (The Weyl stabiliser controls the principal series endomorphisms).

[F6]

$P = L ⋉ U_{P}$ with $L$ normalising $U_{P}$ , and $B = (B \cap L) U_{P}$ is a bijection, so every $b \in B$ has a unique expression $b = u l$ with $u \in U_{P}$ , $l \in B \cap L$ (Block Levi decomposition of standard parabolics, Compositions, partial flags, and standard parabolics).

Proof

technique · direct

1.1F6algebra

In the group algebra $C [G]$ one has $e_{η}^{G} = e_{U_{P}} e_{η}^{L}$ with $e_{U_{P}} = ∣ U_{P} ∣^{- 1} \sum_{u \in U_{P}} u$ and $e_{η}^{L} = \prod_{r} e_{r}$ : indeed $B = U_{P} B_{L}$ is a bijection because $P = L ⋉ U_{P}$ and $B = (B \cap L) U_{P}$ , and $\tilde{η} (u l) = \tilde{η} (l)$ for $u \in U_{P}$ , $l \in B \cap L$ , so $\sum_{b \in B} \tilde{η} (b)^{- 1} b = (\sum_{u \in U_{P}} u) (\sum_{l \in B \cap L} \tilde{η} (l)^{- 1} l) = ∣ U_{P} ∣ e_{U_{P}} \prod_{r} ∣ B_{r} ∣ e_{r}$ , while $∣ B ∣ = ∣ U_{P} ∣ \prod_{r} ∣ B_{r} ∣$ . Moreover $e_{U_{P}}$ commutes with every element of $C [L]$ , because $l U_{P} l^{- 1} = U_{P}$ for $l \in L$ (the Levi normalises the unipotent radical), so conjugation by $l$ permutes the sum defining $e_{U_{P}}$ .

1.2F3F4algebra

Fix a block $r$ and $x, y \in S_{n_{r}}$ with $ℓ (x y) = ℓ (x) + ℓ (y)$ . Since $m_{r}$ is an algebra automorphism with $m_{r} (e_{B_{r}}) = e_{r}$ and $m_{r} (\dot{z}) = ψ_{r} (\dot{z})^{- 1} \dot{z}$ , one has $m_{r} (e_{B_{r}} \dot{z} e_{B_{r}}) = ψ_{r} (\dot{z})^{- 1} e_{r} \dot{z} e_{r}$ for every $z$ . Applying $m_{r}$ to the block identity $e_{B_{r}} \dot{x} e_{B_{r}} \cdot e_{B_{r}} \dot{y} e_{B_{r}} = e_{B_{r}} \dot{x y} e_{B_{r}}$ , which follows from [F4] by writing $e_{B_{r}} \dot{z} e_{B_{r}} = q^{- ℓ (z)} T_{z}^{(r)}$ , and using multiplicativity of $ψ_{r}$ together with $\dot{x} \dot{y} = \dot{x y}$ , the scalar factors cancel and give $e_{r} \dot{x} e_{r} \cdot e_{r} \dot{y} e_{r} = e_{r} \dot{x y} e_{r}$ .

2.1F1step 1.1algebra

For $w \in W_{η}$ the permutation matrix $\dot{w}$ is block diagonal with blocks ${\dot{w}}_{r} \in {GL}_{n_{r}} (F_{q})$ , and $ℓ (w) = \sum_{r} ℓ (w_{r})$ . Using step 1.1 and $\dot{w} \in L$ , $e_{U_{P}} \dot{w} = \dot{w} e_{U_{P}}$ and $e_{U_{P}}^{2} = e_{U_{P}}$ , one gets $e_{η}^{G} {\dot{w}}^{- 1} e_{η}^{G} = e_{U_{P}} e_{η}^{L} {\dot{w}}^{- 1} e_{η}^{L} e_{U_{P}} = e_{U_{P}} \prod_{r} (e_{r} {\dot{w}}_{r}^{- 1} e_{r})$ ; multiplying by $q^{ℓ (w)}$ and distributing the length over the blocks gives $Θ_{w^{- 1}} = e_{U_{P}} \prod_{r} Θ_{w_{r}^{- 1}}^{(r)}$ , where $Θ_{x}^{(r)} = q^{ℓ (x)} e_{r} \dot{x} e_{r}$ is the block corner element.

3.1F2step 2.1step 1.2algebra

Let $u, v \in W_{η}$ satisfy $ℓ (u v) = ℓ (u) + ℓ (v)$ . Writing the block permutations $u = \prod_{r} u_{r}$ , $v = \prod_{r} v_{r}$ , one has $ℓ (u v) = \sum_{r} ℓ (u_{r} v_{r})$ and $ℓ (u) + ℓ (v) = \sum_{r} (ℓ (u_{r}) + ℓ (v_{r}))$ , so $ℓ (u_{r} v_{r}) = ℓ (u_{r}) + ℓ (v_{r})$ in every block. By steps 2.1 and 1.2, $Θ_{v^{- 1}} Θ_{u^{- 1}} = e_{U_{P}} \prod_{r} Θ_{v_{r}^{- 1}}^{(r)} \cdot e_{U_{P}} \prod_{r} Θ_{u_{r}^{- 1}}^{(r)} = e_{U_{P}} \prod_{r} Θ_{v_{r}^{- 1}}^{(r)} Θ_{u_{r}^{- 1}}^{(r)} = e_{U_{P}} \prod_{r} Θ_{(u_{r} v_{r})^{- 1}}^{(r)} = Θ_{(u v)^{- 1}}$ . Since right multiplication is a homomorphism (with the reversed product convention), $B_{u} B_{v} = R_{Θ_{u^{- 1}}} R_{Θ_{v^{- 1}}} = R_{Θ_{v^{- 1}} Θ_{u^{- 1}}} = R_{Θ_{(u v)^{- 1}}} = B_{u v}$ : the raw basis is length-additive in the sorted coordinates.

4.1step 3.1algebra

For general $u, v$ with additivity, multiplicativity of $ρ$ and $\dot{u} \dot{v} = \dot{u v}$ give $T_{u} T_{v} = ρ (\dot{u})^{- 1} ρ (\dot{v})^{- 1} B_{u} B_{v} = ρ (\dot{u v})^{- 1} B_{u v} = T_{u v}$ by step 3.1.

5.1F1step 4.1algebra

For simple transpositions inside a block, the permutations $s_{i} s_{i + 1} s_{i}$ and $s_{i + 1} s_{i} s_{i + 1}$ coincide and both triple products are length-additive, so step 4.1 applied twice gives $T_{s_{i}} T_{s_{i + 1}} T_{s_{i}} = T_{s_{i} s_{i + 1} s_{i}} = T_{s_{i + 1} s_{i} s_{i + 1}} = T_{s_{i + 1}} T_{s_{i}} T_{s_{i + 1}}$ ; for simple transpositions with commuting permutations, both products are length-additive and step 4.1 gives $T_{s_{i}} T_{s_{j}} = T_{s_{i} s_{j}} = T_{s_{j} s_{i}} = T_{s_{j}} T_{s_{i}}$ .

6.1F5step 3.1step 4.1step 5.1∎

Steps 3.1, 4.1 and 5.1 give the length-additive rule for the raw and the normalised basis together with the braid and commuting relations. For an arbitrary $χ$ , let $σ \in S_{n}$ with $η = σ \cdot χ$ be the prescribed sorting and let $J : I (χ) \to I (η)$ be a module isomorphism, which exists by [F5] with $W_{χ} = σ^{- 1} W_{η} σ$ ; conjugating the transported basis $T \mapsto J^{- 1} T J$ is an algebra isomorphism, so the same product identities hold for the transported basis, whose label in $W_{χ}$ is $σ^{- 1} w σ$ and whose governing length is the transported intrinsic length $ℓ (w)$ . This length need not equal the ambient inversion length of $σ^{- 1} w σ$ , because inversion length is not a class function on $S_{n}$ , so the transported basis is not asserted to coincide with the raw ambient-length basis ${B_{v} : v \in W_{χ}}$ , which carries ambient lengths and no $ρ$ -normalisation. All sums are finite, the block decomposition and permutation matrices are explicit, and no choice principle is used.

Depends on

Used by

Dependency tree · two levels

51 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

Olivier Dudas and Jean Michel, Lectures on Finite Reductive Groups and Their Representations - Lemma 11.9 and its proof, printed p. 49 (standard reference, not scraped)
Olivier Dudas and Jean Michel, Lectures on Finite Reductive Groups and Their Representations - Theorem 11.11 and the preceding discussion of (P1)-(P3), printed pp. 49-50 (standard reference, not scraped)
Jay Taylor, Finite Reductive Groups - The relation $\bar T_s\bar T_w=\bar T_{sw}$ for length-increasing products, printed p. 44 (standard reference, not scraped)
Olivier Dudas and Jean Michel, Lectures on Finite Reductive Groups and Their Representations, Remark 9.3, Proposition 9.5, §11.1 and Theorem 11.11 (standard reference, not scraped)