Dominant polynomial maps

Let p : ι → R[X_j : j ∈ σ] be a polynomial map, and suppose that its Jacobian matrix TauCeti.jacobiMatrixAt p v is surjective at one point v. Then the components of p are algebraically independent: no nonzero polynomial q in the variables ι satisfies q(p) = 0. This holds over every commutative ring. Over an infinite domain, where polynomials are determined by their values, it says that a polynomial vanishing on the image of p is zero, so the image of p is Zariski dense.

This is the density statement behind the injectivity half of Chevalley's restriction theorem: an invariant polynomial function on a semisimple Lie algebra that vanishes on a Cartan subalgebra vanishes on the image of a polynomial parametrization of conjugates of the Cartan subalgebra whose differential is surjective at a regular point, and is therefore zero.

Over an algebraically closed field, a dominant polynomial map is more than Zariski dense: its image contains a nonempty principal open set. By Chevalley's theorem (PrimeSpectrum.isConstructible_comap_image) the image of Spec K[X_j] → Spec K[Y_i] is constructible, and it is dense because the pullback aeval p is injective, so it contains a nonempty basic open set D(g). The Nullstellensatz then lifts each closed point of D(g) to a K-point. Applied to the polynomial parametrizations of the conjugates of two Cartan subalgebras, this gives a point common to both families of conjugates, which is how Cartan subalgebras are shown to be conjugate.

Main results

• TauCeti.algebraicIndependent_of_mulVec_surjective_jacobiMatrixAt: a polynomial family whose Jacobian matrix is surjective at some point is algebraically independent.
• TauCeti.eq_zero_of_forall_eval_eq_zero_of_mulVec_surjective_jacobiMatrixAt: over an infinite domain, a polynomial vanishing on the image of such a polynomial map is zero.
• AlgebraicIndependent.exists_ne_zero_setOf_eval_ne_zero_subset_range: over an algebraically closed field, the image of a polynomial map with algebraically independent components contains the complement of the zero locus of a nonzero polynomial.

References

• The Stacks Project, Tag 00FV, Hilbert Nullstellensatz.

theorem TauCeti.algebraicIndependent_of_mulVec_surjective_jacobiMatrixAt {R : Type u_1} {σ : Type u_2} {ι : Type u_3} [CommRing R] [Fintype σ] [Finite ι] {p : ι → MvPolynomial σ R} {v : σ → R} (hJ : Function.Surjective (jacobiMatrixAt p v).mulVec) : AlgebraicIndependent R p

A polynomial family whose Jacobian matrix is surjective at a point is algebraically independent. If the Jacobian matrix of p : ι → R[X_j : j ∈ σ] is surjective at one point v, then a polynomial q in the variables ι with q(p) = 0 is zero.

theorem TauCeti.eq_zero_of_forall_eval_eq_zero_of_mulVec_surjective_jacobiMatrixAt {R : Type u_1} {σ : Type u_2} {ι : Type u_3} [CommRing R] [IsDomain R] [Infinite R] [Fintype σ] [Finite ι] {p : ι → MvPolynomial σ R} {v : σ → R} (hJ : Function.Surjective (jacobiMatrixAt p v).mulVec) {q : MvPolynomial ι R} (hq : ∀ (x : σ → R), (MvPolynomial.eval fun (i : ι) => (MvPolynomial.eval x) (p i)) q = 0) : q = 0

A polynomial vanishing on the image of a polynomial map with surjective differential at a point is zero. Over an infinite domain, if q(p(x)) = 0 at every point x and the Jacobian matrix of p is surjective at one point v, then q = 0.

theorem AlgebraicIndependent.exists_ne_zero_setOf_eval_ne_zero_subset_range {K : Type u_1} {σ : Type u_2} {ι : Type u_3} [Field K] [IsAlgClosed K] [Finite σ] [Finite ι] {p : ι → MvPolynomial σ K} (hp : AlgebraicIndependent K p) : ∃ (g : MvPolynomial ι K), g ≠ 0 ∧ {y : ι → K | (MvPolynomial.eval y) g ≠ 0} ⊆ Set.range fun (x : σ → K) (i : ι) => (MvPolynomial.eval x) (p i)

The image of a dominant polynomial map contains a nonempty principal open set. Over an algebraically closed field K, if the components of p : ι → K[X_j : j ∈ σ] are algebraically independent, then there is a nonzero polynomial g in the variables ι such that every point y with g(y) ≠ 0 is a value p(x) of the polynomial map p.