Common zeros of few polynomials, and irreducibility of nonsingular hypersurfaces

Let K be an algebraically closed field and σ a finite type. Fewer than #σ polynomials that vanish at the origin of K^σ have another common zero there (MvPolynomial.exists_ne_zero_forall_aeval_eq_zero). This is the dimension theorem: their zero set has dimension at least #σ minus their number, so it is not the single point 0. In projective language, with #σ = n + 1, at most n hypersurfaces of ℙⁿ have a common point. The proof is Krull's height theorem together with the Nullstellensatz: if 0 were the only common zero, the maximal ideal of the origin, of height #σ, would be a minimal prime over the ideal the polynomials generate.

In particular two hypersurfaces of ℙⁿ, for n ≥ 2, always meet. At a common point of the factors of a product a * b, the product and all its partial derivatives vanish. So a projective hypersurface G = 0 of dimension at least one whose points over K are all nonsingular is irreducible (TauCeti.irreducible_of_isHomogeneous), since the factors of a homogeneous polynomial are homogeneous. This is the form used by the scheme Proj (k[X₀, …, Xₙ] ⧸ (G)), which is integral for irreducible G. Function fields use the affine form: the equation of G = 0 in a standard affine chart is irreducible over K (TauCeti.irreducible_map_dehomogenize), unless it is a unit. A factorization in the chart lifts to a factorization of G up to a power of the omitted coordinate, by homogenization. For a nonsingular plane curve G = 0 with a point (x : y : 1) in a function field, this makes G(X₀, X₁, 1) the irreducible relation between x and y.

Main results

• MvPolynomial.exists_ne_zero_forall_aeval_eq_zero: fewer than #σ polynomials vanishing at the origin of K^σ have a nonzero common zero.
• MvPolynomial.exists_ne_zero_aeval_mul_eq_zero_and_aeval_pderiv_eq_zero: in at least three variables, a product of two polynomials vanishing at the origin is singular at some point other than the origin.
• TauCeti.irreducible_map_dehomogenize: the affine equation of a nonsingular projective hypersurface of dimension at least one is irreducible over an algebraically closed field.
• TauCeti.irreducible_of_isHomogeneous: a nonsingular homogeneous polynomial of positive degree in at least three variables is irreducible.

References

• R. Hartshorne, Algebraic Geometry, GTM 52, Springer, 1977, Chapter I, Proposition 7.1 and Theorem 7.2 (the affine and projective dimension theorems).
• W. Fulton, Algebraic Curves, Section 5.3, for the irreducibility of a nonsingular projective plane curve.

theorem MvPolynomial.exists_ne_zero_forall_aeval_eq_zero {k : Type u_1} {K : Type u_2} {σ : Type u_3} [Field k] [Field K] [Algebra k K] [IsAlgClosed K] [Finite σ] {s : Finset (MvPolynomial σ k)} (hs : s.card < Nat.card σ) (h0 : ∀ p ∈ s, constantCoeff p = 0) : ∃ (x : σ → K), x ≠ 0 ∧ ∀ p ∈ s, (aeval x) p = 0

The dimension theorem at the origin: let K be an algebraically closed extension of k. Fewer than #σ polynomials in k[X_σ] vanishing at the origin have a common zero in K^σ other than the origin.

theorem MvPolynomial.exists_ne_zero_aeval_mul_eq_zero_and_aeval_pderiv_eq_zero {k : Type u_1} {K : Type u_2} {σ : Type u_3} [Field k] [Field K] [Algebra k K] [IsAlgClosed K] [Finite σ] (hσ : 2 < Nat.card σ) {a b : MvPolynomial σ k} (ha : constantCoeff a = 0) (hb : constantCoeff b = 0) : ∃ (x : σ → K), x ≠ 0 ∧ (aeval x) (a * b) = 0 ∧ ∀ (i : σ), (aeval x) ((pderiv i) (a * b)) = 0

A reducible cone is singular away from its vertex: let K be an algebraically closed extension of k and σ have at least three elements. If a, b ∈ k[X_σ] vanish at the origin, then at some point of K^σ other than the origin, a * b and all its partial derivatives vanish.

theorem TauCeti.irreducible_map_dehomogenize {n d : ℕ} {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsAlgClosed K] (hn : 2 ≤ n) {G : MvPolynomial (Fin (n + 1)) k} (hG : G.IsHomogeneous d) (hsm : ∀ (b : Fin (n + 1) → K), b ≠ 0 → (MvPolynomial.aeval b) G = 0 → ∃ (l : Fin (n + 1)), (MvPolynomial.aeval b) ((MvPolynomial.pderiv l) G) ≠ 0) (i : Fin (n + 1)) (hu : ¬IsUnit ((dehomogenize i) G)) : Irreducible ((MvPolynomial.map (algebraMap k K)) ((dehomogenize i) G))

A nonsingular projective hypersurface is irreducible in its affine charts: let G ∈ k[X₀, …, Xₙ] be homogeneous with n ≥ 2, and suppose that at every point of G = 0 over an algebraically closed extension K of k some partial derivative of G is nonzero. Then the equation of G = 0 in the i-th standard affine chart is irreducible over K, unless it is a unit.

Both hypotheses on the dimension and on units are needed: X₀ X₁ (X₀ - X₁) is nonsingular in ℙ¹, while its equation X₀ (X₀ - 1) in the chart X₁ ≠ 0 is reducible; and the line X₂ = 0 has the unit 1 as its equation in the chart X₂ ≠ 0.

theorem TauCeti.irreducible_of_isHomogeneous {n d : ℕ} {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] [IsAlgClosed K] (hn : 2 ≤ n) {G : MvPolynomial (Fin (n + 1)) k} (hG : G.IsHomogeneous d) (hd : d ≠ 0) (hsm : ∀ (b : Fin (n + 1) → K), b ≠ 0 → (MvPolynomial.aeval b) G = 0 → ∃ (l : Fin (n + 1)), (MvPolynomial.aeval b) ((MvPolynomial.pderiv l) G) ≠ 0) : Irreducible G

A nonsingular projective hypersurface is irreducible: let G ∈ k[X₀, …, Xₙ] be homogeneous of positive degree with n ≥ 2, and suppose that at every point of G = 0 over an algebraically closed extension K of k some partial derivative of G is nonzero. Then G is irreducible.

Taking k = K and the polynomial G with coefficients mapped to K, a nonsingular G is absolutely irreducible. Both hypotheses on the dimension and on the degree are needed: the binary form X₀ X₁ is nonsingular in ℙ¹, and a nonzero constant is a unit.