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.
Over an algebraically closed field, every maximal ideal is an evaluation ideal
Statement
Let be an algebraically closed field, and let be a maximal ideal of . Then there is a unique point such that
Facts & Assumptions
Given: An algebraically closed field and a maximal ideal .
A maximal ideal of a finite-type -algebra has finite residue field over (A maximal ideal of an affine algebra has finite residue field over the base field).
Evaluation at a point has kernel (Evaluation at a point has kernel (x_1-a_1, ..., x_n-a_n)).
In an algebraically closed field, every nonconstant polynomial has a root (An algebraically closed field: every nonconstant polynomial has a root in the field).
Proof
By [L1], the residue field is a finite extension of . Let be the image of in .
Each is algebraic over because is finite. Let be its minimal polynomial. Since is algebraically closed, [L3] gives a root of . Minimality forces , so in .
The quotient map is therefore evaluation at the point . Its kernel is , while [L2] says the evaluation kernel is . Hence these ideals are equal. Uniqueness of follows because the quotient remembers each coordinate class .
Depends on
Used by
- Over an algebraically closed field, maximal ideals of an affine algebra are kernels of points Corollary
- A character of a normal subgroup admits an inverse multiple in a group representation Lemma
- A faithful rational action with a fixed point forces affineness Lemma
- A holomorphic extension of a rational map on a product of smooth complex curves is algebraic Lemma
- A smooth geometrically integral algebraic group has an ample line bundle Lemma
- Affine smooth and connected properties in exact sequences of algebraic groups Lemma
- Algebraically closed field extension preserves covers of a smooth proper scheme Lemma
- Classical affine points are maximal ideals Lemma
- Closed finite-index subgroups of rational points of smooth connected groups over algebraically closed fields are the whole point group Lemma
- Composition at points in the domain of a rational group action Lemma
- Connected finite-type groups are geometrically connected Lemma
- Curves without a common component meet finitely often Lemma
- Fibre dimension and orbit dimension add to the dimension of the group Lemma
- Finite-type algebraic group monomorphisms are closed immersions Lemma
- Good quotients are local on the target and are categorical quotients Lemma
- High relative Frobenius has smooth scheme-theoretic image Lemma
- Indeterminacy of a rational map to a group is divisorial Lemma
- Picard representation by generic quotient and translates Lemma
- Points of an affine algebraic set correspond to maximal ideals of its coordinate ring Lemma
- Power maps with exponent prime to the characteristic are bijective on unipotent groups Lemma
- Smooth orbits are locally closed and their orbit maps are faithfully flat over every field Lemma
- The auxiliary ideal is the unit ideal Lemma
- The nilpotent central fiber is reduced and integral Lemma
- Theta extensions, splitting and isotropic descent Lemma
- Base change, freeness and specialization in the deformed family Proposition
- Borel fixed point theorem for complete schemes Theorem
- Classical affine algebraic sets correspond to radical ideals, and irreducible sets to prime ideals Theorem
- Conjugacy of Borel subgroups and of maximal tori over an algebraically closed field Theorem
- Conjugacy of diagonalizable complements and maximal subgroups under smoothness hypotheses Theorem
- Nonzero multiplication on an abelian variety is finite and faithfully flat Theorem
- Normal subgroup quotients of finite-type group schemes exist as fppf scheme quotients Theorem
- Rosenlicht dichotomy for smooth connected algebraic groups Theorem
Dependency tree · two levels
10 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, A Primer of Commutative Algebra, v4.03, Corollary 13.9 (standard reference, not scraped)
- Allen B. Altman and Steven L. Kleiman, A Term of Commutative Algebra, 13th ed., Corollary (15.5) (standard reference, not scraped)