-- Point ideals, coordinate separation, and residue rings (ZF).
-- 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.PointIdeal
import Assignment
import Field.Homomorphism

def pointIdeal (I A add zero neg mul one v : Set) : Set :=
  ringKernel(polynomialAt(I, A, add, zero, neg, mul, one, v), polynomials(I, A, zero), zero)

notation scoped pointIdeal(I, R, v) => pointIdeal(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, v)

def polynomialCoordinateDifference (I A add zero neg mul one j a : Set) : Set :=
  (polynomialAdd(I, A, add, zero, neg, mul, one))(polynomialVariable(I, A, zero, one, j), (polynomialNeg(I, A, add, zero, neg, mul, one))(polynomialConstant(I, A, zero, a)))

notation scoped polynomialCoordinateDifference(I, R, j, a) => polynomialCoordinateDifference(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, j, a)

section Coordinates
variable (I A add zero neg mul one : Set)
hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)
notation ring R := (A, add, zero, neg, mul, one)
notation ring P := R[I]

theorem polynomialCoordinateDifference.member (j a : Set)
  requires coefficient : a ∈ R
  shows polynomialCoordinateDifference(I, A, add, zero, neg, mul, one, j, a) ∈ P
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have multiplicative := IsRing.multiplicative with ordinary
  have oneIn := IsMonoid.unit_in_carrier with multiplicative
  have variable := polynomialVariable.member at I, A, zero, one, j with *
  have constant := polynomialConstant.member at I, A, zero, a with *
  have source := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *
  have polynomialRing := IsCommRing.ring with source
  have negative := IsRing.neg_closed with polynomialRing, constant
  unfold polynomialCoordinateDifference
  exact IsRing.add_closed with polynomialRing, variable, negative

theorem polynomialAt.coordinate_difference (v j a : Set)
  requires assignment : v : I → A
  requires index : j ∈ I
  requires coefficient : a ∈ R
  shows polynomialAt(I, A, add, zero, neg, mul, one, v)(polynomialCoordinateDifference(I, A, add, zero, neg, mul, one, j, a)) = R[v(j) - a]
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have multiplicative := IsRing.multiplicative with ordinary
  have oneIn := IsMonoid.unit_in_carrier with multiplicative
  have variable := polynomialVariable.member at I, A, zero, one, j with *
  have constant := polynomialConstant.member at I, A, zero, a with *
  have hom := polynomialAt.hom with *
  have source := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *
  have subtraction := IsRingHom.sub with source, hom, variable, constant
  have valueVariable := polynomialAt.variable with *
  have valueConstant := polynomialAt.constant at I, A, add, zero, neg, mul, one, v, a with *
  unfold polynomialCoordinateDifference
  cc

-- Evaluate at the constant point a + 1 to distinguish X_j - a from zero.
theorem polynomialCoordinateDifference.nonzero (j a : Set)
  requires distinct : R[0] ≠ R[1]
  requires index : j ∈ I
  requires coefficient : a ∈ R
  shows polynomialCoordinateDifference(I, A, add, zero, neg, mul, one, j, a) ≠ P[0]
proof
  have ordinary := IsCommRing.ring with ring
  have monoid := IsRing.multiplicative with ordinary
  have oneIn := IsMonoid.unit_in_carrier with monoid
  have shifted := IsRing.add_closed with ordinary, coefficient, oneIn
  have assignment := constantFunction.function at I, A, R[a + 1] with shifted
  have value := constantFunction.apply with index, shifted
  have evaluated := polynomialAt.coordinate_difference with assignment, index, coefficient
  have hom := polynomialAt.hom with *
  have zeroValue := IsRingHom.zero with hom
  have difference : R[(a + 1) - a] = R[1] by ring
  intro equal
  have impossible : R[0] = R[1] by cc
  exact distinct with impossible

end Coordinates

section Points
variable (I A add zero neg mul one v : Set)
hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)
hypothesis assignment : v : I → A
notation ring R := (A, add, zero, neg, mul, one)
notation ring P := R[I]

theorem pointIdeal.membership (p : Set)
  shows p ∈ pointIdeal(I, A, add, zero, neg, mul, one, v) ↔ p ∈ P ∧ polynomialAt(I, A, add, zero, neg, mul, one, v)(p) = R[0]
proof
  simp [pointIdeal, ringKernel.membership]

theorem pointIdeal.ideal
  shows IsIdeal(P, polynomialAdd(I, A, add, zero, neg, mul, one), P[0], polynomialNeg(I, A, add, zero, neg, mul, one), polynomialMul(I, A, add, zero, neg, mul, one), pointIdeal(I, A, add, zero, neg, mul, one, v))
proof
  unfold pointIdeal
  exact polynomialAt.kernel_ideal with *

theorem pointIdeal.coordinate_difference (j a : Set)
  requires index : j ∈ I
  requires coefficient : a ∈ R
  shows polynomialCoordinateDifference(I, A, add, zero, neg, mul, one, j, a) ∈ pointIdeal(I, A, add, zero, neg, mul, one, v) ↔ v(j) = a
proof
  have member := polynomialCoordinateDifference.member at I, A, add, zero, neg, mul, one, j, a with *
  have image := FunctionBetween.apply_closed with *
  have value := polynomialAt.coordinate_difference at I, A, add, zero, neg, mul, one, v, j, a with *
  constructor
  . intro vanishes
    have data := pointIdeal.membership.forward with *
    have equation : R[v(j) - a] = R[0] by cc
    linear_combination equation
  . intro equal
    have equation : R[v(j) - a] = R[0]
      rw equal
      ring
    apply pointIdeal.membership.backward with ring, assignment
    refine ⟨member, ?_⟩
    cc

theorem pointIdeal.contains_centered_variable (j : Set)
  requires index : j ∈ I
  shows polynomialCoordinateDifference(I, A, add, zero, neg, mul, one, j, v(j)) ∈ pointIdeal(I, A, add, zero, neg, mul, one, v)
proof
  have coefficient := FunctionBetween.apply_closed with *
  apply pointIdeal.coordinate_difference.backward with ring, assignment, index, coefficient
  rfl

theorem pointIdeal.subset_iff (w : Set)
  requires other : w : I → A
  shows pointIdeal(I, A, add, zero, neg, mul, one, v) ⊆ pointIdeal(I, A, add, zero, neg, mul, one, w) ↔ v = w
proof
  constructor
  . intro included
    apply FunctionBetween.ext with assignment, other
    intros j hj
    have coefficient := FunctionBetween.apply_closed at v, I, A, j with *
    have centered := pointIdeal.contains_centered_variable at I, A, add, zero, neg, mul, one, v, j with *
    have member := included with polynomialCoordinateDifference(I, A, add, zero, neg, mul, one, j, v(j)), centered
    have equal := pointIdeal.coordinate_difference.forward with ring, other, hj, coefficient, member
    symm
    exact equal
  . intro equal
    rw equal
    simp

theorem pointIdeal.eq_iff (w : Set)
  requires other : w : I → A
  shows pointIdeal(I, A, add, zero, neg, mul, one, v) = pointIdeal(I, A, add, zero, neg, mul, one, w) ↔ v = w
proof
  constructor
  . intro equal
    have included : pointIdeal(I, A, add, zero, neg, mul, one, v) ⊆ pointIdeal(I, A, add, zero, neg, mul, one, w)
      rw equal
      simp
    exact pointIdeal.subset_iff.forward with *
  . intro equal
    rw equal
    rfl

theorem PolynomialCommonZero.iff_subset_pointIdeal (G : Set)
  requires generators : G ⊆ P
  shows PolynomialCommonZero(I, R, G, v) ↔ G ⊆ pointIdeal(I, A, add, zero, neg, mul, one, v)
proof
  constructor
  . intros common p hp
    have member := generators with p, hp
    have value := common.right with p, hp
    apply pointIdeal.membership.backward with ring, assignment
    refine ⟨member, value⟩
  . intro included
    unfold PolynomialCommonZero
    refine ⟨assignment, ?_⟩
    intros p hp
    have member := included with p, hp
    have data := pointIdeal.membership.forward with *
    exact data.right

theorem pointIdeal.quotient_iso
  shows IsRingIso(quotientMap(polynomialAt(I, A, add, zero, neg, mul, one, v), polynomials(I, A, zero), A, idealRelation(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), polynomialNeg(I, A, add, zero, neg, mul, one), pointIdeal(I, A, add, zero, neg, mul, one, v))),
    (polynomials(I, A, zero) ⧸ idealRelation(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), polynomialNeg(I, A, add, zero, neg, mul, one), pointIdeal(I, A, add, zero, neg, mul, one, v))),
    quotientBinary(polynomials(I, A, zero), idealRelation(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), polynomialNeg(I, A, add, zero, neg, mul, one), pointIdeal(I, A, add, zero, neg, mul, one, v)), polynomialAdd(I, A, add, zero, neg, mul, one)), ⟦constantFunction(monomials(I), A, zero)⟧[polynomials(I, A, zero), idealRelation(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), polynomialNeg(I, A, add, zero, neg, mul, one), pointIdeal(I, A, add, zero, neg, mul, one, v))],
    quotientUnary(polynomials(I, A, zero), idealRelation(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), polynomialNeg(I, A, add, zero, neg, mul, one), pointIdeal(I, A, add, zero, neg, mul, one, v)), polynomialNeg(I, A, add, zero, neg, mul, one)), quotientBinary(polynomials(I, A, zero), idealRelation(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), polynomialNeg(I, A, add, zero, neg, mul, one), pointIdeal(I, A, add, zero, neg, mul, one, v)), polynomialMul(I, A, add, zero, neg, mul, one)), ⟦polynomialConstant(I, A, zero, one)⟧[polynomials(I, A, zero), idealRelation(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), polynomialNeg(I, A, add, zero, neg, mul, one), pointIdeal(I, A, add, zero, neg, mul, one, v))],
    A, add, zero, neg, mul, one)
proof
  have source := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *
  have hom := polynomialAt.hom with *
  have onto := polynomialAt.surjective with *
  have iso := idealQuotient.first_isomorphism with source, ring, hom, onto
  simpa [pointIdeal] using iso

end Points

section Fields
variable (I A add zero neg mul one v : Set)
hypothesis field : IsField(A, add, zero, neg, mul, one)
hypothesis assignment : v : I → A
notation ring R := (A, add, zero, neg, mul, one)
notation ring P := R[I]

theorem pointIdeal.maximal
  shows IsMaximalIdeal(P, polynomialAdd(I, A, add, zero, neg, mul, one), P[0], polynomialNeg(I, A, add, zero, neg, mul, one), polynomialMul(I, A, add, zero, neg, mul, one), P[1], pointIdeal(I, A, add, zero, neg, mul, one, v))
proof
  have ring := IsField.comm_ring with field
  have source := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *
  have hom := polynomialAt.hom with *
  have onto := polynomialAt.surjective with *
  unfold pointIdeal
  exact IsRingHom.kernel_maximal with source, field, hom, onto

theorem IsMaximalIdeal.common_zero_iff_point (M : Set)
  requires maximal : IsMaximalIdeal(P, polynomialAdd(I, A, add, zero, neg, mul, one), P[0], polynomialNeg(I, A, add, zero, neg, mul, one), polynomialMul(I, A, add, zero, neg, mul, one), P[1], M)
  shows PolynomialCommonZero(I, R, M, v) ↔ M = pointIdeal(I, A, add, zero, neg, mul, one, v)
proof
  have ring := IsField.comm_ring with field
  have ideal := IsMaximalIdeal.ideal with maximal
  have bounded := IsIdeal.subset_carrier with ideal
  have pointMaximal := pointIdeal.maximal with *
  have pointProper := IsMaximalIdeal.proper with pointMaximal
  constructor
  . intro common
    have included := PolynomialCommonZero.iff_subset_pointIdeal.forward with ring, assignment, bounded, common
    have data := maximal
    have equal := data.right with pointIdeal(I, A, add, zero, neg, mul, one, v), pointProper, included
    symm
    exact equal
  . intro equal
    have included : M ⊆ pointIdeal(I, A, add, zero, neg, mul, one, v)
      rw equal
      simp
    exact PolynomialCommonZero.iff_subset_pointIdeal.backward with *

theorem IsMaximalIdeal.common_zero_unique (M w : Set)
  requires maximal : IsMaximalIdeal(P, polynomialAdd(I, A, add, zero, neg, mul, one), P[0], polynomialNeg(I, A, add, zero, neg, mul, one), polynomialMul(I, A, add, zero, neg, mul, one), P[1], M)
  requires other : w : I → A
  requires first : PolynomialCommonZero(I, R, M, v)
  requires second : PolynomialCommonZero(I, R, M, w)
  shows v = w
proof
  have ring := IsField.comm_ring with field
  have left := IsMaximalIdeal.common_zero_iff_point.forward with field, assignment, maximal, first
  have right := IsMaximalIdeal.common_zero_iff_point.forward with field, other, maximal, second
  have equal : pointIdeal(I, A, add, zero, neg, mul, one, v) = pointIdeal(I, A, add, zero, neg, mul, one, w) by cc
  exact pointIdeal.eq_iff.forward with *

end Fields