Specializations of universal plane sections

Evaluation of a universal section, including the three points obtained from the base point by adding each direction. A nonzero universal witness certifies a geometrically irreducible plane section in characteristic zero, and integer specialization can simultaneously avoid any additional nonzero polynomial condition on the plane parameters.

theorem CCDN.exists_integer_geometrically_good_plane_avoiding {σ : Type u_1} [Finite σ] (f : MvPolynomial (Option σ) ℤ) (hir : AbsolutelyIrreducible f) (hd : 0 < f.totalDegree) (P : MvPolynomial (PlaneParameters (Option σ)) ℤ) (hP : P ≠ 0) : ∃ (v : PlaneParameters (Option σ) → ℤ), (∀ (i : PlaneParameters (Option σ)), 0 ≤ v i ∧ v i ≤ 2 * ↑f.totalDegree ^ 3 + ↑P.totalDegree) ∧ (MvPolynomial.eval v) P ≠ 0 ∧ ((bivariateMap (Int.castRingHom (AlgebraicClosure ℚ))) (universalPlaneSection f v)).natDegree = f.totalDegree ∧ bivariateTotalDegree ((bivariateMap (Int.castRingHom (AlgebraicClosure ℚ))) (universalPlaneSection f v)) = f.totalDegree ∧ Irreducible ((bivariateMap (Int.castRingHom (AlgebraicClosure ℚ))) (universalPlaneSection f v))

Construct an integer plane specialization which is geometrically irreducible of full degree and avoids an additional algebraic condition. The parameter bound is independent of the equation's coefficient height.

noncomputable def CCDN.bivariateEval {K : Type u_1} [CommRing K] (x y : K) : Polynomial (Polynomial K) →+* K

Evaluate the outer coordinate at x and the inner coordinate at y.

Equations

• CCDN.bivariateEval x y = (Polynomial.evalRingHom x).comp (Polynomial.mapRingHom (Polynomial.evalRingHom y))

theorem CCDN.universalPlaneSection_eval {K : Type u_1} {σ : Type u_2} [CommRing K] (f : MvPolynomial σ K) (v : PlaneParameters σ → K) (x y : K) : (bivariateEval x y) (universalPlaneSection f v) = (MvPolynomial.eval fun (i : σ) => v (i, 0) + v (i, 1) * x + v (i, 2) * y) f

Evaluating the universal plane section of f with parameters v at (x, y) gives f at the point a + x • b + y • c of the plane with base point a and directions b, c given by v.

def CCDN.planeTriplePointsEquiv {K : Type u_1} {σ : Type u_2} [CommRing K] : (PlaneParameters σ → K) ≃ (Fin 3 → σ → K)

The equivalence between plane parameters, a base point a with directions b and c, and the three defining points a, a + b and a + c of the plane.

Equations

• One or more equations did not get rendered due to their size.

theorem CCDN.zero_universalPlaneSection_three_points {K : Type u_1} {σ : Type u_2} [CommRing K] (f : MvPolynomial σ K) (v : PlaneParameters σ → K) (hv : universalPlaneSection f v = 0) (j : Fin 3) : (MvPolynomial.eval (planeTriplePointsEquiv v j)) f = 0

A zero section contains all three defining points, including coincident ones. This does not require the parameterization to be injective.