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.
A quadratic norm-one torus and its sign action
Example
Assume the Axiom of Choice. Let have characteristic different from , and let be a nonsquare. The affine group , with product , is a nonsplit torus. Its character module is , on which the nontrivial automorphism of acts by . For and , this is the circle group , as an algebraic group over .
Facts & Assumptions
Assume The Axiom of Choice; it is used through the general multiplicative-type classification, whose affineness interface uses fpqc submersiveness.
The local Hopf dictionary is The affine Hopf dictionary used for multiplicative type.
Classification by Galois modules is Multiplicative type groups and Galois character modules.
The free-lattice criterion is Tori correspond exactly to torsion-free character lattices.
Verification
Given: and nonsquare .
The displayed multiplication is multiplication of ; the norm multiplies, so it preserves the equation. The identity is and the inverse is , and associative multiplication follows by direct expansion in the basis . This gives an affine group by F1. Over put . Then , and , give inverse algebra maps with . They preserve multiplication, so .
The nontrivial sends to , so it sends to . F2 gives the sign action on ; F3 makes a torus. It cannot be split: a split rank-one torus has trivial action, and no isomorphism of abelian groups intertwines the sign action with the trivial action (its nonzero generator would have to equal its negative). For over the equation and product are exactly those of unit complex numbers.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
14 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)