Hypersurface projection kernels in arbitrary dimension. The proper-intersection estimate excludes a second independent equation.
theorem
CCDN.hypersurface_map_eq_zero_iff_dvd
{K : Type u_1}
{A : Type u_2}
[Field K]
[CommRing A]
[Nontrivial A]
[Algebra K A]
{n : ℕ}
(f : MvPolynomial (Fin (n + 2)) K)
(hf : Irreducible f)
(ψ : MvPolynomial (Fin (n + 2)) K →ₐ[K] A)
(hψ : ψ f = 0)
(b : Fin (n + 1) → MvPolynomial (Fin (n + 2)) K)
(hb : ∀ (i : Fin (n + 1)), (b i).totalDegree ≤ 1)
(hi : AlgebraicIndependent K fun (i : Fin (n + 1)) => ψ (b i))
(g : MvPolynomial (Fin (n + 2)) K)
:
An irreducible equation generates the whole kernel whenever the image contains the expected number of independent linear coordinates.
theorem
CCDN.exists_hypersurface_projection_equation
{K : Type u_1}
{τ : Type u_2}
[Field K]
[Fintype τ]
[LinearOrder τ]
{n : ℕ}
(I : Ideal (MvPolynomial τ K))
[I.IsPrime]
(a : Fin (n + 2) → MvPolynomial τ K)
(ha : ∀ (i : Fin (n + 2)), (a i).totalDegree ≤ 1)
(hd : (filteredHilbertPolynomial I).natDegree < n + 2)
(b : Fin (n + 1) → MvPolynomial (Fin (n + 2)) K)
(hb : ∀ (i : Fin (n + 1)), (b i).totalDegree ≤ 1)
(hi : AlgebraicIndependent K fun (i : Fin (n + 1)) => (projectionCoordinateMap I a) (b i))
:
∃ (f : MvPolynomial (Fin (n + 2)) K), Irreducible f ∧ RingHom.ker (projectionCoordinateMap I a) = Ideal.span {f}
A linear projection with one more coordinate than Hilbert dimension and an independent subtuple has a principal prime equation.