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

Borel subgroups of GL_n are flag stabilizers and act on projective space with a fixed line

Example

Assume the Axiom of Choice. Let $k$ be an algebraically closed field, let $V$ be a finite-dimensional $k$ -vector space of dimension $n \geq 1$ and let $G = G L (V)$ (The general linear group scheme and its coordinate ring). The Borel subgroups of $G$ are exactly the stabilizers of maximal flags in $V$ , hence exactly the conjugates of the upper triangular group $T_{n}$ , and each is a semidirect product $U_{n} ⋊ D_{n}$ (The upper unitriangular group scheme U_n and its coordinate ring, Borel subgroups, maximal tori and Borel pairs). The group $T_{n}$ acts on the projective space of lines $P (V)$ with fixed line $⟨ e_{1} ⟩$ , and $G L (V) / T_{n} ≅ F l (V)$ , the complete flag variety, so the Borel fixed point theorem is visible here as the existence of a $T_{n}$ -invariant line: the eigenvector corresponding to the first step of the flag.

Facts & Assumptions

Given: The Axiom of Choice, an algebraically closed field $k$ , a finite-dimensional $k$ -vector space $V$ of dimension $n \geq 1$ , and $G = G L (V)$ .

[F1]

$T_{n} = D_{n} ⋉ U_{n}$ is a closed subgroup scheme of ${G L}_{n}$ , the upper triangular invertible matrices; $D_{n}$ is a diagonalizable torus and $U_{n}$ has a central series with successive quotients $G_{a}$ , so $T_{n}$ is smooth connected and solvable. A smooth connected solvable subgroup of $G$ is trigonalizable: there is a basis of $V$ in which it acts through upper triangular matrices. (The upper unitriangular group scheme U_n and its coordinate ring, The central series of U_n with additive quotients, Lie-Kolchin: smooth connected solvable affine groups over algebraically closed fields are trigonalizable)

[F2]

Assume AC. Any two Borel subgroups of $G$ are conjugate by an element of $G (k)$ , and for every Borel subgroup $B$ the quotient $G / B$ is complete. (Conjugacy of Borel subgroups and of maximal tori over an algebraically closed field)

[F3]

The variety $F l (V)$ of maximal flags is smooth projective, hence separated, finite type and complete; $G L (V)$ acts transitively on it, and the scheme-theoretic stabilizer of the standard flag is $T_{n}$ . The standard flag is a $k$ -point, and $G L (V)$ is smooth of finite type: in a basis it is the determinant-open subscheme $D (\det) \subseteq A_{k}^{n^{2}}$ . Thus the orbit-map lemma applies to this action and gives a locally closed orbit $O_{F}$ and a faithfully flat, locally finitely presented map $G L (V) \to O_{F}$ . Transitivity makes $O_{F}$ contain every closed point of $F l (V)$ ; since it is locally closed and both orbit and flag variety are reduced, $O_{F} = F l (V)$ . The stabilizer of any maximal flag is a closed subgroup scheme conjugate to $T_{n}$ , hence solvable. (Smooth morphism of schemes, The variety of complete flags of a finite-dimensional vector space is smooth projective, The general linear group scheme and its coordinate ring, Smooth orbits are locally closed and their orbit maps are faithfully flat over every field, A Borel subgroup of maximal dimension is the stabilizer of a maximal flag)

[F4]

Assume AC. The standard representation $V$ of $G$ induces a rational action of $G$ , and of each closed subgroup, on the space of lines $P (V)$ , and for a line $L \subseteq V$ the scheme stabilizer of the point $[L]$ has $R$ -points ${g : g L_{R} = L_{R}}$ . (A linear representation induces an action on projective space with the same line stabilizers, Projective bundle in the quotient convention)

[F5]

Assume AC. For a smooth affine group $G$ of finite type and a closed subgroup $H$ , the fppf quotient $G / H$ is representable by a separated finite-type scheme and the orbit map exhibits it as the orbit of the corresponding point of a projective space when $H$ is a line stabilizer; in particular the orbit of the standard flag under $G L (V)$ with stabilizer $T_{n}$ is $G L (V) / T_{n}$ . (Homogeneous spaces of smooth affine groups are separated schemes, A faithfully flat orbit map represents the coset quotient sheaf, A linear representation induces an action on projective space with the same line stabilizers)

Proof

Given: The Axiom of Choice, an algebraically closed field $k$ , a finite-dimensional $k$ -vector space $V$ of dimension $n \geq 1$ , and $G = G L (V)$ .

1.1F1F2

A Borel subgroup $B$ of $G$ is solvable, hence trigonalizable by [F1]: there is a basis $v_{1}, \dots, v_{n}$ of $V$ in which $B$ acts through upper triangular matrices, so $B \subseteq T_{n}$ relative to that basis; maximality of $B$ gives $B = T_{n}$ in that basis. Conversely $T_{n}$ is a Borel subgroup by [F1]: it is connected solvable, and a connected solvable subgroup strictly containing $T_{n}$ would be trigonalizable in a basis of its own, contradicting maximality of the dimension of $T_{n}$ . Hence the Borel subgroups of $G$ are exactly the conjugates of $T_{n}$ , and by [F2] any two of them are conjugate by an element of $G (k)$ .

2.1F1F3step 1.1

A conjugate $g T_{n} g^{- 1}$ is exactly the stabilizer of the flag $g F_{s t d}$ , where $F_{s t d}$ is the standard flag with $i$ -th step $⟨ e_{1}, \dots, e_{i} ⟩$ : an element $h$ stabilizes the flag $F_{s t d}$ if and only if its matrix is upper triangular, so $g T_{n} g^{- 1}$ is the scheme-theoretic stabilizer of $g F_{s t d}$ , and conversely every maximal flag is $g F_{s t d}$ for some $g$ because $G$ acts transitively on bases and maximal flags correspond to bases. Therefore the Borel subgroups of $G$ are exactly the stabilizers of maximal flags in $V$ , and each is a semidirect product $U_{n} ⋊ D_{n}$ by [F1].

3.1F4step 2.1

By [F4] the standard representation makes $G$ , and hence its subgroup $T_{n}$ , act rationally on the space of lines $P (V)$ ; an upper triangular matrix satisfies $g e_{1} = g_{11} e_{1}$ with $g_{11} \in k^{\times}$ , so $g$ preserves the line $⟨ e_{1} ⟩$ . Thus $⟨ e_{1} ⟩$ is a line fixed by all of $T_{n} (k)$ : the Borel fixed point theorem is realized concretely, the fixed line being the first step of the standard flag.

4.1F2F3F5step 3.1

By [F3] the orbit of the standard flag is all of $F l (V)$ , its scheme-theoretic stabilizer is $T_{n}$ , and the orbit map $G L (V) \to F l (V)$ is faithfully flat and locally of finite presentation. The coset-quotient proposition [F5] therefore applies and shows that $F l (V)$ represents the fppf quotient $G L (V) / T_{n}$ . Since $F l (V)$ is complete by [F3], this illustrates the completeness of $G / B$ from [F2] in the special case of $G L (V)$ .

5.1step 2.1step 3.1step 4.1∎

Collecting: the Borel subgroups of $G L (V)$ are the flag stabilizers, equivalently the conjugates of $T_{n} = U_{n} ⋊ D_{n}$ ; the standard maximal flag provides a $T_{n}$ -fixed line in $P (V)$ , and $G L (V) / T_{n} ≅ F l (V)$ is the complete flag variety.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

118 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

J. S. Milne, Algebraic Groups (corrected 2022 printing, Cambridge University Press) (standard reference, not scraped)
Florian Herzig, Linear Algebraic Groups (University of Toronto lecture notes, 2013) (standard reference, not scraped)