PolynomialPoints

Point ideals and coordinate equations, using the public polynomial API

Open in Workbench View on GitHub

1-- Point ideals and coordinate equations, using the public polynomial API.2-- Part of the Grace17 examples.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module PolynomialPoints8import Grace.Cumulus.Algebra.Polynomial.PointIdeal910section Coordinates11variable (I A add zero neg mul one v : Set)12hypothesis coefficients : IsCommRing(A, add, zero, neg, mul, one)13hypothesis assignment : v : I → A14notation ring R := (A, add, zero, neg, mul, one)15notation ring P := R[I]1617-- x denotes X_j and c denotes the constant polynomial with coefficient a.18theorem coordinate_equation (j a x c : Set)19  requires hj : j ∈ I20  requires ha : a ∈ R21  requires variable : x = polynomialVariable(I, R, j)22  requires constant : c = polynomialConstant(I, R, a)23  shows P[x - c] ∈ pointIdeal(I, R, v) ↔ v(j) = a24proof25  have characterization := pointIdeal.coordinate_difference at I, A, add, zero, neg, mul, one, v, j, a with *26  unfold polynomialCoordinateDifference at characterization27  rw ← variable at characterization28  rw ← constant at characterization29  exact characterization3031theorem points_determined_by_their_ideals (w : Set)32  requires other : w : I → A33  shows pointIdeal(I, R, v) = pointIdeal(I, R, w) ↔ v = w34proof35  exact pointIdeal.eq_iff at I, A, add, zero, neg, mul, one, v, w with *3637theorem common_zero_is_ideal_containment (G : Set)38  requires generators : G ⊆ P39  shows PolynomialCommonZero(I, A, add, zero, neg, mul, one, G, v) ↔ G ⊆ pointIdeal(I, R, v)40proof41  exact PolynomialCommonZero.iff_subset_pointIdeal at I, A, add, zero, neg, mul, one, v, G with *4243end Coordinates4445section Fields46variable (I A add zero neg mul one v : Set)47hypothesis field : IsField(A, add, zero, neg, mul, one)48hypothesis assignment : v : I → A49notation ring R := (A, add, zero, neg, mul, one)50notation ring P := R[I]5152theorem point_ideal_is_maximal53  shows IsMaximalIdeal(P, pointIdeal(I, R, v))54proof55  exact pointIdeal.maximal at I, A, add, zero, neg, mul, one, v with *5657theorem maximal_ideal_has_at_most_one_zero (M w : Set)58  requires maximal : IsMaximalIdeal(P, M)59  requires other : w : I → A60  requires first : PolynomialCommonZero(I, A, add, zero, neg, mul, one, M, v)61  requires second : PolynomialCommonZero(I, A, add, zero, neg, mul, one, M, w)62  shows v = w63proof64  exact IsMaximalIdeal.common_zero_unique at I, A, add, zero, neg, mul, one, v, M, w with *6566end Fields67