TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 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.

Bruhat decomposition of GL_n over a finite field

Statement

Let $n \geq 1$ , let $q$ be a prime power, put $G = {GL}_{n} (F_{q})$ with standard Borel subgroup $B$ of invertible upper triangular matrices (Standard subgroups of finite general linear groups), and for $σ \in S_{n} = Sym ({1, \dots, n})$ let $P_{σ} \in G$ be the permutation matrix with $(P_{σ})_{i j} = 1$ exactly when $i = σ (j)$ and let $W = N / T ≅ S_{n}$ be the Weyl group, so that $σ \mapsto w_{σ} = P_{σ} T$ is an isomorphism $S_{n} \to W$ (Permutation Weyl group and inversion length). Then:

Covering. Every $g \in G$ admits a factorisation $g = b_{1} P_{σ} b_{2}$ with $σ \in S_{n}$ and $b_{1}, b_{2} \in B$ ; equivalently $G = ⋃_{σ \in S_{n}} B P_{σ} B$ .
Separation. The southwest rank matrix of an element $x \in B P_{σ} B$ satisfies $r_{i, j} (x) = # {k \leq j : σ (k) \geq i}$ (Southwest rank matrices determine Bruhat cells), hence determines $σ$ ; consequently $B P_{σ} B \cap B P_{τ} B = \emptyset$ whenever $σ \neq τ$ and the double coset $B x B$ of any $x \in G$ equals exactly one of the sets $B P_{σ} B$ .
Decomposition. $G$ is the disjoint union $G = ⨆_{σ \in S_{n}} B P_{σ} B,$ so the map $σ \mapsto B P_{σ} B$ is a bijection from $S_{n}$ onto the set of double cosets $B x B$ of $G$ , and $B \ G / B$ is in bijection with $S_{n}$ and with the Weyl group $W$ .

Facts & Assumptions

Given: An integer $n \geq 1$ , a prime power $q$ , the group $G = {GL}_{n} (F_{q})$ with standard Borel subgroup $B$ of invertible upper triangular matrices, the symmetric group $S_{n}$ with permutation matrices $P_{σ} \in G$ and the Weyl group $W = N / T ≅ S_{n}$ .

[L1]

Every $g \in G$ has a factorisation $g = b_{1} P_{σ} b_{2}$ with $b_{1}, b_{2} \in B$ and a permutation matrix $P_{σ}$ , $σ \in S_{n}$ (Triangular elimination produces a pivot permutation).

[L2]

$B = {b \in G : b is upper triangular}$ is a subgroup of $G$ (Standard subgroups of finite general linear groups).

[L3]

For $g \in M_{n} (F_{q})$ and $1 \leq i, j \leq n$ let $r_{i, j} (g)$ denote the rank of the submatrix of $g$ on the rows $i, \dots, n$ and the columns $1, \dots, j$ . If $g \in B P_{σ} B$ then $r_{i, j} (g) = # {k \leq j : σ (k) \geq i}$ , and, for $g \in G$ , the rank matrix $(r_{i, j} (g))_{1 \leq i, j \leq n}$ determines $σ$ uniquely (Southwest rank matrices determine Bruhat cells).

[L4]

$W = N / T$ is a group and $σ \mapsto w_{σ} = P_{σ} T$ is an isomorphism of groups $S_{n} \to W$ , so that every element of $W$ has the form $w_{σ}$ for exactly one $σ \in S_{n}$ ; in particular $∣ W ∣ = ∣ S_{n} ∣$ (Permutation Weyl group and inversion length, The symmetric group $Sym (X)$ : the bijections of a set $X$ under composition).

Proof

technique · direct

1.1

By [L1] every $g \in G$ can be written $g = b_{1} P_{σ} b_{2}$ with $b_{1}, b_{2} \in B$ and $σ \in S_{n}$ ; since $B$ is a subgroup of $G$ by [L2], this says $g \in B P_{σ} B$ . Hence the union of the sets $B P_{σ} B$ over $σ \in S_{n}$ is all of $G$ .

L1L2

1.2

Suppose $x \in B P_{σ} B \cap B P_{τ} B$ for $σ, τ \in S_{n}$ . Applying the first assertion of [L3] to $x \in B P_{σ} B$ and to $x \in B P_{τ} B$ gives, for every pair $(i, j)$ of indices, $r_{i, j} (x) = # {k \leq j : σ (k) \geq i}$ and $r_{i, j} (x) = # {k \leq j : τ (k) \geq i}$ ; hence the rank matrices of $σ$ and $τ$ in the sense of [L3] coincide, and the second assertion of [L3] yields $σ = τ$ .

2.1

In particular, if $σ, τ \in S_{n}$ satisfy $σ \neq τ$ , then no element lies in $B P_{σ} B \cap B P_{τ} B$ , that is $B P_{σ} B \cap B P_{τ} B = \emptyset$ ; and for $x \in G$ step 1.1 provides some $σ$ with $x \in B P_{σ} B$ , so $B x B = B P_{σ} B$ equals one of the displayed sets.

step 1.1step 1.2

3.1

Combining steps 1.1 and 2.1, the family $(B P_{σ} B)_{σ \in S_{n}}$ consists of pairwise disjoint subsets of $G$ whose union is $G$ ; that is exactly the displayed disjoint union $G = ⨆_{σ \in S_{n}} B P_{σ} B$ . Consequently the assignment $σ \mapsto B P_{σ} B$ is a well-defined injection $S_{n} \to {B x B : x \in G}$ (distinct $σ$ give disjoint double cosets) and it is surjective, because every $x \in G$ lies in the set $B P_{σ} B = B x B$ for the $σ$ provided by step 1.1.

step 1.1step 2.1L2

4.1

Composing the bijection $σ \mapsto B P_{σ} B$ of step 3.1 with the inverse of the isomorphism $S_{n} \to W$ , $σ \mapsto w_{σ}$ , of [L4] gives a bijection $W \to {B x B : x \in G}$ ; hence the double coset set $B \ G / B$ has exactly $∣ W ∣ = ∣ S_{n} ∣$ elements, indexed by the elements of $W$ .

step 3.1L4∎

Remark. The two ingredients are independent: Triangular elimination produces a pivot permutation produces the factorisation by explicit triangular row and column operations and so gives the covering, while Southwest rank matrices determine Bruhat cells shows that the southwest rank matrix is constant on double cosets and separates them, which gives the disjointness. No choice principle is used: the elimination of the first lemma is deterministic and the rank matrix is a finite invariant.

Depends on

Used by

Flags and Bruhat cells for GL₂(F_q) Example
GL₁ and the trivial parabolic endpoints Example
The six relative positions of GL₃ flags Example
Parabolic double cosets and block permutations Lemma
Cardinality of a finite Bruhat cell Proposition
Relative position classifies pairs of complete flags Theorem

Dependency tree · two levels

30 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 Lemma 4.7, printed p. 18 (standard reference, not scraped)
Jay Taylor, Finite Reductive Groups - Exercise 4.28, printed pp. 38-39 (standard reference, not scraped)