A point on a prime component forces a transcendental coordinate and positive eventual Hilbert slope in codimension two.

noncomputable def CCDN.partialCoordinateEval {K : Type u_1} [CommRing K] (c : Fin 3 → K) (n : ℕ) : MvPolynomial (Fin 3) K →+* MvPolynomial (Fin 3) K

Evaluate the first n coordinates, leaving all later coordinates free.

Equations

• CCDN.partialCoordinateEval c n = MvPolynomial.eval₂Hom MvPolynomial.C fun (j : Fin 3) => if ↑j < n then MvPolynomial.C (c j) else MvPolynomial.X j

@[simp]

theorem CCDN.partialCoordinateEval_C {K : Type u_1} [CommRing K] (c : Fin 3 → K) (n : ℕ) (a : K) : (partialCoordinateEval c n) (MvPolynomial.C a) = MvPolynomial.C a

partialCoordinateEval c n fixes constants.

@[simp]

theorem CCDN.partialCoordinateEval_X {K : Type u_1} [CommRing K] (c : Fin 3 → K) (n : ℕ) (j : Fin 3) : (partialCoordinateEval c n) (MvPolynomial.X j) = if ↑j < n then MvPolynomial.C (c j) else MvPolynomial.X j

partialCoordinateEval c n replaces X j by c j for j < n and fixes the other variables.

theorem CCDN.algebraic_eq_scalar_of_point {K : Type u_1} {A : Type u_2} [Field K] [CommRing A] [IsDomain A] [Algebra K A] (φ : A →ₐ[K] K) {y : A} (hy : IsAlgebraic K y) : (algebraMap K A) (φ y) = y

An algebraic element detected by a base-field-valued point is scalar.

noncomputable def CCDN.coordinatePoint {K : Type u_1} {σ : Type u_2} [Field K] (p : Ideal (MvPolynomial σ K)) (z : σ → K) (hz : z ∈ idealZeroLocus p) : MvPolynomial σ K ⧸ p →ₐ[K] K

Evaluation at a rational point descends to its prime coordinate ring.

Equations

• CCDN.coordinatePoint p z hz = Ideal.Quotient.liftₐ p (MvPolynomial.aeval z) ⋯

@[simp]

theorem CCDN.coordinatePoint_mk {K : Type u_1} {σ : Type u_2} [Field K] (p : Ideal (MvPolynomial σ K)) (z : σ → K) (hz : z ∈ idealZeroLocus p) (f : MvPolynomial σ K) : (coordinatePoint p z hz) ((Ideal.Quotient.mk p) f) = (MvPolynomial.eval z) f

Evaluation at the point z sends the class of f to f(z).

theorem CCDN.height_two_transcendental_coordinate_of_point {K : Type u_1} [Field K] (p : Ideal (MvPolynomial (Fin 3) K)) [p.IsPrime] (hp : p.height = 2) (z : Fin 3 → K) (hz : z ∈ idealZeroLocus p) : ∃ (j : Fin 3), Transcendental K ((Ideal.Quotient.mk p) (MvPolynomial.X j))

A height-two prime in three variables containing a rational point retains a transcendental coordinate over its base field.

theorem CCDN.height_two_eventual_slope_pos_of_point {K : Type u_1} [Field K] (p : Ideal (MvPolynomial (Fin 3) K)) [p.IsPrime] (hp : p.height = 2) (z : Fin 3 → K) (hz : z ∈ idealZeroLocus p) {d : ℕ} (hlinear : HasFilteredCurveDegree p d) : 0 < d

A height-two component with a base-field point has positive slope in any eventual linear Hilbert formula, independently of its cutoff.