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.

The simple modules of SL_2 and its fundamental representation

Example

Assume the Axiom of Choice inherited from the named suppliers. Let $k$ be a field and $G = {S L}_{2}$ with its diagonal maximal torus $T_{2}$ , upper triangular Borel $B$ and root datum $X (T_{2}) = Z χ$ , $α = 2 χ$ , $α^{\lor} = χ^{\lor}$ (The root datum of a split reductive group, Structure of SL_2 and root coordinates). The fundamental weight is $ω = χ$ , the dominant characters are $X (T_{2})^{+} = {m ω : m \geq 0}$ , and Dominant weights classify the simple rational representations of a split reductive group attaches to each $m \geq 0$ exactly one simple module $L (m)$ , with $L (0)$ the trivial representation and $L (1) = k^{2}$ the standard representation (Weights, dominant weights and the highest-weight order of a rational representation). For every $m$ , $L (m)_{m χ}$ is one-dimensional and all other weights of $L (m)$ belong to ${m χ, (m - 2) χ, \dots, - m χ}$ , each with multiplicity at most one; in particular $\dim_{k} L (m) \leq m + 1$ . If $p = char (k) > 0$ , the vectors $e_{1}^{p}, e_{2}^{p}$ span a two-dimensional simple submodule of the symmetric power $S^{p} (k^{2})$ with highest weight $p χ$ , so this submodule is isomorphic to $L (p)$ , realized as the Frobenius twist of the standard module $L (1)$ through $g \cdot e_{i}^{p} = (g \cdot e_{i})^{p}$ .

Facts & Assumptions

Given: AC; a field $k$ , $G = {S L}_{2}$ with diagonal torus $T_{2}$ , upper triangular Borel $B = T_{2} ⋉ U^{+}$ , root groups $U^{+} = {(\binom{1 a}{0 1})}$ and $U^{-} = {(\binom{1 0}{a 1})}$ , and a prime $p = char (k) > 0$ in the last part.

[F1]

Root coordinates of ${S L}_{2}$ . $X (T_{2}) = Z χ$ , $Φ = {\pm 2 χ}$ , $α = 2 χ$ , $α^{\lor} = χ^{\lor}$ with $⟨ χ, α^{\lor} ⟩ = 1$ , the Weyl group is ${1, s_{α}}$ acting by $s_{α} (χ) = χ - ⟨ χ, α^{\lor} ⟩ α = - χ$ , $u_{α} (a) = (\binom{1 a}{0 1})$ , $u_{- α} (a) = (\binom{1 0}{a 1})$ , and ${S L}_{2}$ is generated by $U^{+}$ and $U^{-}$ (Structure of SL_2 and root coordinates, The root datum of a split reductive group).

[F2]

Classification of simple modules. The map sending a simple rational representation of $G$ to its highest weight is a bijection onto $X (T_{2})^{+}$ ; we write $L (m)$ for the simple module of highest weight $m χ$ (Dominant weights classify the simple rational representations of a split reductive group, Weights, dominant weights and the highest-weight order of a rational representation).

[F3]

Simple modules and primitive vectors. Every simple rational representation $V$ of $G$ contains a primitive vector $v$ , unique up to a nonzero scalar, whose weight is the highest weight $λ$ of $V$ ; one has $V_{λ} = k v$ , every weight $μ$ of $V$ satisfies $μ = λ - \sum m_{α} α$ with $m_{α} \geq 0$ , and the set of weights is stable under the Weyl group (Simple rational representations have a unique highest weight, The normalizer of the torus permutes weight spaces).

[F4]

Modules generated by a primitive vector. If a rational representation $W$ of $G$ is generated as a $G$ -module by a primitive vector $v$ of weight $λ$ , then $W$ is generated as a $U^{-}$ -module by $v$ , and $W = k v \oplus ⨁_{μ < λ} W_{μ}$ with $W_{λ} = k v$ (Modules generated by a primitive vector, Primitive vectors for a Borel pair).

[F5]

Root-group expansion. For a weight vector $v \in V_{λ}$ and any root $β$ there are $v_{i} \in V_{λ + i β}$ with $u_{β} (c) \cdot v = v + \sum_{i \geq 1} c^{i} v_{i}$ , finitely many nonzero (Expansion of a root-group translate of a weight vector).

[F6]

Weight decompositions. The weight spaces of a rational $T_{2}$ -representation are the eigenspaces of the diagonalizable group $T_{2}$ , and every subrepresentation is the direct sum of its intersections with those weight spaces; in particular a nonzero subrepresentation contains a nonzero weight vector (Representations of diagonalizable groups split into character eigenspaces, Rational representations and comodules of an affine group scheme).

[F7]

Symmetric powers. For a $k$ -vector space $V$ , $S^{p} (V)$ is the quotient of $V^{\otimes p}$ by the symmetric relations, with basis $e_{1}^{a} e_{2}^{p - a}$ ( $0 \leq a \leq p$ ) when $V = k^{2}$ ; a representation of $G$ on $V$ induces a rational representation on $S^{p} (V)$ by functoriality, and in characteristic $p$ the Frobenius identity $(x + y)^{p} = x^{p} + y^{p}$ and the binomial expansion hold (Symmetric algebra of a vector space, Rational representations and comodules of an affine group scheme).

For the basis assertion, the maps $e_{1} \mapsto x$ , $e_{2} \mapsto y$ identify $S (k^{2})$ with $k [x, y]$ : the map from the tensor algebra kills the commutator relations, and the inverse sends $x, y$ to the commuting generators $e_{1}, e_{2}$ . Both composites fix the generators, hence are identities. The degree- $p$ monomials therefore form the stated basis. The substitution action of any $g \in {S L}_{2} (R)$ preserves degree and respects the group law; its coefficients are polynomials in the matrix entries, so each symmetric-power action is rational.

Verification

Given: AC; a field $k$ , $G = {S L}_{2}$ with diagonal torus $T_{2}$ , upper triangular Borel $B = T_{2} ⋉ U^{+}$ , root groups $U^{\pm}$ , and a prime $p = char (k) > 0$ in the last part.

Proof technique: direct.

1.1F1F2

With the identification $X (T_{2}) = Z χ$ of [F1], the fundamental weight is $ω = χ$ and $X (T_{2})^{+} = {m χ : m \geq 0}$ , so [F2] gives the simple modules $L (m) = V (m χ)$ for $m \geq 0$ . The trivial representation is one-dimensional hence simple with highest weight $0$ , so $L (0)$ is the trivial representation. The standard representation $k^{2}$ is simple: for any nonzero $v = (a, b)$ one has $(\binom{a 0}{b a^{- 1}}) e_{1} = v$ when $a \neq 0$ and $(\binom{0 - b^{- 1}}{b 0}) e_{1} = v$ when $a = 0$ , so the submodule generated by any nonzero vector is all of $k^{2}$ ; moreover $e_{1}$ is fixed by $U^{+}$ and is a $T_{2}$ -eigenvector of weight $χ$ , so $e_{1}$ is primitive of weight $χ = ω$ and $k^{2} ≅ L (1)$ by [F2].

1.2F3F4F5

Fix $m \geq 0$ and let $v \in L (m)$ be a primitive vector of weight $m χ$ , which exists and is unique up to scalar by [F3]. By [F4] $L (m)$ is generated as a $U^{-}$ -module by $v$ , and $U^{-} = U_{- α} ≅ G_{a}$ . By [F5] write $u_{- α} (c) \cdot v = \sum_{i \geq 0} c^{i} v_{i}$ , where $v_{0} = v$ , $v_{i} \in L (m)_{(m - 2 i) χ}$ , and only finitely many $v_{i}$ are nonzero. Let $W = {span}_{k} {v_{i} : i \geq 0}$ . For every $k$ -algebra $R$ and $a \in R$ , the group law gives $u_{- α} (a) \cdot (u_{- α} (c) \cdot v) = u_{- α} (a + c) \cdot v$ ; comparing coefficients of $c^{j}$ in these polynomial expressions yields $u_{- α} (a) \cdot v_{j} = \sum_{i \geq j} (\binom{i}{j}) a^{i - j} v_{i}$ , so $W_{R}$ is stable under every $U^{-} (R)$ -point. Thus $W$ is a $U^{-}$ -submodule containing $v$ , and [F4] implies $L (m) = W$ . The weights $(m - 2 i) χ$ are distinct, so this is a direct sum of one-dimensional spaces $k v_{i}$ for the nonzero coefficients; hence every weight space of $L (m)$ has dimension at most one.

1.3F7given

Assume now $p = char (k) > 0$ and put $W = k e_{1}^{p} \oplus k e_{2}^{p} \subseteq S^{p} (k^{2})$ . For $g \in {S L}_{2} (R)$ with $g e_{1} = a e_{1} + c e_{2}$ , the multinomial expansion in characteristic $p$ gives $g \cdot e_{1}^{p} = (a e_{1} + c e_{2})^{p} = a^{p} e_{1}^{p} + c^{p} e_{2}^{p} \in W_{R}$ , and likewise $g \cdot e_{2}^{p} = (b e_{1} + d e_{2})^{p} = b^{p} e_{1}^{p} + d^{p} e_{2}^{p} \in W_{R}$ ; thus $W$ is a $G$ -submodule of $S^{p} (k^{2})$ , of dimension two because $e_{1}^{p}, e_{2}^{p}$ are distinct basis monomials. The same computation is the identity $g \cdot e_{i}^{p} = (g \cdot e_{i})^{p}$ .

2.1F1F3step 1.2

If $v_{i} \neq 0$ , then $(m - 2 i) χ$ is a weight of $L (m)$ , so by the Weyl-group stability of [F3] and $s_{α} (χ) = - χ$ of [F1], the character $(2 i - m) χ$ is again a weight; by [F3] applied to $L (m)$ it has the form $(m - 2 j) χ$ with $j \geq 0$ , so $2 i - m = m - 2 j$ , that is $i + j = m$ and $0 \leq i \leq m$ . Hence at most $m + 1$ of the vectors $v_{i}$ are nonzero and $\dim_{k} L (m) \leq m + 1$ ; every weight other than $m χ$ lies in ${(m - 2) χ, \dots, - m χ}$ with multiplicity at most one.

2.2F1F6F7step 1.3

The submodule $W$ is $T_{2}$ -stable with weight spaces $k e_{1}^{p}$ of weight $p χ$ and $k e_{2}^{p}$ of weight $- p χ$ . Let $S \subseteq W$ be a nonzero submodule; by [F6] $S$ contains a nonzero weight vector, hence a nonzero multiple of $e_{1}^{p}$ or of $e_{2}^{p}$ . If $e_{1}^{p} \in S$ , then $u_{- α} (1) \cdot e_{1}^{p} = e_{1}^{p} + e_{2}^{p} \in S$ and hence $e_{2}^{p} \in S$ ; if $e_{2}^{p} \in S$ , then $u_{α} (1) \cdot e_{2}^{p} = e_{2}^{p} + e_{1}^{p} \in S$ and hence $e_{1}^{p} \in S$ . In both cases $S = W$ , so $W$ is simple.

3.1F2F3step 1.3step 2.2∎

Finally $e_{1}^{p}$ is fixed by $U^{+}$ and is a $T_{2}$ -eigenvector of weight $p χ$ , so it is a primitive vector of weight $p χ$ in the simple module $W$ ; the submodule it generates is contained in $W$ by step 1.3 and contains it by step 2.2, so it is all of $W$ , and $p χ$ is dominant. By the classification [F2] the simple module with highest weight $p χ = p ω$ is $L (p)$ , whence $W ≅ L (p)$ . In the basis $e_{1}^{p}, e_{2}^{p}$ of $W$ , step 1.3 gives the entrywise $p$ -th powers of the standard representation matrices. These are the action matrices of the Frobenius twist $L (1)^{(p)}$ . The $k$ -linear map sending its two basis vectors to $e_{1}^{p}, e_{2}^{p}$ is therefore a $G$ -module isomorphism onto $W$ , over every field $k$ of characteristic $p$ .

Remarks

The first part of the verification is the standard weight analysis of the simple ${S L}_{2}$ -modules: the $U^{-}$ -orbit of a highest weight vector has one nonzero coefficient in each admissible weight space, so the weight spaces are one-dimensional and the weights lie between $m χ$ and $- m χ$ .
The computation $g \cdot e_{i}^{p} = (g \cdot e_{i})^{p}$ shows that the $p$ -th symmetric power always contains the Frobenius twist $L (1)^{(p)} ≅ L (p)$ . For $0 \leq m < p$ , $S^{m} (k^{2})$ is simple: a nonzero submodule contains a weight monomial $e_{1}^{a} e_{2}^{m - a}$ by [F6]; the coefficient of $t^{m - a}$ in its universal $U^{+}$ -translate is $e_{1}^{m}$ , so the submodule contains $e_{1}^{m}$ . The universal $U^{-}$ -translate of $e_{1}^{m}$ has coefficients $(\binom{m}{i}) e_{1}^{m - i} e_{2}^{i}$ , all nonzero because $m < p$ , so the submodule is the whole symmetric power. Coefficients belong to the submodule by its coaction criterion, rather than by interpolation over $k$ .

Depends on

Used by

Rational modules need not be semisimple in characteristic p Counterexample

Dependency tree · two levels

59 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)
Robert Steinberg, Lectures on Chevalley Groups (Yale University, 1967; notes prepared by J. Faulkner and R. Wilson) (standard reference, not scraped)