Hilbert degree controls function-field rank over a transcendental linear coordinate. Independent functions over the parameter field produce independent blocks over the constant field, whose filtered growth bounds their number.
theorem
CCDN.tower_smul_independent
{K : Type u_1}
{R : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
[Field K]
[Field R]
[Field F]
[Algebra K R]
[Algebra R F]
[Algebra K F]
[IsScalarTower K R F]
[Finite ι]
[Finite κ]
(v : ι → F)
(hv : LinearIndependent R v)
(u : κ → R)
(hu : LinearIndependent K u)
:
LinearIndependent K fun (t : ι × κ) => u t.2 • v t.1
In a tower K → R → F, the products u k • v i of a family v independent over R and a
family u independent over K are independent over K.
theorem
CCDN.transcendental_powers_independent
{K : Type u_1}
{R : Type u_2}
[Field K]
[CommRing R]
[Algebra K R]
(u : R)
(hu : Transcendental K u)
(N : ℕ)
:
LinearIndependent K fun (i : Fin N) => u ^ ↑i
The powers 1, u, …, u ^ (N - 1) of a transcendental element u are linearly independent.
theorem
CCDN.polynomial_parameter_rank_le
{K : Type u_1}
{R : Type u_2}
{F : Type u_3}
{σ : Type u_4}
{ι : Type u_5}
[Field K]
[Field R]
[Field F]
[Algebra K R]
[Algebra R F]
[Algebra K F]
[IsScalarTower K R F]
[Finite σ]
[Fintype ι]
(I : Ideal (MvPolynomial σ K))
(d : ℕ)
(hdegree : HasFilteredCurveDegree I d)
(φ : MvPolynomial σ K ⧸ I →ₐ[K] F)
(l : MvPolynomial σ K)
(hl : l.totalDegree ≤ 1)
(u : R)
(hu : Transcendental K u)
(he : φ ((Ideal.Quotient.mk I) l) = (algebraMap R F) u)
(h : ι → MvPolynomial σ K)
(hi : LinearIndependent R fun (i : ι) => φ ((Ideal.Quotient.mk I) (h i)))
:
A finite family of polynomial classes independent over a parameter field has cardinality at most the affine Hilbert degree.