Lüroth's theorem #
This file proves Lüroth's theorem, which says that for every field K, every
intermediate field between K and the rational function field K⟮X⟯ is either
K or isomorphic to K(X) as an K-algebra, see Luroth.algEquiv. The proof
depends on the following lemma on degrees of rational functions:
Let f be a rational function, i.e. an element in the field K⟮X⟯.
Let p be its numerator and q its denominator. Then the degree of the
field extension K⟮X⟯/K⟮f⟯ equals the maximum of the degrees of p and q,
see finrank_eq_max_natDegree. Since finrank is defined to be zero when the
extension is infinite, this holds even when f is constant.
References:
The equivalence between E⟮X⟯ and K⟮X⟯ as E-algebras.
Equations
Instances For
The minimal polynomial of X over K⟮f⟯. It is defined as f.num - f * f.denom, viewed
as a polynomial with coefficients in A, where A is a K[f]-algebra.
Equations
- f.minpolyX A = Polynomial.map (algebraMap K A) f.num - Polynomial.C ((algebraMap (↥(Algebra.adjoin K {f})) A) ⟨f, ⋯⟩) * Polynomial.map (algebraMap K A) f.denom
Instances For
A choice of a generator for Lüroth's theorem, see Luroth.eq_adjoin_generator.
Equations
- RatFunc.Luroth.generator E = if h : E = ⊥ then 0 else ↑((RatFunc.Luroth.φ✝ E).coeff (RatFunc.Luroth.generatorIndex✝ h))
Instances For
Lüroth's theorem. Any intermediate field between K and K⟮X⟯ is
generated by a single element generator E. See also transcendental_generator
for the statement that the generator is transcendental if E ≠ ⊥.
The K-algebra equivalence between K⟮X⟯ and an intermediate field E given
by sending X to generator E. See also Luroth.eq_adjoin_generator.