Irreducible plane sections transverse to a prescribed direction. The avoidance condition also ensures that a second equation restricts nontrivially, by requiring its value at the plane's base point to be nonzero.

noncomputable def CCDN.affinePlaneMap {K : Type u_1} {σ : Type u_2} [CommRing K] (a b c : σ → K) : MvPolynomial σ K →ₐ[K] MvPolynomial (Fin 2) K

The algebra map restricting a polynomial to the plane parametrized by (s, t) ↦ a + s b + t c, sending Xᵢ to aᵢ + bᵢ X 0 + cᵢ X 1.

Equations

• CCDN.affinePlaneMap a b c = MvPolynomial.aeval fun (i : σ) => MvPolynomial.C (a i) + MvPolynomial.C (b i) * MvPolynomial.X 0 + MvPolynomial.C (c i) * MvPolynomial.X 1

theorem CCDN.affinePlaneMap_eval {K : Type u_1} {σ : Type u_2} [CommRing K] (a b c : σ → K) (f : MvPolynomial σ K) (z : Fin 2 → K) : (MvPolynomial.eval z) ((affinePlaneMap a b c) f) = (MvPolynomial.eval fun (i : σ) => a i + b i * z 0 + c i * z 1) f

Evaluating the restriction of f to the plane a + s b + t c at z gives the value of f at a + z 0 • b + z 1 • c.

theorem CCDN.affinePlaneMap_totalDegree_le {K : Type u_1} {σ : Type u_2} [CommRing K] (a b c : σ → K) (f : MvPolynomial σ K) : ((affinePlaneMap a b c) f).totalDegree ≤ f.totalDegree

Restricting a polynomial to an affine plane does not increase its total degree.

def CCDN.planeDirectionMatrix {K : Type u_1} (b c v : Fin 3 → K) : Matrix (Fin 3) (Fin 3) K

The 3 × 3 matrix with columns b, c and v; over a field, its determinant is nonzero exactly when b, c and v are linearly independent.

Equations

• CCDN.planeDirectionMatrix b c v i j = ![b i, c i, v i] j

theorem CCDN.exists_surface_transverse_plane (f : MvPolynomial (Fin 3) ℤ) (hir : AbsolutelyIrreducible f) (hd : 0 < f.totalDegree) (v : Fin 3 → ℚ) (hv : v ≠ 0) (g : MvPolynomial (Fin 3) ℚ) (hg : g ≠ 0) : ∃ (a : Fin 3 → ℚ) (b : Fin 3 → ℚ) (c : Fin 3 → ℚ), (planeDirectionMatrix b c v).det ≠ 0 ∧ Irreducible ((affinePlaneMap a b c) ((MvPolynomial.map (Int.castRingHom ℚ)) f)) ∧ ((affinePlaneMap a b c) ((MvPolynomial.map (Int.castRingHom ℚ)) f)).totalDegree = f.totalDegree ∧ (affinePlaneMap a b c) g ≠ 0

A geometrically irreducible surface admits a transverse plane whose restriction of any prescribed nonzero second equation is nonzero.