Alphabeta MathHow 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.
For a field , is its rational function field; in particular
Statement
For every field , the polynomial ring is an integral domain, and is a field containing an embedded copy of . It is called the rational function field over . In particular, .
Facts & Assumptions
Given: A field .
Every field is an integral domain (Every field is a commutative ring with ; it is an integral domain, and it is a commutative division ring).
If is an integral domain, then is an integral domain (A polynomial ring over an integral domain is an integral domain).
The field of fractions of a domain consists of fractions with nonzero denominator and is a field containing the domain injectively (The field of fractions of an integral domain, is a field and embeds the integral domain ).
Proof
By [F1] and [F2], is an integral domain. Applying [F3] gives the displayed set of fractions, its field structure, and the embedding of .
Taking gives the final assertion.
Depends on
- $\operatorname{Frac}(D)$ is a field and $d\mapsto d/1$ embeds the integral domain $D$
- A polynomial ring over an integral domain is an integral domain
- The field of fractions $\operatorname{Frac}(D)=(D\setminus\{0\})^{-1}D$ of an integral domain
- Every field is a commutative ring with $1 \ne 0$; it is an integral domain, and it is a commutative division ring
Used by
- Fₚ(s,t)/Fₚ(sᵖ,tᵖ) has degree p², infinitely many intermediate fields, and no primitive element Counterexample
- ⋃_n≥0Fₚ(t^1/pⁿ) is an infinite perfect field of characteristic p Example
- F[x]₍ₓ₎ is the ring of rational functions defined at 0, with maximal ideal generated by x and residue field F Example
- For Fₚ(t)/Fₚ(tᵖ), the trace is identically zero Example
- Fₚ(t)/Fₚ(tᵖ) is purely inseparable of degree p and separable degree one Example
- Over Fₚ(t), the polynomial xᵖ-x-t gives a cyclic Artin-Schreier extension Example
- The rational function field ℝ(t) ordered by the eventual sign is an ordered field, worked out Example
- xᵖ-t is irreducible and inseparable over Fₚ(t) Example
- A finitely localized polynomial ring in positive dimension is not a field Lemma
- The rational function field k(t) is not finite over k[t] Lemma
- For a bi-infinite linear recurrence over K, the two half-series satisfy F_+(x)=-F_-(x⁻¹) in K(x) Proposition
- The general polynomial of degree n has Galois group Sₙ Theorem
Dependency tree · two levels
19 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
- The CRing Project, Chapter 13: Fields and Extensions (standard reference, not scraped)