-- Conditional reduction of the weak Nullstellensatz to residue-field surjectivity.
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Algebra.Polynomial.NullstellensatzReduction
import ResidueCriterion
import Ring.MaximalIdeal

-- Residue surjectivity is a hypothesis of this section; Zariski's lemma and
-- algebraic closedness establish it elsewhere.
section ResidueSurjectivity
variable (I A add zero neg mul one : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring P := R[I]
hypothesis field : IsField(R)
hypothesis residues : ∀ J, IsMaximalIdeal(P, J) → SurjectiveBetween(polynomialResidueCoefficients(I, R, J), R, (P ⧸ idealRelation(P, J)))

theorem IsMaximalIdeal.common_zero_of_residue_surjectivity (J : Set)
  requires maximal : IsMaximalIdeal(P, J)
  shows ∃ v, PolynomialCommonZero(I, R, J, v)
proof
  have onto := residues with J, maximal
  exact polynomialResidueCoefficients.common_zero_of_surjective with *

theorem IsMaximalIdeal.point_of_residue_surjectivity (J : Set)
  requires maximal : IsMaximalIdeal(P, J)
  shows ∃ v, FunctionBetween(v, I, R) ∧ J = pointIdeal(I, R, v)
proof
  obtain ⟨v, common⟩ := IsMaximalIdeal.common_zero_of_residue_surjectivity at I, A, add, zero, neg, mul, one, J with *
  have data := common
  have equal := IsMaximalIdeal.common_zero_iff_point.forward with field, data.left, maximal, common
  refine ⟨v, data.left, equal⟩

theorem polynomialIdeal.common_zero_of_residue_surjectivity (G : Set)
  requires generators : G ⊆ P
  requires proper : ¬(P[1] ∈ idealSpan(P, G))
  shows ∃ v, PolynomialCommonZero(I, R, G, v)
proof
  have ring := IsField.comm_ring with field
  have source := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *
  obtain ⟨J, maximal, contains⟩ := idealSpan.exists_maximal with source, generators, proper
  obtain ⟨v, common⟩ := IsMaximalIdeal.common_zero_of_residue_surjectivity at I, A, add, zero, neg, mul, one, J with *
  witness v
  constructor
  . exact common.left
  . intros p hp
    have member := contains with p, hp
    exact common.right with p, member

theorem polynomialIdeal.unit_iff_no_common_zero_of_residue_surjectivity (G : Set)
  requires generators : G ⊆ P
  shows P[1] ∈ idealSpan(P, G) ↔ ¬(∃ v, PolynomialCommonZero(I, R, G, v))
proof
  constructor
  . intro certificate
    have ring := IsField.comm_ring with field
    have nontrivial := IsField.nontrivial with field
    exact polynomialIdeal.no_common_zero with *
  . intro absent
    by_contra proper
    have common := polynomialIdeal.common_zero_of_residue_surjectivity with *
    exact absent with common

end ResidueSurjectivity

-- An explicit sufficient hypothesis for the outstanding residue-surjectivity step.
-- It remains a hypothesis: no theorem here claims it for algebraically closed fields.
section FieldAlgebraRigidity
variable (I A add zero neg mul one : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring P := R[I]
hypothesis field : IsField(R)
hypothesis finite : Finite(I)
hypothesis 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)

theorem polynomialResidueCoefficients.surjective_of_field_algebra_rigidity (J : Set)
  requires maximal : IsMaximalIdeal(P, J)
  shows SurjectiveBetween(polynomialResidueCoefficients(I, R, J), R, (P ⧸ idealRelation(P, J)))
proof
  have ring := IsField.comm_ring with field
  have source := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *
  have ideal := IsMaximalIdeal.ideal with maximal
  have quotientField := idealQuotient.is_field_of_maximal with source, maximal
  have hom := polynomialResidueCoefficients.hom with *
  have generated := polynomialResidueCoefficients.finitely_generated with *
  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, generated

theorem polynomialIdeal.unit_iff_no_common_zero_of_field_algebra_rigidity (G : Set)
  requires generators : G ⊆ P
  shows P[1] ∈ idealSpan(P, G) ↔ ¬(∃ v, PolynomialCommonZero(I, R, G, v))
proof
  have residues : ∀ J, IsMaximalIdeal(P, J) → SurjectiveBetween(polynomialResidueCoefficients(I, R, J), R, (P ⧸ idealRelation(P, J)))
    intros J maximal
    exact polynomialResidueCoefficients.surjective_of_field_algebra_rigidity with *
  exact polynomialIdeal.unit_iff_no_common_zero_of_residue_surjectivity with field, residues, generators

end FieldAlgebraRigidity