-- Point ideals of bundled polynomial rings: pointIdeal(R, I, v), the
-- polynomials vanishing at v, as an ideal of polynomialRing(R, I), the
-- kernel of evaluationAt(R, I, v), its maximality over a field, and the
-- maximal ideals with a common zero; everything here is 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.BundledIdeals
import BundledEvaluation
import PointIdeal

-- The polynomials over R vanishing at the point v : I → R.
def pointIdeal (R I v : Set) : Set :=
  pointIdeal(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, v)

theorem pointIdeal.engine (R I v : Set)
  shows pointIdeal(R, I, v) =
    pointIdeal(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, v)
proof
  simp [BundledIdeals.pointIdeal]

section Points
variable (R I v : Set)
notation ring K := (R.carrier, R.add, R.zero, R.neg, R.mul, R.one)
notation ring P := K[I]
hypothesis comm : CommRing(R)
hypothesis assignment : v : I → R.carrier

theorem pointIdeal.mem_iff (p : Set)
  shows p ∈ pointIdeal(R, I, v) ↔
    p ∈ polynomialRing(R, I) ∧ evaluationAt(R, I, v)(p) = R[0]
proof
  have parts := CommRing.parts with comm
  have engine := pointIdeal.membership at I, R.carrier, R.add, R.zero, R.neg,
    R.mul, R.one, v, p with parts, assignment
  rw [pointIdeal.engine, polynomialRing.carrierOf, evaluationAt.graph]
  exact engine

theorem pointIdeal.kernel
  shows pointIdeal(R, I, v) = ringKernel(evaluationAt(R, I, v),
    polynomialRing(R, I), R[0])
proof
  rw [pointIdeal.engine, polynomialRing.carrierOf, evaluationAt.graph]
  simp [PointIdeal.pointIdeal]

theorem Ideal.point
  shows Ideal(polynomialRing(R, I), pointIdeal(R, I, v))
proof
  have parts := CommRing.parts with comm
  have engine := pointIdeal.ideal with parts, assignment
  rw pointIdeal.engine
  exact Ideal.polynomial_of_parts with comm, engine

-- Distinct points have distinct ideals, and one contains the other only
-- when the points agree.
theorem pointIdeal.subset_iff_eq (w : Set)
  requires other : w : I → R.carrier
  shows pointIdeal(R, I, v) ⊆ pointIdeal(R, I, w) ↔ v = w
proof
  have parts := CommRing.parts with comm
  have engine := pointIdeal.subset_iff with parts, assignment, other
  rw [pointIdeal.engine, pointIdeal.engine]
  exact engine

theorem pointIdeal.injective (w : Set)
  requires other : w : I → R.carrier
  shows pointIdeal(R, I, v) = pointIdeal(R, I, w) ↔ v = w
proof
  have parts := CommRing.parts with comm
  have engine := pointIdeal.eq_iff with parts, assignment, other
  rw [pointIdeal.engine, pointIdeal.engine]
  exact engine

end Points

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

-- Over a field the point ideals are maximal.
theorem MaximalIdeal.point
  shows MaximalIdeal(polynomialRing(R, I), pointIdeal(R, I, v))
proof
  have comm := Field.to_comm_ring with field
  have isField := Field.parts with field
  have engine := pointIdeal.maximal with isField, assignment
  rw pointIdeal.engine
  exact MaximalIdeal.polynomial_of_parts with comm, engine

-- A maximal ideal vanishes at v exactly when it is the point ideal of v.
theorem MaximalIdeal.vanishes_iff_point (M : Set)
  requires maximal : MaximalIdeal(polynomialRing(R, I), M)
  shows (∀ p ∈ M, evaluationAt(R, I, v)(p) = R[0]) ↔
    M = pointIdeal(R, I, v)
proof
  have comm := Field.to_comm_ring with field
  have isField := Field.parts with field
  have engine := MaximalIdeal.polynomial_parts with comm, maximal
  have criterion := IsMaximalIdeal.common_zero_iff_point with isField,
    assignment, engine
  rw pointIdeal.engine
  constructor
  . intro vanishes
    have common : PolynomialCommonZero(I, K, M, v)
      unfold PolynomialCommonZero
      refine ⟨assignment, ?_⟩
      intros p hp
      rw ← evaluationAt.graph
      exact vanishes with p, hp
    exact criterion.forward with common
  . intro equal
    have common := criterion.backward with equal
    unfold PolynomialCommonZero at common
    intros p hp
    rw evaluationAt.graph
    exact common.right with p, hp

end Fields