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 spherical principal series is the flag permutation module

Statement

Let $1 \in \hat{T}$ be the trivial character and let $G = {GL}_{n} (F_{q})$ with Borel $B = T ⋉ U$ . Then $I (1) = R_{T}^{G} (1) = {Ind}_{B}^{G} (1)$ (The principal series module for finite GL_n) is isomorphic, as a complex $G$ -module, to the permutation module $C [G / B]$ on the left cosets of $B$ (Left and right cosets $g H$ and $H g$ of a subgroup, Left group actions, transitive actions, and faithful actions), and hence, under the $G$ -equivariant bijection $G / B \to {complete flags}$ , $g B \mapsto g V_{∙}$ , to the permutation module on the complete flags of $F_{q}^{n}$ (Complete flags are G/B): the induced module corresponds to the module of complex functions on complete flags with $G$ acting by translation. In particular $\dim_{C} I (1) = [G : B] = # {complete flags} = \prod_{i = 1}^{n} \frac{q^{i} - 1}{q - 1} .$ No choice principle is used.

Facts & Assumptions

Given: $G = {GL}_{n} (F_{q})$ with Borel $B = T ⋉ U$ , the trivial character $1$ of $T$ , and the principal series module $I (1) = R_{T}^{G} (1)$ .

[F1]

Inflating the trivial character of $T$ to $B$ gives the trivial character of $B$ , so $I (1) = {Ind}_{B}^{G} (1)$ ; the module $I (1)$ has dimension $[G : B] = \prod_{i = 1}^{n} (q^{i} - 1) / (q - 1)$ , the number of complete flags (The principal series module for finite GL_n).

[F2]

Inducing the trivial complex representation of a subgroup $H$ of a finite group $G$ gives the permutation representation on the left coset set $G / H$ (Inducing the trivial representation gives the permutation representation on $G / H$ ).

[F3]

The map $g B \mapsto g V_{∙}$ is a $G$ -equivariant bijection from $G / B$ onto the set of complete flags of $F_{q}^{n}$ (Complete flags are G/B).

Proof

technique · direct

1.1F1

The trivial character of $T$ is fixed by inflation, so ${Inf}_{T}^{B} 1 = 1$ and therefore $I (1) = R_{T}^{G} (1) = {Ind}_{B}^{G} (1)$ by definition of $I (1)$ .

1.2F2

By the permutation description of induction of the trivial representation, the complex $G$ -module ${Ind}_{B}^{G} (1)$ is the permutation module on the left cosets $G / B$ .

2.1F1F3step 1.1step 1.2

Composing the isomorphism of step 1.2 with the $G$ -equivariant bijection of [F3] identifies $I (1)$ with the module of complex functions on the complete flags of $F_{q}^{n}$ on which $G$ acts by translation: an equivariant bijection of $G$ -sets induces an isomorphism of permutation modules by transporting a function $φ$ to $φ \circ β$ , where $β : G / B \to {complete flags}$ is the bijection. Since $β$ identifies the $B$ -cosets with the flags, this transport preserves the action. The dimension is $\dim_{C} I (1) = [G : B]$ by [F1], and $[G : B]$ equals the number of complete flags because of the same bijection; the product formula is the one recorded in [F1].

3.1step 1.1step 1.2step 2.1∎

Steps 1.1 and 1.2 give the isomorphism $I (1) ≅ C [G / B]$ , step 2.1 transports it to the flag module and computes the dimension; the trivial character, the induction and the bijection are canonical, and no selection of coset representatives is made, so no choice principle is used.

Depends on

Used by

Dependency tree · two levels

25 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

Jay Taylor, Finite Reductive Groups - Exercise 5.10 (Ind_B^G(M) is the Harish-Chandra induction R_T^G(M_0)), printed p. 44 (standard reference, not scraped)
Masao Oi, Representation Theory of Finite Groups of Lie Type - Section 2.3 (the spherical principal series for GL_2), printed pp. 12-13 (standard reference, not scraped)