PolynomialOrigin

Coefficient embedding and evaluation at the origin, using generic ring APIs

Open in Workbench View on GitHub

1-- Coefficient embedding and evaluation at the origin, using generic ring APIs.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 PolynomialOrigin8import Grace.Cumulus.Algebra.Polynomial.Origin910section Rings11variable (I A add zero neg mul one : Set)12hypothesis coefficients : IsCommRing(A, add, zero, neg, mul, one)13notation ring R := (A, add, zero, neg, mul, one)14notation ring P := R[I]1516theorem embed_product (a b : Set)17  requires ha : a ∈ A18  requires hb : b ∈ A19  shows polynomialCoefficients(I, A, zero)(R[a * b]) = P[polynomialCoefficients(I, A, zero)(a) * polynomialCoefficients(I, A, zero)(b)]20proof21  have hom := polynomialCoefficients.hom at I, A, add, zero, neg, mul, one with coefficients22  exact IsRingHom.mul with hom, ha, hb2324theorem evaluate_product (p q : Set)25  requires hp : p ∈ P26  requires hq : q ∈ P27  shows polynomialAtOrigin(I, A, zero)(P[p * q]) = R[polynomialAtOrigin(I, A, zero)(p) * polynomialAtOrigin(I, A, zero)(q)]28proof29  have hom := polynomialAtOrigin.hom at I, A, add, zero, neg, mul, one with coefficients30  exact IsRingHom.mul with hom, hp, hq3132theorem evaluate_sum (p q : Set)33  requires hp : p ∈ P34  requires hq : q ∈ P35  shows polynomialAtOrigin(I, A, zero)(P[p + q]) = R[polynomialAtOrigin(I, A, zero)(p) + polynomialAtOrigin(I, A, zero)(q)]36proof37  have hom := polynomialAtOrigin.hom at I, A, add, zero, neg, mul, one with coefficients38  exact IsRingHom.add with hom, hp, hq3940theorem recover_coefficient (a : Set)41  requires ha : a ∈ A42  shows polynomialAtOrigin(I, A, zero)(polynomialCoefficients(I, A, zero)(a)) = a43proof44  have ordinary := IsCommRing.ring with coefficients45  have zeroIn := IsRing.zero_in_carrier with ordinary46  exact polynomialAtOrigin.coefficients at I, A, zero, a with *4748theorem variable_vanishes (j : Set)49  requires hj : j ∈ I50  shows polynomialAtOrigin(I, A, zero)(polynomialVariable(I, A, zero, one, j)) = R[0]51proof52  have ordinary := IsCommRing.ring with coefficients53  have zeroIn := IsRing.zero_in_carrier with ordinary54  have multiplicative := IsRing.multiplicative with ordinary55  have oneIn := IsMonoid.unit_in_carrier with multiplicative56  exact polynomialAtOrigin.variable at I, A, zero, one, j with *5758theorem vanishing_is_closed_under_products (p q : Set)59  requires hp : p ∈ P60  requires hq : q ∈ P61  requires vanishes : polynomialAtOrigin(I, A, zero)(p) = R[0]62  shows polynomialAtOrigin(I, A, zero)(P[p * q]) = R[0]63proof64  have hom := polynomialAtOrigin.hom at I, A, add, zero, neg, mul, one with coefficients65  have product := IsRingHom.mul with hom, hp, hq66  have valueQ := IsRingHom.closed with hom, hq67  rw product68  rw vanishes69  ring7071end Rings72