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.

Root groups and Bruhat cells for SL_2

Example

Assume the Axiom of Choice inherited from the named suppliers. Let $k$ be any field and $G = {S L}_{2}$ over $k$ with diagonal torus $T_{2} = {diag (x, x^{- 1})}$ , upper triangular Borel $B$ , $U^{+} = {(\binom{1 a}{0 1})}$ and $U^{-} = {(\binom{1 0}{a 1})}$ (The root datum of a split reductive group, Structure of SL_2 and root coordinates, Bruhat decomposition for a split reductive group). The root datum is $X (T_{2}) = Z χ$ with $α = 2 χ$ and $α^{\lor} = χ^{\lor}$ , so $⟨ α, α^{\lor} ⟩ = 2$ and the group is simply connected; the root groups are $U_{\pm α} = U^{\pm}$ , $n_{α} = (\binom{0 1}{- 1 0})$ represents $s_{α}$ , $t u_{α} (a) t^{- 1} = u_{α} (α (t) a)$ , and ${s l}_{2} = t \oplus g_{α} \oplus g_{- α}$ with $\dim g_{\pm α} = 1$ . The Weyl group is $W = {1, s_{α}} ≅ Z / 2$ ; the Bruhat decomposition is $G = B ⊔ B n_{α} B$ with $B n_{α} B = U^{+} n_{α} B$ the open Bruhat cell, parametrized by $U^{+} \times B ≅ A^{1} \times G_{m} \times A^{1}$ ; separately $U^{-} T_{2} U^{+}$ is the open Gaussian cell; on $k$ -points ${S L}_{2} (k) = B (k) ⊔ B (k) n_{α} B (k)$ , while $G / B ≅ P^{1}$ with $G (k)$ acting through ${P G L}_{2} (k)$ . The cell $B$ has dimension $2$ and the open Bruhat cell has dimension $3$ ; the unique longest element $w_{0} = s_{α}$ gives this dense open cell, and the opposite Borel is $B^{-} = U^{-} T$ .

Facts & Assumptions

Given: AC, a field $k$ and $G = {S L}_{2}$ with its diagonal torus $T_{2}$ , Borel $B = U^{+} T_{2}$ and root groups $U^{\pm}$ .

[F1]

The root coordinates of ${S L}_{2}$ : $X (T_{2}) = Z χ$ , $Φ = {\pm 2 χ}$ , $α^{\lor} = χ^{\lor}$ , $n_{α} = u_{α} (1) u_{- α} (- 1) u_{α} (1)$ represents $s_{α}$ , and the conjugation identities hold (Structure of SL_2 and root coordinates, The root datum of a split reductive group).

[F2]

Bruhat decomposition: for a split reductive group, $G = ⨆_{w \in W} B n_{w} B$ , the multiplication $U^{w} \times B \to B n_{w} B$ is an isomorphism, the big cell is open dense with $U^{-} \times T \times U \to G$ an open immersion, and the flag-cell dimensions are $n (w)$ while group cells have dimension $\dim B + n (w)$ (Bruhat decomposition for a split reductive group, Root subgroups of a split reductive group).

[F3]

Homogeneous curves and $Aut (P^{1}) = {P G L}_{2}$ : the quotient of ${S L}_{2}$ by the Borel subgroup is a smooth complete geometrically connected homogeneous curve with the rational base point $B$ , hence $P^{1}$ , with the action of $G$ through ${P G L}_{2}$ (Homogeneous curves and automorphisms of P^1, The root datum of a split reductive group).

Verification

1.1F1givenalgebra

The root datum and root coordinates are those of [F1]: $Φ = {\pm 2 χ}$ with coroot $χ^{\lor}$ and $⟨ α, α^{\lor} ⟩ = 2$ , so the root datum is the simply connected rank-one datum; the root groups are $U_{\pm α} = U^{\pm}$ , and the Lie algebra decomposes as ${s l}_{2} = t \oplus g_{α} \oplus g_{- α}$ with one-dimensional root spaces. The Weyl group is $W = N_{G} (T_{2}) / T_{2} = {1, s_{α}} ≅ Z / 2$ because ${S L}_{2}$ has exactly two Borel subgroups containing $T_{2}$ , namely $B$ and $U^{-} T_{2} = B^{-}$ .

2.1F1F2step 1.1algebra

Write $g = (\begin{array}{cc} a & b \\ c & d \end{array})$ with $a d - b c = 1$ . The cell $B$ is defined by $c = 0$ and has dimension $2$ . If $c \neq 0$ , then $g = u_{α} (a / c) n_{α} diag (- c, - c^{- 1}) u_{α} (d / c)$ by multiplication. Thus $B n_{α} B = U^{+} n_{α} B$ is exactly $c \neq 0$ , parametrized uniquely by $U^{+} \times T_{2} \times U^{+}$ and of dimension $3$ . This proves the two-cell decomposition over $k$ and on $k$ -points. The Gaussian cell $U^{-} T_{2} U^{+}$ is instead $a \neq 0$ , as follows from $g = u_{- α} (c / a) diag (a, a^{- 1}) u_{α} (b / a)$ ; its multiplication map is also an open immersion, but its image differs from $B n_{α} B$ .

3.1F2F3step 2.1algebra∎

Finally $G / B ≅ P^{1}$ by [F3], since the quotient of the connected nonsolvable group ${S L}_{2}$ by the Borel subgroup is a homogeneous curve; the cell decomposition of $G / B$ is ${B} ⊔ Y (s_{α})$ with $Y (s_{α}) = U w_{0} B / B ≅ A^{n (w_{0})} = A^{1}$ , so the two Bruhat cells of the flag variety correspond to the two $T_{2}$ -fixed points of $P^{1}$ ; the action of $G (k)$ factors through ${P G L}_{2} (k) = Aut (P^{1}) (k)$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

41 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)