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.
Global functions on proper integral schemes form a finite extension of the base field
Statement
Assume the Axiom of Choice. Let be a field and let be a nonempty proper integral finite-type -scheme with function field . Then is a finite field extension of contained in .
If in addition is geometrically integral over for the chosen algebraic closure of , then . In particular for every nonempty proper integral finite-type -scheme when is algebraically closed. No Noetherian or reducedness hypothesis is added, and need not be projective.
Facts & Assumptions
Given: A field , a nonempty proper integral finite-type -scheme , its generic point , the function field , and a chosen algebraic closure for the geometrically integral clause. AC is assumed.
is canonically for every nonempty affine open , the extension is finitely generated, and restriction embeds into . Under AC, if is geometrically integral over for , then is a domain. (Function field of an integral finite-type scheme)
An integral scheme is nonempty, reduced, and irreducible. (Integral schemes)
A point is generic when ; in particular lies in every nonempty open subset. (Generic points of irreducible closed subsets)
For a scheme and a ring , taking global sections is a natural bijection . (Morphisms to an affine scheme and global sections)
The standard charts of are and over an affine base , they cover , and their overlap is the open subscheme identified with by the ring isomorphism sending to . For we write , , so , and with . (Relative projective space from standard charts)
A proper morphism is separated, of finite type and universally closed; "proper over " means the structure morphism is proper. (Proper morphisms)
For every scheme and every the diagonal of is a closed immersion, so is separated. (The relative projective-space diagonal is closed)
Assume AC. If is proper and is separated, then every -morphism is proper. (Morphisms from a proper scheme to a separated one are proper)
A proper morphism is a closed map of topological spaces; in particular the image of the whole source is closed. (Proper morphisms are closed)
Points of are prime ideals, , and is the complement of . (The prime spectrum and vanishing sets, Principal distinguished subsets of the prime spectrum)
Every point of an open subset of a spectrum has a distinguished-open neighbourhood inside that open subset. (Every point of a Zariski-open set has a distinguished-open neighbourhood inside it)
If is a finitely generated field extension, the elements of algebraic over form a finite extension of . (A finite-type field has finite relative algebraic constants)
If and is a linear subspace, then is finite-dimensional, , and if and only if . (If and is a linear subspace of , then is finite-dimensional, , and if and only if )
For a linear map with finite-dimensional, . (Rank-nullity: )
If is free with basis and is free with basis , then is free with basis ; dimension is the cardinality of a basis. (The elementary tensors of two bases form the product basis of the tensor product, Finite-dimensional vector space, and its dimension ; infinite-dimensional means having no finite basis)
For -algebras the module carries a unique -algebra structure with and , and commutative give commutative ; the universal property of the module tensor product produces the multiplication map , . (The tensor product of -algebras has multiplication , Universal property of the tensor product for balanced maps into abelian groups)
Assume AC. Every linear subspace of a vector space has a linear complement with . (Every linear subspace of a vector space has a complement: a linear subspace with )
Assume AC. If is algebraic, is algebraically closed and is a field embedding, then extends to a field embedding . (Assuming Choice, a base-field embedding extends across every algebraic extension)
A field is algebraically closed when every nonconstant polynomial over it has a root in it; an algebraic closure of is an algebraically closed field algebraic over . (An algebraically closed field: every nonconstant polynomial has a root in the field, An algebraic closure of a field)
AC states that every family of nonempty sets has a choice function. (The Axiom of Choice)
AC use: Exactly the following suppliers carry the assumption: [F1] in its geometric-integrality clause, [F8], [F17] and [F18]; the remaining facts and all computations are choice-free.
Proof
The scheme is nonempty, reduced and irreducible by [F2], with generic point satisfying by [F3]; the structure morphism is proper, hence separated and of finite type, by [F6]. By [F1], restriction of global sections to the generic point embeds into and is finitely generated.
Fix . Since is a -algebra, there is a unique -algebra homomorphism with , and by [F4] it corresponds to a -morphism ; composing with the open immersion of the standard chart [F5] gives a -morphism with , so .
The morphism is proper: is proper, is separated by [F7], and is a -morphism, so [F8] applies. By [F9] is a closed map, so is closed in ; since is contained in the open chart , it is closed in .
The closure of in is exactly . The map factors as by [F4]. Since the restriction is injective by [F1], the point is the zero prime of the domain , and under contraction. Every point of contains , so its closure is contained in by [F10]. Conversely the closure of the point is by the Zariski closed-set description [F10], and this point lies in ; hence the reverse containment holds.
The image is not all of : otherwise , being the image of the closed map of step 2.1, would be closed in . But lies in the closure of : given an open neighbourhood of in , the open set contains a distinguished open with by [F11]; here , so , and with in the domain the point lies in by [F5] and [F10]. Hence every neighbourhood of meets , so and is not closed — a contradiction.
Consequently : step 2.1 makes closed in , while step 2.2 identifies its closure with , so . By step 3.1 this is a proper subset of , whereas ; hence . Choosing gives in , so is algebraic over . As was arbitrary, inside .
By [F12] the set is a finite extension of , and is a -linear subspace, hence finite-dimensional with by [F13]. Moreover is a subring of a field, hence a domain, and multiplication by is an injective -linear self-map of ; by [F14] its image has dimension , so by [F13] the image is all of , is invertible, and is a field. Thus is a finite field extension of contained in , which is the first assertion.
Now assume that is geometrically integral over for the chosen algebraic closure , so that is a domain by [F1]. Suppose, for contradiction, that the field of step 5.1 is not , and let and . Then is a commutative -algebra by [F16], free with the product basis of [F15]; hence and by [F15]. The multiplication map , , is a surjective -algebra homomorphism by [F16], and .
If were a domain, then it would be a field: for multiplication by is an injective -linear self-map of the finite-dimensional space , its image has dimension by [F14] and hence equals by [F13], so is invertible. A -algebra homomorphism from a field to the nonzero ring is then injective, because its kernel is an ideal of a field and does not contain ; so , contradicting . Hence is not a domain.
But is a domain. Since is a linear subspace, [F17] gives a -linear complement, hence a -linear retraction of the inclusion ; then retracts as a -linear map on , so is injective. By [F18] the embedding extends to a -algebra embedding (the extension is finite, hence algebraic); its underlying -linear injection is retracted by a -linear map supplied by [F17], so is injective. The composite is thus an injective -algebra map [F15, F16] into the domain of [F1]; the image of an injective ring map is a subring of a domain, hence a domain, and is isomorphic to that image, so is a domain, contradicting step 7.1.
Therefore , i.e. , whenever is geometrically integral over . If is algebraically closed and is a nonempty proper integral finite-type -scheme, the chosen algebraic closure satisfies : an algebraic closure is algebraic over by [F19], and an element algebraic over an algebraically closed field lies in it because its minimal polynomial has a root there, so the geometric fibre is , which is integral; the previous conclusion applies and . The empty scheme is excluded by hypothesis, and the zero ring does not occur since is nonempty. The Axiom of Choice [F20] is assumed and is used exactly through the four AC-carrying suppliers [F1], [F8], [F17] and [F18], as recorded in the AC-use line; every other ingredient and computation is choice-free.
Depends on
- Proper morphisms
- Morphisms from a proper scheme to a separated one are proper
- Proper morphisms are closed
- A finite-type field has finite relative algebraic constants
- Function field of an integral finite-type scheme
- Geometric properties of fibres
- The relative projective-space diagonal is closed
- Relative projective space from standard charts
- The Axiom of Choice
- Integral schemes
- Generic points of irreducible closed subsets
- The prime spectrum and vanishing sets
- Principal distinguished subsets of the prime spectrum
- Every point of a Zariski-open set has a distinguished-open neighbourhood inside it
- Morphisms to an affine scheme and global sections
- If $\dim_F V = n$ and $U$ is a linear subspace of $V$, then $U$ is finite-dimensional, $\dim_F U \le n$, and $\dim_F U = n$ if and only if $U = V$
- Rank-nullity: $\dim_F V=\operatorname{nullity}T+\operatorname{rank}T$
- Finite-dimensional vector space, and its dimension $\dim_F V$; infinite-dimensional means having no finite basis
- The elementary tensors of two bases form the product basis of the tensor product
- The tensor product of $R$-algebras has multiplication $(a\otimes b)(a'\otimes b')=aa'\otimes bb'$
- Universal property of the tensor product for balanced maps into abelian groups
- Every linear subspace $U$ of a vector space $V$ has a complement: a linear subspace $W$ with $V = U \oplus W$
- Assuming Choice, a base-field embedding extends across every algebraic extension
- An algebraically closed field: every nonconstant polynomial has a root in the field
- An algebraic closure of a field
Used by
Dependency tree · two levels
135 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
- Stacks Project, Varieties, Lemma 33.9.3 (tag 0BUG) (standard reference, not scraped)
- Vakil, The Rising Sea §§8.3, 11.3, 17.4 (standard reference, not scraped)