A fraction field of an affine curve is finite over the field of a transcendental linear parameter, of degree at most its affine Hilbert degree. Common denominators transfer arbitrary field elements to polynomial classes.
theorem
CCDN.field_common_multiple_independent
{R : Type u_1}
{F : Type u_2}
{ι : Type u_3}
[Field R]
[Field F]
[Algebra R F]
[Finite ι]
(v : ι → F)
(hv : LinearIndependent R v)
(b : F)
(hb : b ≠ 0)
:
LinearIndependent R fun (i : ι) => b * v i
Multiplying a linearly independent family in a field by a common nonzero element keeps it linearly independent.
theorem
CCDN.curve_functionField_finite_rank_le
{K : Type u_1}
{R : Type u_2}
{F : Type u_3}
{σ : Type u_4}
[Field K]
[Field R]
[Field F]
[Algebra K R]
[Algebra R F]
[Algebra K F]
[IsScalarTower K R F]
(I : Ideal (MvPolynomial σ K))
[I.IsPrime]
[Algebra (MvPolynomial σ K ⧸ I) F]
[IsScalarTower K (MvPolynomial σ K ⧸ I) F]
[IsFractionRing (MvPolynomial σ K ⧸ I) F]
[Finite σ]
(d : ℕ)
(hdegree : HasFilteredCurveDegree I d)
(l : MvPolynomial σ K)
(hl : l.totalDegree ≤ 1)
(u : R)
(hu : Transcendental K u)
(he : (algebraMap (MvPolynomial σ K ⧸ I) F) ((Ideal.Quotient.mk I) l) = (algebraMap R F) u)
:
The function-field extension is finite and has degree at most d.