TheoremStatement: Literature-sourcedProof: 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.

Complete flags are G/B

Statement

Let $n \geq 1$ and let $q$ be a prime power. Put $G = {GL}_{n} (F_{q})$ and let $V = F_{q}^{n}$ . Then:

$G$ acts on the set $X$ of complete flags $0 = F_{0} < F_{1} < \dots < F_{n} = V$ with $\dim_{F_{q}} F_{i} = i$ by $g \cdot F : = (g (F_{0}), \dots, g (F_{n}))$ ;
the standard flag $V_{∙}$ with $V_{i} = ⟨ e_{1}, \dots, e_{i} ⟩$ , where $e_{1}, \dots, e_{n}$ is the standard basis of $V$ , is a complete flag whose stabiliser is the standard Borel subgroup $B$ of Standard subgroups of finite general linear groups;
consequently $g B \mapsto g \cdot V_{∙}$ is a $G$ -equivariant bijection $G / B \to X$ , so the complete flags are in bijection with the left cosets of $B$ .

Facts & Assumptions

Given: An integer $n \geq 1$ , a prime power $q$ , the group $G = {GL}_{n} (F_{q})$ acting by matrix-vector multiplication on $V = F_{q}^{n}$ , the standard basis $e_{1}, \dots, e_{n}$ of $V$ , and the set $X$ of complete flags of $V$ .

[L1]

$B = {b \in G : b is upper triangular}$ , $T \leq B$ , $U \leq B$ , $T \cap U = {I_{n}}$ and $B = T ⋉ U$ ; $T$ , $U$ and $B$ are the standard torus, the standard maximal unipotent subgroup and the standard Borel subgroup of $G$ , with $U ⊴ B$ (Standard subgroups of finite general linear groups).

[L2]

The standard flag of $V = F_{q}^{n}$ is the chain $V_{0} : = {0} ⊊ V_{1} : = ⟨ e_{1} ⟩ ⊊ \dots ⊊ V_{n} : = ⟨ e_{1}, \dots, e_{n} ⟩ = V$ of standard coordinate subspaces, and each $V_{i}$ has $\dim_{F_{q}} V_{i} = i$ with $V_{i - 1} ⊊ V_{i}$ for $1 \leq i \leq n$ (Standard subgroups of finite general linear groups).

[L3]

A matrix $A = (a_{i j}) \in M_{n} (F_{q})$ is upper triangular when $a_{i j} = 0$ for $i > j$ (Upper triangular, lower triangular and diagonal square matrices over a commutative ring).

[L4]

A left action of $G$ on a set $X$ is a map $G \times X \to X$ , $(g, x) \mapsto g \cdot x$ , with $e \cdot x = x$ and $(g h) \cdot x = g \cdot (h \cdot x)$ for all $g, h \in G$ , $x \in X$ ; the action is transitive when every $x, y \in X$ satisfy $g \cdot x = y$ for some $g \in G$ (Left group actions, transitive actions, and faithful actions).

[L5]

If $X$ is a transitive $G$ -set and $x \in X$ , the orbit map $G / G_{x} \to X$ , $g G_{x} \mapsto g \cdot x$ , is an equivariant isomorphism from the left-coset action to the given action (Every transitive $G$ -set is equivariantly isomorphic to $G / G_{x}$ for any chosen point $x$ ).

[L6]

For $A \in M_{n} (F)$ the following are equivalent: $A$ is invertible; and $x \mapsto A x$ is a linear isomorphism (Invertible matrix theorem: invertibility, full pivot rank, RREF $I$ , trivial nullspace and unique solvability are equivalent).

[L7]

For an ordered basis $b_{1}, \dots, b_{m}$ of a vector space and a linear map $T$ , the $j$ -th column of the matrix of $T$ is the coordinate column of $T (b_{j})$ ; conversely a matrix with prescribed columns defines the linear map sending $b_{j}$ to the corresponding vector (Coordinate columns $[v]_{B}$ and matrices $[T]_{B}^{C}$ of linear maps relative to ordered bases).

[L8]

$⟨ e_{1}, \dots, e_{i} ⟩$ has $e_{1}, \dots, e_{i}$ as a basis, so every $g \in G$ satisfies $g (⟨ e_{1}, \dots, e_{i} ⟩) = ⟨ g (e_{1}), \dots, g (e_{i}) ⟩$ and $\dim_{F_{q}} g (⟨ e_{1}, \dots, e_{i} ⟩) = i$ (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis, Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis, Linear subspace of a vector space, Rank-nullity: $\dim_{F} V = nullity T + rank T$ ).

[L9]

If $U, W$ are finite-dimensional linear subspaces then $\dim (U + W) + \dim (U \cap W) = \dim U + \dim W$ (The dimension formula: for finite-dimensional linear subspaces $U$ and $W$ of $V$ , the subspaces $U + W$ and $U \cap W$ are finite-dimensional and $\dim_{F} (U + W) + \dim_{F} (U \cap W) = \dim_{F} U + \dim_{F} W$ ).

[L10]

If $U \leq W$ are finite-dimensional linear subspaces with $\dim U = \dim W$ then $U = W$ (If $\dim_{F} V = n$ and $U$ is a linear subspace of $V$ , then $U$ is finite-dimensional, $\dim_{F} U \leq n$ , and $\dim_{F} U = n$ if and only if $U = V$ ).

Proof

technique · direct

1.1

The map $G \times X \to X$ , $(g, F_{∙}) \mapsto g \cdot F_{∙}$ with $(g \cdot F)_{i} : = g (F_{i})$ , is a well-defined left action: for $g \in G$ and $F_{∙} \in X$ each $g (F_{i})$ is a linear subspace with $g (F_{0}) = {0}$ and $g (F_{n}) = V$ , and by [L6] the map $x \mapsto g x$ is injective, so restricting it to $F_{i}$ and applying [L8] gives $\dim_{F_{q}} g (F_{i}) = \dim_{F_{q}} F_{i} = i$ ; dimensions therefore increase by one at each step, so $g (F_{i - 1}) ⊊ g (F_{i})$ and $g \cdot F_{∙} \in X$ . Moreover $I_{n} x = x$ and $(g h) x = g (h x)$ for all $x \in V$ , so $I_{n} \cdot F_{∙} = F_{∙}$ and $(g h) \cdot F_{∙} = g \cdot (h \cdot F_{∙})$ ; thus $X$ is a $G$ -set.

L4L6L8given

1.2

The standard flag $V_{∙}$ lies in $X$ : by [L2] each $V_{i} = ⟨ e_{1}, \dots, e_{i} ⟩$ is a linear subspace of $V$ with $V_{0} = {0}$ , $V_{n} = V$ , $\dim_{F_{q}} V_{i} = i$ and $V_{i - 1} ⊊ V_{i}$ .

L2given

1.3

The stabiliser of $V_{∙}$ is $B$ . Let $g \in G$ have matrix $A = (a_{i j})$ in the standard basis, so that $g (e_{i}) = \sum_{k} a_{k i} e_{k}$ and $g (e_{i}) \in V_{i}$ if and only if $a_{k i} = 0$ for every $k > i$ , that is, if and only if $A$ is upper triangular by [L3]. If $g \cdot V_{∙} = V_{∙}$ then $g (e_{i}) \in g (V_{i}) = V_{i}$ for every $i$ ; conversely, if $g (e_{i}) \in V_{i}$ for every $i$ , then $g (V_{i}) = ⟨ g (e_{1}), \dots, g (e_{i}) ⟩ \subseteq V_{i}$ by [L8], and both spaces have dimension $i$ by [L8] and [L2], so $g (V_{i}) = V_{i}$ by [L10]. Hence $g$ stabilises $V_{∙}$ if and only if $A$ is upper triangular, that is, if and only if $g \in B$ by [L1], so $G_{V_{∙}} = B$ .

L1L2L3L7L8L10given

1.4

Let $F_{∙} \in X$ be an arbitrary complete flag. Since $F_{i - 1} ⊊ F_{i}$ , for each $1 \leq i \leq n$ there is a vector $v_{i} \in F_{i} ∖ F_{i - 1}$ .

constructgiven

2.1

The list $v_{1}, \dots, v_{i}$ is a basis of $F_{i}$ for every $i$ , by induction on $i$ : $v_{1} \neq 0$ spans the line $F_{1}$ ; and if $v_{1}, \dots, v_{i - 1}$ is a basis of $F_{i - 1}$ , then $F_{i - 1} + ⟨ v_{i} ⟩ \subseteq F_{i}$ has dimension $(i - 1) + 1 - \dim (F_{i - 1} \cap ⟨ v_{i} ⟩) = i$ by [L9], because $v_{i} \notin F_{i - 1}$ forces $F_{i - 1} \cap ⟨ v_{i} ⟩ = {0}$ , while $\dim_{F_{q}} F_{i} = i$ ; hence $F_{i - 1} + ⟨ v_{i} ⟩ = F_{i}$ by [L10], so $v_{1}, \dots, v_{i}$ spans $F_{i}$ , and it is linearly independent because a relation $\sum_{j \leq i} c_{j} v_{j} = 0$ with $c_{i} \neq 0$ expresses $v_{i}$ as an element of $span (v_{1}, \dots, v_{i - 1}) = F_{i - 1}$ , contrary to the choice of $v_{i}$ , while $c_{i} = 0$ reduces the relation to the independent list $v_{1}, \dots, v_{i - 1}$ . In particular $v_{1}, \dots, v_{n}$ is a basis of $F_{n} = V$ .

step 1.4L9L10

3.1

Let $g : V \to V$ be the linear map with $g (e_{i}) = v_{i}$ for all $i$ ; by [L7] it has a unique matrix in the standard basis. It carries the basis $e_{1}, \dots, e_{n}$ of $V$ onto the basis $v_{1}, \dots, v_{n}$ of $V$ from step 2.1, hence is bijective, so its matrix is invertible by [L6] and $g \in G$ . Moreover, for every $i$ , the members $V_{i}$ of the standard flag of [L2] satisfy $g (V_{i}) = ⟨ g (e_{1}), \dots, g (e_{i}) ⟩ = ⟨ v_{1}, \dots, v_{i} ⟩ = F_{i}$ by [L8], the last equality by step 2.1, so $g \cdot V_{∙} = F_{∙}$ .

step 2.1L2L6L7L8

4.1

By step 3.1 every $F_{∙} \in X$ has the form $g \cdot V_{∙}$ for some $g \in G$ , so the action of step 1.1 is transitive in the sense of [L4]; with $G_{V_{∙}} = B$ by step 1.3, the orbit map of [L5], applied to the transitive $G$ -set $X$ and the point $V_{∙}$ , is a $G$ -equivariant bijection $G / B \to X$ , $g B \mapsto g \cdot V_{∙}$ . This is the asserted bijection between complete flags and left cosets of $B$ . ∎

step 1.1step 1.3step 3.1L4L5

Depends on

Used by

Compositions, partial flags, and standard parabolics Definition
Ordered partitions and coordinate parabolics Definition
Flags and Bruhat cells for GL₂(F_q) Example
GL₁ and the trivial parabolic endpoints Example
Parabolic induction of the trivial module as flag functions Example
Relative position classifies pairs of complete flags Theorem

Dependency tree · two levels

70 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 - Example 4.5 and Example 8.4, printed pp. 18 and 30 (standard reference, not scraped)
Jay Taylor, Finite Reductive Groups - Exercise 4.28, printed pp. 38-39 (standard reference, not scraped)