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 character lattice of a split torus

Example

Assume the Axiom of Choice. For every field $k$ , $T = G_{m}^{r}$ has $X^{*} (T) = Z^{r}$ with trivial Galois action. A vector $(n_{1}, \dots, n_{r})$ represents the character $(t_{1}, \dots, t_{r}) \mapsto \prod_{i} t_{i}^{n_{i}}$ . A map $G_{m}^{r} \to G_{m}^{s}$ is therefore an $s$ -tuple of such monomials, or an integer $s \times r$ matrix, in every characteristic.

Facts & Assumptions

[A1]

Assume The Axiom of Choice; it is used through the general multiplicative-type classification, whose affineness interface uses fpqc submersiveness.

[F1]

The complete split character dictionary is Split diagonalizable groups are dual to abelian groups.

[F2]

Galois descent of characters and the torus distinction are Multiplicative type groups and Galois character modules, Tori correspond exactly to torsion-free character lattices.

Verification

Given: $r, s \geq 0$ and a field $k$ .

1.1F1F2algebra

The coordinate algebra is $k [t_{1}^{\pm 1}, \dots, t_{r}^{\pm 1}] = k [Z^{r}]$ . F1 shows that all characters are exactly its monomials; every exponent tuple occurs uniquely. These functions are defined over $k$ , so the entire Galois action is trivial.

2.1A1F1F2step 1.1algebra∎

F1 identifies a map to $G_{m}^{s}$ with a homomorphism $Z^{s} \to Z^{r}$ , determined by the images of the $s$ basis vectors, giving the stated matrix and formulas. The module is torsion-free, so F2 identifies this group as a torus. The same formulas include rank zero and the unique map involving a trivial source or target as appropriate.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

12 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 edition (standard reference, not scraped)
SGA 3, Expose VIII, section 1, Polo–Gille edition (standard reference, not scraped)
SGA 3, Expose X, section 1, Polo–Gille edition (standard reference, not scraped)