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:

• https://github.com/leanprover-community/mathlib4/pull/7788#issuecomment-1788132019
• [P. M. Cohn, Basic Algebra: Groups, Rings and Fields][cohn_2003], Theorem 11.3.4
• [N. Jacobson, Basic Algebra II: Second Edition][jacobson1989], Theorem 8.38

noncomputable def RatFunc.Luroth.generator {K : Type u_1} [Field K] (E : IntermediateField K (RatFunc K)) : RatFunc K

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))

theorem RatFunc.Luroth.generator_eq_zero {K : Type u_1} [Field K] {E : IntermediateField K (RatFunc K)} (h : E = ⊥) : generator E = 0

theorem RatFunc.Luroth.generator_mem {K : Type u_1} [Field K] {E : IntermediateField K (RatFunc K)} : generator E ∈ E

theorem RatFunc.Luroth.generator_spec {K : Type u_1} [Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥) : generator E ∉ (algebraMap K (RatFunc K)).range

theorem RatFunc.Luroth.generator_ne_C {K : Type u_1} [Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥) : ¬∃ (c : K), generator E = C c

theorem RatFunc.Luroth.transcendental_generator {K : Type u_1} [Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥) : Transcendental K (generator E)

theorem RatFunc.Luroth.generator_ne_zero {K : Type u_1} [Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥) : generator E ≠ 0

theorem RatFunc.Luroth.adjoin_generator_le {K : Type u_1} [Field K] {E : IntermediateField K (RatFunc K)} : K⟮generator E⟯ ≤ E

theorem RatFunc.Luroth.eq_adjoin_generator {K : Type u_1} [Field K] {E : IntermediateField K (RatFunc K)} : E = K⟮generator E⟯

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 ≠ ⊥.

noncomputable def RatFunc.Luroth.algEquiv {K : Type u_1} [Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥) : RatFunc K ≃ₐ[K] ↥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.

Equations

• RatFunc.Luroth.algEquiv h = (RatFunc.algEquivOfTranscendental (RatFunc.Luroth.generator E) ⋯).trans (IntermediateField.equivOfEq ⋯)

@[simp]

theorem RatFunc.Luroth.algEquiv_algebraMap {K : Type u_1} [Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥) (g : Polynomial K) : ↑((algEquiv h) ((algebraMap (Polynomial K) (RatFunc K)) g)) = (Polynomial.aeval (generator E)) g

@[simp]

theorem RatFunc.Luroth.algEquiv_X {K : Type u_1} [Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥) : ↑((algEquiv h) X) = generator E

theorem RatFunc.Luroth.algEquiv_apply {K : Type u_1} [Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥) (u : RatFunc K) : ↑((algEquiv h) u) = (Polynomial.aeval (generator E)) u.num / (Polynomial.aeval (generator E)) u.denom