Grace/Cumulus/Algebra/Polynomial/BundledNullstellensatz.g17

Open in Workbench Download source

Imports

BundledIdeals · Nullstellensatz · Ring.GeneratedIdeal

Declarations

Source

1-- The weak Nullstellensatz for bundled polynomial rings: over an2-- algebraically closed field, finitely many variables, and a set G of3-- polynomials, one lies in the ideal generated by G exactly when G has no4-- common zero; the predicate AlgebraicallyClosed(R) over a bundled field5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Algebra.Polynomial.BundledNullstellensatz11import BundledIdeals12import Nullstellensatz13import Ring.GeneratedIdeal1415-- An algebraically closed field as a property of the bundled ring;16-- IsAlgebraicallyClosed(A, add, zero, neg, mul, one) remains the form over17-- separate pieces, bridged by the instance below.18predicate AlgebraicallyClosed (R : Set) :=19  Field(R) ∧20  IsAlgebraicallyClosed(R.carrier, R.add, R.zero, R.neg, R.mul, R.one)2122instance AlgebraicallyClosed.parts (R : Set)23  requires closed : AlgebraicallyClosed(R)24  shows IsAlgebraicallyClosed(R.carrier, R.add, R.zero, R.neg, R.mul, R.one)25proof26  obtain ⟨field, engine⟩ := closed27  exact engine2829instance AlgebraicallyClosed.to_field (R : Set)30  requires closed : AlgebraicallyClosed(R)31  shows Field(R)32proof33  obtain ⟨field, engine⟩ := closed34  exact field3536theorem AlgebraicallyClosed.of_projections (R : Set)37  requires field : Field(R)38  requires closed : IsAlgebraicallyClosed(R.carrier, R.add, R.zero, R.neg,39    R.mul, R.one)40  shows AlgebraicallyClosed(R)41proof42  unfold BundledNullstellensatz.AlgebraicallyClosed43  exact ⟨field, closed⟩4445section Nullstellensatz46variable (R I G : Set)47notation ring K := (R.carrier, R.add, R.zero, R.neg, R.mul, R.one)48notation ring P := K[I]49hypothesis closed : AlgebraicallyClosed(R)50hypothesis finite : Finite(I)51hypothesis generators : G ⊆ polynomialRing(R, I)5253-- The weak Nullstellensatz: one is a combination of G exactly when the54-- polynomials of G have no common zero.55theorem polynomialRing.unit_iff_no_common_zero56  shows Ring.one(polynomialRing(R, I)) ∈57      generatedIdeal(polynomialRing(R, I), G) ↔58    ¬(∃ v, (v : I → R.carrier) ∧59      (∀ p ∈ G, evaluationAt(R, I, v)(p) = R[0]))60proof61  have parts := AlgebraicallyClosed.parts with closed62  rw polynomialRing.carrierOf at generators63  have engine := polynomialIdeal.unit_iff_no_common_zero with parts, finite,64    generators65  have same : (∃ v, (v : I → R.carrier) ∧66      (∀ p ∈ G, evaluationAt(R, I, v)(p) = R[0])) ↔67    (∃ v, PolynomialCommonZero(I, K, G, v))68    constructor69    . intro common70      obtain ⟨v, assignment, vanishes⟩ := common71      refine ⟨v, ?_⟩72      unfold PolynomialCommonZero73      refine ⟨assignment, ?_⟩74      intros p hp75      rw ← evaluationAt.graph76      exact vanishes with p, hp77    . intro common78      obtain ⟨v, assignment, vanishes⟩ := common79      refine ⟨v, assignment, ?_⟩80      intros p hp81      rw evaluationAt.graph82      exact vanishes with p, hp83  rw [generatedIdeal.value, polynomialRing.oneOf, polynomialRing.carrierOf,84    polynomialRing.addOf, polynomialRing.zeroOf, polynomialRing.negOf,85    polynomialRing.mulOf]86  tauto8788end Nullstellensatz89