ExampleConstruction: Literature-sourcedVerification: 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.

The six relative positions of GL_3 flags

Example

Let $q$ be a prime power, put $G = {GL}_{3} (F_{q})$ and write the six elements of $S_{3}$ in one-line notation. For each $σ \in S_{3}$ let $w = P_{σ}$ be the permutation matrix and let $r_{i, j} (w) = # {k \leq j : σ (k) \geq i}$ be the southwest ranks of $w$ (Southwest rank matrices determine Bruhat cells, Permutation Weyl group and inversion length). Then $r (w) = (\begin{array}{ccc} 1 & 2 & 3 \\ 0 & 1 & 2 \\ 0 & 0 & 1 \end{array}), (\begin{array}{ccc} 1 & 2 & 3 \\ 0 & 1 & 2 \\ 0 & 1 & 1 \end{array}), (\begin{array}{ccc} 1 & 2 & 3 \\ 1 & 1 & 2 \\ 0 & 0 & 1 \end{array}),$ $r (w) = (\begin{array}{ccc} 1 & 2 & 3 \\ 1 & 2 & 2 \\ 0 & 1 & 1 \end{array}), (\begin{array}{ccc} 1 & 2 & 3 \\ 1 & 1 & 2 \\ 1 & 1 & 1 \end{array}), (\begin{array}{ccc} 1 & 2 & 3 \\ 1 & 2 & 2 \\ 1 & 1 & 1 \end{array})$ for $σ = 123, 132, 213, 231, 312, 321$ respectively, and the equivalent intersection-dimension matrices $(\dim_{F_{q}} (V_{i} \cap w V_{j}))_{i, j} = (j - r_{i + 1, j} (w))_{i, j}$ , with $r_{4, j} (w) : = 0$ , are $(\begin{array}{ccc} 1 & 1 & 1 \\ 1 & 2 & 2 \\ 1 & 2 & 3 \end{array}), (\begin{array}{ccc} 1 & 1 & 1 \\ 1 & 1 & 2 \\ 1 & 2 & 3 \end{array}), (\begin{array}{ccc} 0 & 1 & 1 \\ 1 & 2 & 2 \\ 1 & 2 & 3 \end{array}),$ $(\begin{array}{ccc} 0 & 0 & 1 \\ 1 & 1 & 2 \\ 1 & 2 & 3 \end{array}), (\begin{array}{ccc} 0 & 1 & 1 \\ 0 & 1 & 2 \\ 1 & 2 & 3 \end{array}), (\begin{array}{ccc} 0 & 0 & 1 \\ 0 & 1 & 2 \\ 1 & 2 & 3 \end{array})$ in the same order. The six southwest rank matrices are pairwise distinct, and so are the six intersection-dimension matrices; by Relative position classifies pairs of complete flags the six permutations therefore realise the six distinct relative positions of pairs of complete flags of $F_{q}^{3}$ (Bruhat decomposition of GL_n over a finite field).

Facts & Assumptions

Given: A prime power $q$ , the space $V = F_{q}^{3}$ with standard basis $e_{1}, e_{2}, e_{3}$ and standard flag $V_{∙}$ with $V_{i} = ⟨ e_{1}, \dots, e_{i} ⟩$ , the group $G = {GL}_{3} (F_{q})$ with standard Borel subgroup $B$ , and the six permutations of ${1, 2, 3}$ in one-line notation.

[F1]

For $g \in M_{n} (F_{q})$ the symbol $r_{i, j} (g)$ denotes the rank of the submatrix on the rows $i, i + 1, \dots, n$ and the columns $1, 2, \dots, j$ ; if $g \in B w B$ for a permutation matrix $w = P_{σ}$ , then $r_{i, j} (g) = # {k \leq j : σ (k) \geq i}$ , these ranks are constant on the double coset $B w B$ , and for $g \in G$ the rank matrix determines $σ$ uniquely (Southwest rank matrices determine Bruhat cells, Standard subgroups of finite general linear groups).

[F2]

For a permutation matrix $w = P_{σ}$ one has $w V_{j} = ⟨ e_{σ (1)}, \dots, e_{σ (j)} ⟩$ for the standard flag $V_{∙}$ , and for $x \in G$ and all $i, j$ one has $\dim_{F_{q}} (V_{i} \cap x V_{j}) = j - r_{i + 1, j} (x)$ , with the convention $r_{n + 1, j} (x) : = 0$ (Relative position classifies pairs of complete flags).

[F3]

The map $σ \mapsto B P_{σ} B$ is a bijection from $S_{3}$ onto the set of double cosets $B \ G / B$ , and the relative position $σ (F, E)$ of a pair of complete flags is the element of $S_{3}$ attached to it by Relative position classifies pairs of complete flags; two pairs have the same relative position exactly when they lie in the same diagonal $G$ -orbit on $X \times X$ (Bruhat decomposition of GL_n over a finite field, Relative position classifies pairs of complete flags).

Verification

technique · direct

1.1

For the three permutations $123, 132, 213$ with values $σ (1), σ (2), σ (3)$ equal to $1, 2, 3$ and $1, 3, 2$ and $2, 1, 3$ the defining count of [F1] gives: for $σ = 123$ one has $r_{1, j} = j$ and $r_{i, j} = \max (0, j - i + 1)$ , so the rows are $[1, 2, 3], [0, 1, 2], [0, 0, 1]$ ; for $σ = 132$ the rows are $[1, 2, 3]$ , then $# {k \leq j : σ (k) \geq 2} = [0, 1, 2]$ , then $# {k \leq j : σ (k) \geq 3} = [0, 1, 1]$ ; for $σ = 213$ the rows are $[1, 2, 3]$ , then $# {k \leq j : σ (k) \geq 2} = [1, 1, 2]$ (for $j = 1$ the value $σ (1) = 2$ contributes, for $j = 2$ only $k = 1$ does, for $j = 3$ the values $2$ and $3$ do), then $# {k \leq j : σ (k) \geq 3} = [0, 0, 1]$ .

givenF1

1.2

For the three permutations $231, 312, 321$ with values $2, 3, 1$ and $3, 1, 2$ and $3, 2, 1$ the same count gives: for $σ = 231$ the rows are $[1, 2, 3]$ , then $# {k \leq j : σ (k) \geq 2} = [1, 2, 2]$ , then $# {k \leq j : σ (k) \geq 3} = [0, 1, 1]$ ; for $σ = 312$ the rows are $[1, 2, 3]$ , then $[1, 1, 2]$ , then $[1, 1, 1]$ ; for $σ = 321$ the rows are $[1, 2, 3]$ , then $[1, 2, 2]$ , then $[1, 1, 1]$ .

givenF1

2.1

For each of the six permutations the intersection-dimension matrix is obtained from the rank matrix by the formula of [F2], $D_{i, j} : = j - r_{i + 1, j} (w)$ with $r_{4, j} (w) = 0$ : using the second and third rows listed in steps 1.1 and 1.2 this gives $D_{1, j} = [1, 1, 1]$ for $123$ and $132$ (second rows $[0, 1, 2]$ ), $[0, 1, 1]$ for $213$ and $312$ (second rows $[1, 1, 2]$ ) and $[0, 0, 1]$ for $231$ and $321$ (second rows $[1, 2, 2]$ ); $D_{2, j} = [1, 2, 2]$ for $123$ and $213$ (third rows $[0, 0, 1]$ ), $[1, 1, 2]$ for $132$ and $231$ (third rows $[0, 1, 1]$ ) and $[0, 1, 2]$ for $312$ and $321$ (third rows $[1, 1, 1]$ ); and $D_{3, j} = [1, 2, 3]$ for all six, because $r_{4, j} = 0$ . Explicitly, in the order $123, 132, 213, 231, 312, 321$ these are the six displayed matrices of the Example section, and the formula $r_{i + 1, j} (w) = j - D_{i, j}$ recovers the rank matrix from the intersection-dimension matrix.

step 1.1step 1.2F2

2.2

The six rank matrices are pairwise distinct: those of $123$ and $132$ differ in position $(3, 2)$ , where they are $0$ and $1$ ; each of those of $123, 132$ differs from that of $213$ in position $(2, 1)$ , where $123$ and $132$ have $0$ and $213$ has $1$ ; $213$ and $312$ differ in position $(3, 1)$ , where they are $0$ and $1$ ; $231$ and $321$ differ in position $(3, 1)$ , where they are $0$ and $1$ ; and each of $231, 321$ differs from each of $213, 312$ in position $(2, 2)$ , where $231, 321$ have $2$ and $213, 312$ have $1$ . Since the rank matrices of the six permutations are pairwise distinct and a rank matrix determines its double coset by [F1], the six elements of $S_{3}$ realise six distinct double cosets in $B \ G / B$ , in agreement with the bijection of [F3].

step 1.1step 1.2F1F3

3.1

The six intersection-dimension matrices displayed in the Example section are pairwise distinct as well: the entry $(1, 1)$ equals $1$ for $123$ and $132$ and $0$ for $213, 231, 312, 321$ , so it separates these two groups; within the first group the entry $(2, 2)$ is $2$ for $123$ and $1$ for $132$ ; and within the second group the pair of entries $((1, 2), (2, 1))$ takes the four distinct values $(1, 1), (1, 0), (0, 1), (0, 0)$ for $213, 312, 231, 321$ respectively. Consequently the six permutations of $S_{3}$ give the six pairwise distinct relative positions of pairs of complete flags of $F_{q}^{3}$ , and the intersection dimensions $\dim_{F_{q}} (V_{i} \cap w V_{j})$ are the complete invariant of the diagonal orbit of the pair $(V_{∙}, w V_{∙})$ by [F3]. ∎

step 2.1step 2.2F2F3

Remarks

The example illustrates the complete invariant of Relative position classifies pairs of complete flags at $n = 3$ : the six $3 \times 3$ intersection-dimension matrices, which is equivalent to the southwest rank matrix, distinguishes the $3! = 6$ relative positions, and the first column $\dim (V_{i} \cap w V_{1})$ recovers the least $i$ for which the line $w V_{1}$ lies in $V_{i}$ . For the two extreme permutations the intersection matrices are the pattern $\min (i, j)$ (for $123$ ) and its opposite counterpart $D_{i, j} = \max (0, i + j - 3)$ (for $321$ ), which is the extreme opposite position, while the four remaining matrices are the intermediate positions.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

36 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, printed p. 18 (standard reference, not scraped)
Jay Taylor, Finite Reductive Groups - Section 3.5, printed pp. 37-39 (standard reference, not scraped)