Finite evaluation tests for polynomial submodules

A finitely generated submodule of multivariate polynomials over an integral domain is separated by finitely many evaluations. The evaluation points can be chosen in any box with infinite sides. In particular, one finite set tests all polynomials with a prescribed total degree bound, rather than depending on the coefficients of the polynomial being tested.

theorem Submodule.exists_finset_eq_zero_iff_forall_eval_eq_zero {σ : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] (V : Submodule R (MvPolynomial σ R)) [Module.Finite R ↥V] (s : σ → Set R) (hs : ∀ (i : σ), (s i).Infinite) : ∃ (T : Finset (σ → R)), ↑T ⊆ Set.univ.pi s ∧ ∀ p ∈ V, p = 0 ↔ ∀ v ∈ T, (MvPolynomial.eval v) p = 0

Finitely many evaluations in a box with infinite sides detect zero in a finitely generated submodule of polynomials over an integral domain.

theorem TauCeti.exists_finset_eq_zero_iff_forall_eval_eq_zero_of_totalDegree_le {σ : Type u_1} {R : Type u_2} [CommRing R] [IsDomain R] [Finite σ] (D : ℕ) (s : σ → Set R) (hs : ∀ (i : σ), (s i).Infinite) : ∃ (T : Finset (σ → R)), ↑T ⊆ Set.univ.pi s ∧ ∀ (p : MvPolynomial σ R), p.totalDegree ≤ D → (p = 0 ↔ ∀ v ∈ T, (MvPolynomial.eval v) p = 0)

A fixed finite set in a box with infinite sides tests zero for every polynomial of total degree at most D over an integral domain.