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.
Classical Affine Varieties: Coordinate Rings, Morphisms, and Rational Maps — Examples
1 · Prerequisites
- Algebraic Extensions, Extension Degree, and Finite Fields
- Binary Operations, Monoids, Groups and Subgroups
- Chain Conditions, Semisimple Modules and the Wedderburn–Artin Theorem
- Classical Affine Varieties: Coordinate Rings, Morphisms, and Rational Maps
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Determinants of Matrices over a Commutative Ring
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Eigenvalues, Eigenvectors and the Characteristic Polynomial
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Group Homomorphisms and the Isomorphism Theorems
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Linear Independence, Bases and Dimension
- Modules, Submodules, Quotient Modules and the Isomorphism Theorems
- Noether Normalisation and Nullstellensatz
- Noetherian Rings and Hilbert Basis
- Normal Subgroups and Quotient Groups
- Order, Zorn's Lemma, and the Axiom of Choice
- Polynomial Rings, the Division Algorithm and Roots
- Prime Spectra and Radicals
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Roots, Rational Powers, and Classical Inequalities
- Simple Field Extensions and the Construction of the Complex Numbers
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- Tensor Products of Modules
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- The Field of Fractions and Localisation
- The ZFC Axioms and the Basic Set Constructions
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
The affine line gives an explicit calculation of coordinate rings, point localizations, principal opens and the function field. Polynomial substitution computes the pullback of the squaring morphism in every characteristic.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
The affine-line coordinate, local, and function-field dictionary
Example
Assume the Axiom of Choice, inherited from the Nullstellensatz route. Let be algebraically closed and with coordinate . Then , with residue field k, and . The principal open has coordinate ring and the same function field. The morphism , , pulls back the target coordinate u to . These calculations hold in every characteristic.
Facts & Assumptions
Given: AC, an algebraically closed field , the affine line with coordinate , and a point . Consider also its principal open and the polynomial map .
For the zero ideal in k[t], the vanishing ideal of its locus is its radical (Classical affine algebraic sets correspond to radical ideals, and irreducible sets to prime ideals).
Coordinate rings are quotients by vanishing ideals (The coordinate ring of a classical affine algebraic set).
The local ring at a point is localization at its evaluation ideal (The classical affine local ring is localization at the point's maximal ideal).
The function field is the fraction field (The function field of an irreducible classical affine variety).
Principal-open sections identify with principal localization (Regular functions on a principal open are the principal localization).
Nonempty principal opens are affine (Every nonempty principal open is a classical affine variety).
Coordinate substitution describes pullback of affine morphisms (Classical affine morphisms are contravariantly equivalent to coordinate-ring homomorphisms).
Nonempty affine opens have the same function field (The function field is independent of the chosen nonempty principal affine open).
Verification
The polynomial ring k[t] is a domain: for two nonzero polynomials the product of their nonzero leading coefficients is the nonzero leading coefficient of their product. Thus its zero ideal is radical. F1 gives , so F2 gives . F4 gives .
Evaluation at has kernel : for , the identity proves divisibility when , and the converse follows by evaluation. F3 therefore identifies the local ring with fractions where . Its maximal ideal consists of fractions with and its residue map is . Constants make this map onto k.
For f=t, contains 1. F5 and F6 give its coordinate ring as . The graph realization is with , the inverse of projection being . F8 identifies its fraction field with k(t). For f=0 the open is empty and its function algebra zero; for f=1 the ring is k[t].
The polynomial map is the morphism associated by F7 to , . Explicitly ; in particular , , and . No division by 2 occurs, so this verification includes characteristic 2.
Sources
Source comparison: Milne, Algebraic Geometry, v6.10, 3.17 pp. 63–64, Proposition 3.32 p. 71 and Proposition 3.26 p. 67. Conventions here distinguish arbitrary affine algebraic sets from nonempty irreducible varieties.