-- A maximal polynomial ideal has a common zero exactly when its coefficient map is onto.
-- 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.ResidueCriterion
import Residue
import PointIdeal

section Residues
variable (I A add zero neg mul one J : Set)
notation ring R := (A, add, zero, neg, mul, one)
notation ring P := R[I]
notation ring Q := P ⧸ J
hypothesis field : IsField(R)
hypothesis maximal : IsMaximalIdeal(P, J)

theorem polynomialResidueCoefficients.surjective_of_common_zero (v : Set)
  requires common : PolynomialCommonZero(I, R, J, v)
  shows SurjectiveBetween(polynomialResidueCoefficients(I, R, J), R, Q)
proof
  have ring := IsField.comm_ring with field
  have polynomialRing := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have ideal := IsMaximalIdeal.ideal with maximal
  have equivalence := idealRelation.equivalence with polynomialRing, ideal
  have data := common
  have assignment := data.left
  have evaluation := polynomialAt.hom with *
  have equalIdeal := IsMaximalIdeal.common_zero_iff_point.forward with *
  have hom := polynomialResidueCoefficients.hom with *
  have function := IsRingHom.function with hom
  constructor
  . exact function
  . intros X hX
    obtain ⟨p, hp, shape⟩ := quotient.representative with hX
    have value := IsRingHom.closed with evaluation, hp
    have constant := polynomialConstant.member at I, A, zero, polynomialAt(I, R, v)(p) with *
    have constantValue := polynomialAt.constant at I, A, add, zero, neg, mul, one, v, polynomialAt(I, R, v)(p) with *
    have congruent := IsRingHom.kernel_congruent.backward with polynomialRing, ring, evaluation, constant, hp, constantValue
    unfold pointIdeal at equalIdeal
    rw ← equalIdeal at congruent
    have equalClass := idealClass.eq_iff_congruent.backward with *
    have residueValue := polynomialResidueCoefficients.value at I, A, add, zero, neg, mul, one, J, polynomialAt(I, R, v)(p) with *
    have projectionValue := quotientProjection.value at P, idealRelation(P, J), polynomialConstant(I, R, polynomialAt(I, R, v)(p)) with *
    have output : polynomialResidueCoefficients(I, R, J)(polynomialAt(I, R, v)(p)) = X by cc
    have edge := FunctionBetween.relates_apply with function, value
    witness polynomialAt(I, R, v)(p)
    constructor
    . exact value
    . rw output at edge
      exact edge

theorem polynomialResidueCoefficients.surjective_iff_common_zero
  shows SurjectiveBetween(polynomialResidueCoefficients(I, R, J), R, Q) ↔ ∃ v, PolynomialCommonZero(I, R, J, v)
proof
  constructor
  . intro onto
    exact polynomialResidueCoefficients.common_zero_of_surjective with *
  . intro exists
    obtain ⟨v, common⟩ := exists
    exact polynomialResidueCoefficients.surjective_of_common_zero with *

end Residues