Grace/Cumulus/Algebra/Polynomial/BundledIdeals.g17

Open in Workbench Download source

Imports

BundledEvaluation · PointIdeal

Declarations

Source

1-- Point ideals of bundled polynomial rings: pointIdeal(R, I, v), the2-- polynomials vanishing at v, as an ideal of polynomialRing(R, I), the3-- kernel of evaluationAt(R, I, v), its maximality over a field, and the4-- maximal ideals with a common zero; everything here is ZF5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Algebra.Polynomial.BundledIdeals11import BundledEvaluation12import PointIdeal1314-- The polynomials over R vanishing at the point v : I → R.15def pointIdeal (R I v : Set) : Set :=16  pointIdeal(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, v)1718theorem pointIdeal.engine (R I v : Set)19  shows pointIdeal(R, I, v) =20    pointIdeal(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, v)21proof22  simp [BundledIdeals.pointIdeal]2324section Points25variable (R I v : Set)26notation ring K := (R.carrier, R.add, R.zero, R.neg, R.mul, R.one)27notation ring P := K[I]28hypothesis comm : CommRing(R)29hypothesis assignment : v : I → R.carrier3031theorem pointIdeal.mem_iff (p : Set)32  shows p ∈ pointIdeal(R, I, v) ↔33    p ∈ polynomialRing(R, I) ∧ evaluationAt(R, I, v)(p) = R[0]34proof35  have parts := CommRing.parts with comm36  have engine := pointIdeal.membership at I, R.carrier, R.add, R.zero, R.neg,37    R.mul, R.one, v, p with parts, assignment38  rw [pointIdeal.engine, polynomialRing.carrierOf, evaluationAt.graph]39  exact engine4041theorem pointIdeal.kernel42  shows pointIdeal(R, I, v) = ringKernel(evaluationAt(R, I, v),43    polynomialRing(R, I), R[0])44proof45  rw [pointIdeal.engine, polynomialRing.carrierOf, evaluationAt.graph]46  simp [PointIdeal.pointIdeal]4748theorem Ideal.point49  shows Ideal(polynomialRing(R, I), pointIdeal(R, I, v))50proof51  have parts := CommRing.parts with comm52  have engine := pointIdeal.ideal with parts, assignment53  rw pointIdeal.engine54  exact Ideal.polynomial_of_parts with comm, engine5556-- Distinct points have distinct ideals, and one contains the other only57-- when the points agree.58theorem pointIdeal.subset_iff_eq (w : Set)59  requires other : w : I → R.carrier60  shows pointIdeal(R, I, v) ⊆ pointIdeal(R, I, w) ↔ v = w61proof62  have parts := CommRing.parts with comm63  have engine := pointIdeal.subset_iff with parts, assignment, other64  rw [pointIdeal.engine, pointIdeal.engine]65  exact engine6667theorem pointIdeal.injective (w : Set)68  requires other : w : I → R.carrier69  shows pointIdeal(R, I, v) = pointIdeal(R, I, w) ↔ v = w70proof71  have parts := CommRing.parts with comm72  have engine := pointIdeal.eq_iff with parts, assignment, other73  rw [pointIdeal.engine, pointIdeal.engine]74  exact engine7576end Points7778section Fields79variable (R I v : Set)80notation ring K := (R.carrier, R.add, R.zero, R.neg, R.mul, R.one)81notation ring P := K[I]82hypothesis field : Field(R)83hypothesis assignment : v : I → R.carrier8485-- Over a field the point ideals are maximal.86theorem MaximalIdeal.point87  shows MaximalIdeal(polynomialRing(R, I), pointIdeal(R, I, v))88proof89  have comm := Field.to_comm_ring with field90  have isField := Field.parts with field91  have engine := pointIdeal.maximal with isField, assignment92  rw pointIdeal.engine93  exact MaximalIdeal.polynomial_of_parts with comm, engine9495-- A maximal ideal vanishes at v exactly when it is the point ideal of v.96theorem MaximalIdeal.vanishes_iff_point (M : Set)97  requires maximal : MaximalIdeal(polynomialRing(R, I), M)98  shows (∀ p ∈ M, evaluationAt(R, I, v)(p) = R[0]) ↔99    M = pointIdeal(R, I, v)100proof101  have comm := Field.to_comm_ring with field102  have isField := Field.parts with field103  have engine := MaximalIdeal.polynomial_parts with comm, maximal104  have criterion := IsMaximalIdeal.common_zero_iff_point with isField,105    assignment, engine106  rw pointIdeal.engine107  constructor108  . intro vanishes109    have common : PolynomialCommonZero(I, K, M, v)110      unfold PolynomialCommonZero111      refine ⟨assignment, ?_⟩112      intros p hp113      rw ← evaluationAt.graph114      exact vanishes with p, hp115    exact criterion.forward with common116  . intro equal117    have common := criterion.backward with equal118    unfold PolynomialCommonZero at common119    intros p hp120    rw evaluationAt.graph121    exact common.right with p, hp122123end Fields124