Quantitative primitive elements and separation by affine coordinates.
theorem
CCDN.exists_bounded_primitive_element
{R : Type u_1}
{F : Type u_2}
[Field R]
[CharZero R]
[Field F]
[Algebra R F]
[Module.Finite R F]
{n : ℕ}
(a : Fin n → F)
(hsep : Function.Injective fun (φ : F →ₐ[R] AlgebraicClosure R) (j : Fin n) => φ (a j))
:
A finite separating coordinate tuple has a primitive integer linear combination with coefficients (1,k,...), where k<=n*[F:R]^2.
theorem
CCDN.exists_bounded_curve_primitive_element
{K : Type u_1}
{R : Type u_2}
{F : Type u_3}
[Field K]
[Field R]
[CharZero R]
[Field F]
[Algebra K R]
[Algebra K F]
[Algebra R F]
[IsScalarTower K R F]
[Module.Finite R F]
{n : ℕ}
(I : Ideal (MvPolynomial (Fin n) K))
[Algebra (MvPolynomial (Fin n) K ⧸ I) F]
[IsScalarTower K (MvPolynomial (Fin n) K ⧸ I) F]
[IsFractionRing (MvPolynomial (Fin n) K ⧸ I) F]
:
∃ k ≤ n * Module.finrank R F ^ 2,
R⟮∑ j : Fin n, (algebraMap (MvPolynomial (Fin n) K ⧸ I) F) ((Ideal.Quotient.mk I) (MvPolynomial.X j)) * ↑k ^ ↑j⟯ = ⊤
The quantitative primitive element applies to the original coordinates of a curve's function field, with no coordinate-generation hypothesis left over.