NullstellensatzCertificate

The certificate-soundness groundwork for Hilbert's Nullstellensatz

Open in Workbench View on GitHub

1-- The certificate-soundness groundwork for Hilbert's Nullstellensatz.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module NullstellensatzCertificate8import Grace.Cumulus.Algebra.Ring910section Rings11variable (A add zero neg mul one G p q a b : Set)12hypothesis source : IsCommRing(A, add, zero, neg, mul, one)13hypothesis bounded : G ⊆ A14hypothesis hp : p ∈ G15hypothesis hq : q ∈ G16hypothesis ha : a ∈ A17hypothesis hb : b ∈ A18notation ring R := (A, add, zero, neg, mul, one)19hypothesis identity : a * p + b * q = 12021theorem unit_certificate22  shows 1 ∈ idealSpan(A, add, zero, neg, mul, G)23proof24  exact idealSpan.unit_of_linear_combination2 with source, bounded, hp, hq, ha, hb, identity2526section Evaluations27variable (f B plus z minus times unit : Set)28hypothesis target : IsCommRing(B, plus, z, minus, times, unit)29hypothesis hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)30hypothesis nontrivial : Nontrivial(B, z, unit)31notation ring S := (B, plus, z, minus, times, unit)3233theorem no_common_zero34  shows ¬(∀ g ∈ G, f(g) = S[0])35proof36  have certificate := idealSpan.unit_of_linear_combination2 with source, bounded, hp, hq, ha, hb, identity37  exact idealSpan.unit_obstructs_vanishing with source, target, hom, nontrivial, bounded, certificate3839end Evaluations40end Rings41