Nullstellensatz

Weak Nullstellensatz over an arbitrary algebraically closed field

Open in Workbench View on GitHub

1-- Weak Nullstellensatz over an arbitrary algebraically closed field.2-- Copyright (c) 2026 Grant Passmore.3-- Released under the Apache License 2.0. See LICENSE in the repository root.4-- Authors: Grant Passmore56module NullstellensatzExample7import Grace.Cumulus.Algebra.Polynomial.Nullstellensatz89section Fields10variable (I A add zero neg mul one G : Set)11notation ring R := (A, add, zero, neg, mul, one)12notation ring P := R[I]13hypothesis closed : IsAlgebraicallyClosed(R)14hypothesis finite : Finite(I)15hypothesis generators : G ⊆ P1617theorem unit_iff_unsatisfiable18  shows P[1] ∈ idealSpan(P, G) ↔ ¬(∃ v, PolynomialCommonZero(I, A, add, zero, neg, mul, one, G, v))19proof20  exact polynomialIdeal.unit_iff_no_common_zero with *2122theorem certificate_iff_unsatisfiable23  shows (∃ terms, List(idealProducts(P, G), terms) ∧ P[1] = ringSum{idealProducts(P, G)}(polynomialAdd(I, R), P[0], terms)) ↔ ¬(∃ v, PolynomialCommonZero(I, A, add, zero, neg, mul, one, G, v))24proof25  exact polynomialIdeal.finite_certificate_iff_no_common_zero with *2627end Fields28