Grace/Cumulus/Algebra/Polynomial/NullstellensatzReduction.g17

Open in Workbench Download source

Imports

ResidueCriterion · Ring.MaximalIdeal

Declarations

Source

1-- Conditional reduction of the weak Nullstellensatz to residue-field surjectivity.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 Grace.Cumulus.Algebra.Polynomial.NullstellensatzReduction8import ResidueCriterion9import Ring.MaximalIdeal1011-- Residue surjectivity is a hypothesis of this section; Zariski's lemma and12-- algebraic closedness establish it elsewhere.13section ResidueSurjectivity14variable (I A add zero neg mul one : Set)15notation ring R := (A, add, zero, neg, mul, one)16notation ring P := R[I]17hypothesis field : IsField(R)18hypothesis residues : ∀ J, IsMaximalIdeal(P, J) → SurjectiveBetween(polynomialResidueCoefficients(I, R, J), R, (P ⧸ idealRelation(P, J)))1920theorem IsMaximalIdeal.common_zero_of_residue_surjectivity (J : Set)21  requires maximal : IsMaximalIdeal(P, J)22  shows ∃ v, PolynomialCommonZero(I, R, J, v)23proof24  have onto := residues with J, maximal25  exact polynomialResidueCoefficients.common_zero_of_surjective with *2627theorem IsMaximalIdeal.point_of_residue_surjectivity (J : Set)28  requires maximal : IsMaximalIdeal(P, J)29  shows ∃ v, FunctionBetween(v, I, R) ∧ J = pointIdeal(I, R, v)30proof31  obtain ⟨v, common⟩ := IsMaximalIdeal.common_zero_of_residue_surjectivity at I, A, add, zero, neg, mul, one, J with *32  have data := common33  have equal := IsMaximalIdeal.common_zero_iff_point.forward with field, data.left, maximal, common34  refine ⟨v, data.left, equal⟩3536theorem polynomialIdeal.common_zero_of_residue_surjectivity (G : Set)37  requires generators : G ⊆ P38  requires proper : ¬(P[1] ∈ idealSpan(P, G))39  shows ∃ v, PolynomialCommonZero(I, R, G, v)40proof41  have ring := IsField.comm_ring with field42  have source := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *43  obtain ⟨J, maximal, contains⟩ := idealSpan.exists_maximal with source, generators, proper44  obtain ⟨v, common⟩ := IsMaximalIdeal.common_zero_of_residue_surjectivity at I, A, add, zero, neg, mul, one, J with *45  witness v46  constructor47  . exact common.left48  . intros p hp49    have member := contains with p, hp50    exact common.right with p, member5152theorem polynomialIdeal.unit_iff_no_common_zero_of_residue_surjectivity (G : Set)53  requires generators : G ⊆ P54  shows P[1] ∈ idealSpan(P, G) ↔ ¬(∃ v, PolynomialCommonZero(I, R, G, v))55proof56  constructor57  . intro certificate58    have ring := IsField.comm_ring with field59    have nontrivial := IsField.nontrivial with field60    exact polynomialIdeal.no_common_zero with *61  . intro absent62    by_contra proper63    have common := polynomialIdeal.common_zero_of_residue_surjectivity with *64    exact absent with common6566end ResidueSurjectivity6768-- An explicit sufficient hypothesis for the outstanding residue-surjectivity step.69-- It remains a hypothesis: no theorem here claims it for algebraically closed fields.70section FieldAlgebraRigidity71variable (I A add zero neg mul one : Set)72notation ring R := (A, add, zero, neg, mul, one)73notation ring P := R[I]74hypothesis field : IsField(R)75hypothesis finite : Finite(I)76hypothesis rigidity : ∀ B, ∀ plus, ∀ z, ∀ minus, ∀ times, ∀ unit, ∀ f, IsField(B, plus, z, minus, times, unit) → IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit) → FinitelyGeneratedAlgebra(f, A, B, plus, z, minus, times, unit) → SurjectiveBetween(f, A, B)7778theorem polynomialResidueCoefficients.surjective_of_field_algebra_rigidity (J : Set)79  requires maximal : IsMaximalIdeal(P, J)80  shows SurjectiveBetween(polynomialResidueCoefficients(I, R, J), R, (P ⧸ idealRelation(P, J)))81proof82  have ring := IsField.comm_ring with field83  have source := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *84  have ideal := IsMaximalIdeal.ideal with maximal85  have quotientField := idealQuotient.is_field_of_maximal with source, maximal86  have hom := polynomialResidueCoefficients.hom with *87  have generated := polynomialResidueCoefficients.finitely_generated with *88  exact rigidity with (P ⧸ idealRelation(P, J)), quotientBinary(P, idealRelation(P, J), polynomialAdd(I, A, add, zero, neg, mul, one)), ⟦P[0]⟧[P, idealRelation(P, J)], quotientUnary(P, idealRelation(P, J), polynomialNeg(I, A, add, zero, neg, mul, one)), quotientBinary(P, idealRelation(P, J), polynomialMul(I, A, add, zero, neg, mul, one)), ⟦P[1]⟧[P, idealRelation(P, J)], polynomialResidueCoefficients(I, R, J), quotientField, hom, generated8990theorem polynomialIdeal.unit_iff_no_common_zero_of_field_algebra_rigidity (G : Set)91  requires generators : G ⊆ P92  shows P[1] ∈ idealSpan(P, G) ↔ ¬(∃ v, PolynomialCommonZero(I, R, G, v))93proof94  have residues : ∀ J, IsMaximalIdeal(P, J) → SurjectiveBetween(polynomialResidueCoefficients(I, R, J), R, (P ⧸ idealRelation(P, J)))95    intros J maximal96    exact polynomialResidueCoefficients.surjective_of_field_algebra_rigidity with *97  exact polynomialIdeal.unit_iff_no_common_zero_of_residue_surjectivity with field, residues, generators9899end FieldAlgebraRigidity100