Function-field rank bounds for polynomial parameters of bounded degree, obtained from the geometric Hilbert multiplicity. Linear parameters are the case of degree one.
theorem
CCDN.bounded_degree_hilbert_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]
[Fintype σ]
[LinearOrder σ]
(I : Ideal (MvPolynomial σ K))
[I.IsPrime]
[Algebra (MvPolynomial σ K ⧸ I) F]
[IsScalarTower K (MvPolynomial σ K ⧸ I) F]
[IsFractionRing (MvPolynomial σ K ⧸ I) F]
{τ : Type u_5}
[Fintype τ]
(d q : ℕ)
(hq : 0 < q)
(hdimdeg : HasAffineDimensionDegree I (Fintype.card τ) d)
(l : τ → MvPolynomial σ K)
(hl : ∀ (i : τ), (l i).totalDegree ≤ q)
(u : τ → R)
(hu : AlgebraicIndependent K u)
(he : ∀ (i : τ), (algebraMap (MvPolynomial σ K ⧸ I) F) ((Ideal.Quotient.mk I) (l i)) = (algebraMap R F) (u i))
:
The function field is finite over the field generated by the expected number of independent degree-q parameters. Its degree is at most the geometric multiplicity times q to the Hilbert dimension.
theorem
CCDN.hilbert_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]
[Fintype σ]
[LinearOrder σ]
(I : Ideal (MvPolynomial σ K))
[I.IsPrime]
[Algebra (MvPolynomial σ K ⧸ I) F]
[IsScalarTower K (MvPolynomial σ K ⧸ I) F]
[IsFractionRing (MvPolynomial σ K ⧸ I) F]
{τ : Type u_5}
[Fintype τ]
(d : ℕ)
(hdimdeg : HasAffineDimensionDegree I (Fintype.card τ) d)
(l : τ → MvPolynomial σ K)
(hl : ∀ (i : τ), (l i).totalDegree ≤ 1)
(u : τ → R)
(hu : AlgebraicIndependent K u)
(he : ∀ (i : τ), (algebraMap (MvPolynomial σ K ⧸ I) F) ((Ideal.Quotient.mk I) (l i)) = (algebraMap R F) (u i))
:
The function field is finite over any field containing the expected number of independent linear parameters, of rank at most the multiplicity.