Zariski closure of sets of points

Let K be a field and k a field with K a k-algebra. The Zariski closure of a set S ⊆ K^σ with respect to equations over k is Z(I(S)), the common zero locus in K^σ of the ideal of polynomials in k[X_σ] vanishing on S. This file packages it as a ClosureOperator on Set (σ → K), built from Mathlib's Galois connection MvPolynomial.zeroLocus_vanishingIdeal_galoisConnection. Its closed sets are exactly the zero loci of ideals of k[X_σ], so the general closure-operator API (ClosureOperator.le_closure, ClosureOperator.monotone, ClosureOperator.idempotent, ClosureOperator.closure_min, ...) supplies extensivity, monotonicity, idempotence and minimality among zero loci.

No algebraic closedness of K is assumed, so no Nullstellensatz is used: over ℝ, for instance, the closure is still the smallest real zero locus of real equations containing S.

A box ∏ᵢ sᵢ whose sides are infinite subsets of K is Zariski dense, since only the zero polynomial vanishes on it; for instance the closed half-line [0, ∞) is Zariski dense in ℝ. Polynomial maps send the closure of a set into the closure of its image. Over finitely many coordinates kernels of K-linear maps are closed, so a K-linear map f with a K-linear left inverse on a set S keeps that left inverse on the closure of S, commutes with the closure of S, and preserves and reflects closedness of S; invertible K-linear changes of coordinates are a special case. Extension by zero along an injective map of coordinate types, such as the zero-padding of coefficient vectors when a degree bound is raised, also commutes with the closure and preserves and reflects closedness, for any number of coordinates; the padding coordinates vanish on the closure.

Over an infinite field, a point that is the limit at t = 0 of a family x + t • v lying in S for t ≠ 0 is in the Zariski closure of S: a polynomial vanishing on S restricts to a one-variable polynomial with infinitely many roots, so it also vanishes at t = 0. This is the algebraic form of a degeneration argument. The analogue for the usual closure needs a topological field in which 0 is not isolated: then x is the limit of the points x + t • v as t → 0 with t ≠ 0, by continuity of t ↦ x + t • v. Over a discrete field, for instance, it fails.

Main definitions and results

• MvPolynomial.zariskiClosure: the closure operator S ↦ Z(I(S)).
• MvPolynomial.zariskiClosure_isClosed_iff: the closed sets are the zero loci of ideals.
• MvPolynomial.vanishingIdeal_zariskiClosure: I(Z(I(S))) = I(S).
• MvPolynomial.zariskiClosure_pi_eq_univ: a box with infinite sides is Zariski dense.
• MvPolynomial.image_zariskiClosure_subset_zariskiClosure_image: polynomial maps are continuous for the Zariski closure.
• MvPolynomial.zariskiClosure_isClosed_ker: kernels of linear maps are closed.
• MvPolynomial.zariskiClosure_image_linearMap_of_leftInvOn: a linear map with a linear left inverse on S commutes with the closure of S.
• MvPolynomial.zariskiClosure_image_linearEquiv: invariance under linear coordinate changes.
• MvPolynomial.zariskiClosure_image_extendByZero: invariance under extension by zero along an injective map of coordinate types.
• MvPolynomial.mem_zeroLocus_vanishingIdeal_of_forall_add_smul_mem: the Zariski closure of a set containing a punctured line contains the missing point.

def MvPolynomial.zariskiClosure (k : Type u_1) {K : Type u_2} {σ : Type u_3} [Field k] [Field K] [Algebra k K] : ClosureOperator (Set (σ → K))

The Zariski closure of a set S ⊆ K^σ with respect to equations over k: the common zero locus of all polynomials in k[X_σ] vanishing on S. Its closed sets are the zero loci of ideals of k[X_σ].

theorem MvPolynomial.zariskiClosure_apply {k : Type u_1} {K : Type u_2} {σ : Type u_3} [Field k] [Field K] [Algebra k K] (S : Set (σ → K)) : (zariskiClosure k) S = zeroLocus K (vanishingIdeal k S)

The Zariski closure is the zero locus of the vanishing ideal.

@[simp]

theorem MvPolynomial.mem_zariskiClosure_iff {k : Type u_1} {K : Type u_2} {σ : Type u_3} [Field k] [Field K] [Algebra k K] {S : Set (σ → K)} {x : σ → K} : x ∈ (zariskiClosure k) S ↔ ∀ (p : MvPolynomial σ k), (∀ y ∈ S, (aeval y) p = 0) → (aeval x) p = 0

A point lies in the Zariski closure of S exactly when every polynomial over k vanishing on S also vanishes at that point.

theorem MvPolynomial.zariskiClosure_isClosed_iff {k : Type u_1} {K : Type u_2} {σ : Type u_3} [Field k] [Field K] [Algebra k K] {S : Set (σ → K)} : (zariskiClosure k).IsClosed S ↔ ∃ (I : Ideal (MvPolynomial σ k)), zeroLocus K I = S

The sets closed for the Zariski closure are exactly the zero loci of ideals of k[X_σ].

theorem MvPolynomial.zariskiClosure_isClosed_zeroLocus {k : Type u_1} {K : Type u_2} {σ : Type u_3} [Field k] [Field K] [Algebra k K] (I : Ideal (MvPolynomial σ k)) : (zariskiClosure k).IsClosed (zeroLocus K I)

The zero locus of an ideal is closed for the Zariski closure.

@[simp]

theorem MvPolynomial.zariskiClosure_zeroLocus {k : Type u_1} {K : Type u_2} {σ : Type u_3} [Field k] [Field K] [Algebra k K] (I : Ideal (MvPolynomial σ k)) : (zariskiClosure k) (zeroLocus K I) = zeroLocus K I

The Zariski closure of a zero locus is that zero locus.

theorem MvPolynomial.zariskiClosure_le_zeroLocus_iff {k : Type u_1} {K : Type u_2} {σ : Type u_3} [Field k] [Field K] [Algebra k K] {S : Set (σ → K)} {I : Ideal (MvPolynomial σ k)} : (zariskiClosure k) S ⊆ zeroLocus K I ↔ S ⊆ zeroLocus K I

The Zariski closure of S is the smallest zero locus containing S: it lies in a zero locus exactly when S does.

@[simp]

theorem MvPolynomial.vanishingIdeal_zariskiClosure {k : Type u_1} {K : Type u_2} {σ : Type u_3} [Field k] [Field K] [Algebra k K] (S : Set (σ → K)) : vanishingIdeal k ((zariskiClosure k) S) = vanishingIdeal k S

A set and its Zariski closure have the same vanishing ideal.

@[simp]

theorem MvPolynomial.zariskiClosure_empty {k : Type u_1} {K : Type u_2} {σ : Type u_3} [Field k] [Field K] [Algebra k K] : (zariskiClosure k) ∅ = ∅

The empty set is Zariski closed.

@[simp]

theorem MvPolynomial.zariskiClosure_univ {k : Type u_1} {K : Type u_2} {σ : Type u_3} [Field k] [Field K] [Algebra k K] : (zariskiClosure k) Set.univ = Set.univ

The whole affine space is Zariski closed.

theorem MvPolynomial.vanishingIdeal_pi_eq_bot {k : Type u_1} {K : Type u_2} {σ : Type u_3} [Field k] [Field K] [Algebra k K] {s : σ → Set K} (hs : ∀ (i : σ), (s i).Infinite) : vanishingIdeal k (Set.univ.pi s) = ⊥

Only the zero polynomial over k vanishes on a box ∏ᵢ sᵢ ⊆ K^σ whose sides are infinite.

theorem MvPolynomial.zariskiClosure_pi_eq_univ {k : Type u_1} {K : Type u_2} {σ : Type u_3} [Field k] [Field K] [Algebra k K] {s : σ → Set K} (hs : ∀ (i : σ), (s i).Infinite) : (zariskiClosure k) (Set.univ.pi s) = Set.univ

A box ∏ᵢ sᵢ ⊆ K^σ whose sides are infinite is Zariski dense.

theorem MvPolynomial.image_zariskiClosure_subset_zariskiClosure_image {k : Type u_1} {K : Type u_2} {σ : Type u_3} {τ : Type u_4} [Field k] [Field K] [Algebra k K] (P : τ → MvPolynomial σ k) (S : Set (σ → K)) : (fun (x : σ → K) (t : τ) => (aeval x) (P t)) '' (zariskiClosure k) S ⊆ (zariskiClosure k) ((fun (x : σ → K) (t : τ) => (aeval x) (P t)) '' S)

A polynomial map x ↦ (aeval x (P t))ₜ sends the Zariski closure of a set into the Zariski closure of its image.

theorem MvPolynomial.image_zariskiClosure_subset_zariskiClosure_image_linearMap {K : Type u_2} {σ : Type u_3} {τ : Type u_4} [Field K] [Finite σ] (f : (σ → K) →ₗ[K] τ → K) (S : Set (σ → K)) : ⇑f '' (zariskiClosure K) S ⊆ (zariskiClosure K) (⇑f '' S)

Over finitely many source coordinates, a K-linear map sends the Zariski closure of a set into the Zariski closure of its image.

theorem MvPolynomial.zariskiClosure_isClosed_ker {K : Type u_2} {σ : Type u_3} {τ : Type u_4} [Field K] [Finite σ] (u : (σ → K) →ₗ[K] τ → K) : (zariskiClosure K).IsClosed ↑u.ker

Over finitely many source coordinates, the kernel of a K-linear map is Zariski closed.

theorem MvPolynomial.leftInvOn_zariskiClosure {K : Type u_2} {σ : Type u_3} {τ : Type u_4} [Field K] [Finite σ] (f : (σ → K) →ₗ[K] τ → K) (g : (τ → K) →ₗ[K] σ → K) {S : Set (σ → K)} (h : Set.LeftInvOn (⇑g) (⇑f) S) : Set.LeftInvOn (⇑g) (⇑f) ((zariskiClosure K) S)

Over finitely many coordinates, if K-linear maps f and g satisfy g (f x) = x for every x ∈ S, then they do so on the Zariski closure of S.

theorem MvPolynomial.zariskiClosure_image_linearMap_of_leftInvOn {K : Type u_2} {σ : Type u_3} {τ : Type u_4} [Field K] [Finite σ] [Finite τ] (f : (σ → K) →ₗ[K] τ → K) (g : (τ → K) →ₗ[K] σ → K) {S : Set (σ → K)} (h : Set.LeftInvOn (⇑g) (⇑f) S) : (zariskiClosure K) (⇑f '' S) = ⇑f '' (zariskiClosure K) S

Over finitely many coordinates, a K-linear map f admitting a K-linear left inverse on S commutes with the Zariski closure of S.

theorem MvPolynomial.zariskiClosure_isClosed_image_linearMap_iff_of_leftInvOn {K : Type u_2} {σ : Type u_3} {τ : Type u_4} [Field K] [Finite σ] [Finite τ] (f : (σ → K) →ₗ[K] τ → K) (g : (τ → K) →ₗ[K] σ → K) {S : Set (σ → K)} (h : Set.LeftInvOn (⇑g) (⇑f) S) : (zariskiClosure K).IsClosed (⇑f '' S) ↔ (zariskiClosure K).IsClosed S

Over finitely many coordinates, a K-linear map f admitting a K-linear left inverse on S preserves and reflects Zariski closedness of S.

theorem MvPolynomial.zariskiClosure_image_linearEquiv {K : Type u_2} {σ : Type u_3} {τ : Type u_4} [Field K] [Finite σ] (e : (σ → K) ≃ₗ[K] τ → K) (S : Set (σ → K)) : (zariskiClosure K) (⇑e '' S) = ⇑e '' (zariskiClosure K) S

An invertible K-linear change of finitely many coordinates commutes with the Zariski closure.

theorem MvPolynomial.zariskiClosure_isClosed_image_linearEquiv_iff {K : Type u_2} {σ : Type u_3} {τ : Type u_4} [Field K] [Finite σ] (e : (σ → K) ≃ₗ[K] τ → K) {S : Set (σ → K)} : (zariskiClosure K).IsClosed (⇑e '' S) ↔ (zariskiClosure K).IsClosed S

An invertible K-linear change of finitely many coordinates preserves and reflects Zariski closedness.

theorem MvPolynomial.apply_eq_zero_of_mem_zariskiClosure_image_extendByZero {k : Type u_1} {K : Type u_2} {σ : Type u_3} {τ : Type u_4} [Field k] [Field K] [Algebra k K] (s : σ → τ) {S : Set (σ → K)} {x : τ → K} (hx : x ∈ (zariskiClosure k) (⇑(Function.ExtendByZero.linearMap K K s) '' S)) {t : τ} (ht : t ∉ Set.range s) : x t = 0

Every point in the Zariski closure of a set extended by zero along s : σ → τ vanishes at the coordinates outside the range of s.

theorem MvPolynomial.zariskiClosure_image_extendByZero {k : Type u_1} {K : Type u_2} {σ : Type u_3} {τ : Type u_4} [Field k] [Field K] [Algebra k K] {s : σ → τ} (hs : Function.Injective s) (S : Set (σ → K)) : (zariskiClosure k) (⇑(Function.ExtendByZero.linearMap K K s) '' S) = ⇑(Function.ExtendByZero.linearMap K K s) '' (zariskiClosure k) S

For injective s : σ → τ, extension by zero along s commutes with the Zariski closure. No finiteness of the coordinates is needed.

theorem MvPolynomial.zariskiClosure_isClosed_image_extendByZero_iff {k : Type u_1} {K : Type u_2} {σ : Type u_3} {τ : Type u_4} [Field k] [Field K] [Algebra k K] {s : σ → τ} (hs : Function.Injective s) {S : Set (σ → K)} : (zariskiClosure k).IsClosed (⇑(Function.ExtendByZero.linearMap K K s) '' S) ↔ (zariskiClosure k).IsClosed S

For injective s : σ → τ, extension by zero along s preserves and reflects Zariski closedness.

theorem MvPolynomial.mem_zeroLocus_vanishingIdeal_of_forall_add_smul_mem {k : Type u_1} {K : Type u_2} {σ : Type u_3} [Field k] [Field K] [Algebra k K] [Infinite K] {S : Set (σ → K)} {x v : σ → K} (h : ∀ (t : K), t ≠ 0 → x + t • v ∈ S) : x ∈ zeroLocus K (vanishingIdeal k S)

Over an infinite field, a point x lies in the Zariski closure of any set S containing the points x + t • v for all t ≠ 0.