Grace/Cumulus/Algebra/Polynomial/Assignment.g17

Open in Workbench Download source

Imports

EvaluationHom · Ring.FiniteProduct · Group.Power

Declarations

Source

1-- Evaluation of monomials at arbitrary variable assignments (ZF).2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.Polynomial.Assignment8import EvaluationHom9import Ring.FiniteProduct10import Group.Power1112defgraph monomialWeights (I D A add zero neg mul one v m : Set) (i ∈ D) : A := monoidPow(mul, one, v(i), m(i))13requires ring : IsCommRing(A, add, zero, neg, mul, one)14requires assignment : v : I → A15requires monomial : m ∈ monomials(I)16requires domain : D ⊆ I17proof18  unfold Subset at domain19  have index := domain with i, member20  have exponent := monomials.exponent at I, m, i with *21  have value := FunctionBetween.apply_closed at v, I, A, i with *22  have ordinary := IsCommRing.ring with ring23  have multiplicative := IsRing.multiplicative with ordinary24  exact monoidPow.closed at A, mul, one, v(i), m(i) with *2526defgraph monomialEvaluate (I A add zero neg mul one v : Set) (m ∈ monomials(I)) : A :=27  finiteRingProduct(functionSupport(m, I, 0), A, add, zero, neg, mul, one, monomialWeights(I, functionSupport(m, I, 0), A, add, zero, neg, mul, one, v, m))28requires ring : IsCommRing(A, add, zero, neg, mul, one)29requires assignment : v : I → A30proof31  have domain := functionSupport.subset at m, I, 032  have map := monomials.map with member33  have finite := CoefficientMap.finite_support with map34  have weights := monomialWeights.function at I, functionSupport(m, I, 0), A, add, zero, neg, mul, one, v, m with *35  exact finiteRingProduct.closed at functionSupport(m, I, 0), A, add, zero, neg, mul, one, monomialWeights(I, functionSupport(m, I, 0), A, add, zero, neg, mul, one, v, m) with *3637-- The evaluation graph associated with an assignment of values to variables.38def polynomialAt (I A add zero neg mul one v : Set) : Set :=39  polynomialEvaluate(I, A, add, zero, neg, mul, one, monomialEvaluate(I, A, add, zero, neg, mul, one, v))4041notation scoped polynomialAt(I, R, v) => polynomialAt(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, v)4243section Evaluation44variable (I A add zero neg mul one v : Set)45hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)46hypothesis assignment : v : I → A4748theorem monomialEvaluate.on_domain (m D : Set)49  requires monomial : m ∈ monomials(I)50  requires domain : D ⊆ I51  requires finite : Finite(D)52  requires covers : functionSupport(m, I, 0) ⊆ D53  shows monomialEvaluate(I, A, add, zero, neg, mul, one, v)(m) = finiteRingProduct(D, A, add, zero, neg, mul, one,  monomialWeights(I, D, A, add, zero, neg, mul, one, v,  m))54proof55  have supportDomain := functionSupport.subset at m, I, 056  have weights := monomialWeights.function at I, D, A, add, zero, neg, mul, one, v, m with *57  have supported := monomialWeights.function at I, functionSupport(m, I, 0), A, add, zero, neg, mul, one, v, m with *58  have agreement : ∀ i ∈ functionSupport(m, I, 0), monomialWeights(I, D, A, add, zero, neg, mul, one, v,  m)(i) = monomialWeights(I, functionSupport(m, I, 0), A, add, zero, neg, mul, one, v,  m)(i)59    intros i hi60    have included := covers61    have inD := included with i, hi62    have left := monomialWeights.value at I, D, A, add, zero, neg, mul, one, v, m, i with *63    have right := monomialWeights.value at I, functionSupport(m, I, 0), A, add, zero, neg, mul, one, v, m, i with *64    cc65  have neutral : ∀ i ∈ D, ¬(i ∈ functionSupport(m, I, 0)) → monomialWeights(I, D, A, add, zero, neg, mul, one, v,  m)(i) = one66    intros i hi outside67    have included := domain68    have index := included with i, hi69    have exponent := functionSupport.outside with *70    have weight := monomialWeights.value at I, D, A, add, zero, neg, mul, one, v, m, i with *71    rw [weight, exponent]72    exact monoidPow.zero73  have extended := finiteRingProduct.unit_extension with *74  have value := monomialEvaluate.value at I, A, add, zero, neg, mul, one, v, m with *75  cc7677theorem monomialEvaluate.one78  shows monomialEvaluate(I, A, add, zero, neg, mul, one, v)(monomialOne(I)) = one79proof80  have member := monomialOne.member at I81  have map := monomials.map with member82  have finite := CoefficientMap.finite_support with map83  have domain := functionSupport.subset at monomialOne(I), I, 084  have weights := monomialWeights.function at I, functionSupport(monomialOne(I), I, 0), A, add, zero, neg, mul, one, v, monomialOne(I) with *85  have values : ∀ i ∈ functionSupport(monomialOne(I), I, 0), monomialWeights(I, functionSupport(monomialOne(I), I, 0), A, add, zero, neg, mul, one, v,  monomialOne(I))(i) = one86    intros i hi87    have index := functionSupport.membership.forward with hi88    have exponent := monomialOne.value at I, i with *89    have weight := monomialWeights.value at I, functionSupport(monomialOne(I), I, 0), A, add, zero, neg, mul, one, v, monomialOne(I), i with *90    rw [weight, exponent]91    exact monoidPow.zero92  have product := finiteRingProduct.one at functionSupport(monomialOne(I), I, 0), A, add, zero, neg, mul, one, monomialWeights(I, functionSupport(monomialOne(I), I, 0), A, add, zero, neg, mul, one, v,  monomialOne(I)) with *93  have value := monomialEvaluate.value at I, A, add, zero, neg, mul, one, v, monomialOne(I) with *94  cc9596theorem monomialEvaluate.mul (m n : Set)97  requires memberM : m ∈ monomials(I)98  requires memberN : n ∈ monomials(I)99  shows monomialEvaluate(I, A, add, zero, neg, mul, one, v)(monomialProduct(I, m, n)) = call2(mul, monomialEvaluate(I, A, add, zero, neg, mul, one, v)(m), monomialEvaluate(I, A, add, zero, neg, mul, one, v)(n))100proof101  have memberProduct := monomialProduct.member at I, m, n with *102  have mapM := monomials.map with memberM103  have mapN := monomials.map with memberN104  have finiteM := CoefficientMap.finite_support with mapM105  have finiteN := CoefficientMap.finite_support with mapN106  have finite := Finite.union with finiteM, finiteN107  have domainM := functionSupport.subset at m, I, 0108  have domainN := functionSupport.subset at n, I, 0109  have domain : functionSupport(m, I, 0) ∪ functionSupport(n, I, 0) ⊆ I by simp [Subset, union2.membership]110  have coversM : functionSupport(m, I, 0) ⊆ functionSupport(m, I, 0) ∪ functionSupport(n, I, 0)111    simp [Subset, union2.membership]112  have coversN : functionSupport(n, I, 0) ⊆ functionSupport(m, I, 0) ∪ functionSupport(n, I, 0)113    simp [Subset, union2.membership]114  have support := monomialProduct.support at I, m, n with *115  have coversProduct : functionSupport(monomialProduct(I, m, n), I, 0) ⊆ functionSupport(m, I, 0) ∪ functionSupport(n, I, 0)116    rw support117    simp118  have productValue := monomialEvaluate.on_domain at I, A, add, zero, neg, mul, one, v, monomialProduct(I, m, n), functionSupport(m, I, 0) ∪ functionSupport(n, I, 0) with *119  have firstValue := monomialEvaluate.on_domain at I, A, add, zero, neg, mul, one, v, m, functionSupport(m, I, 0) ∪ functionSupport(n, I, 0) with *120  have secondValue := monomialEvaluate.on_domain at I, A, add, zero, neg, mul, one, v, n, functionSupport(m, I, 0) ∪ functionSupport(n, I, 0) with *121  have weightsM := monomialWeights.function at I, functionSupport(m, I, 0) ∪ functionSupport(n, I, 0), A, add, zero, neg, mul, one, v, m with *122  have weightsN := monomialWeights.function at I, functionSupport(m, I, 0) ∪ functionSupport(n, I, 0), A, add, zero, neg, mul, one, v, n with *123  have weightsProduct := monomialWeights.function at I, functionSupport(m, I, 0) ∪ functionSupport(n, I, 0), A, add, zero, neg, mul, one, v, monomialProduct(I, m, n) with *124  have equations : ∀ i ∈ functionSupport(m, I, 0) ∪ functionSupport(n, I, 0), monomialWeights(I, functionSupport(m, I, 0) ∪ functionSupport(n, I, 0), A, add, zero, neg, mul, one, v,  monomialProduct(I, m, n))(i) = call2(mul, monomialWeights(I, functionSupport(m, I, 0) ∪ functionSupport(n, I, 0), A, add, zero, neg, mul, one, v,  m)(i), monomialWeights(I, functionSupport(m, I, 0) ∪ functionSupport(n, I, 0), A, add, zero, neg, mul, one, v,  n)(i))125    intros i hi126    have included := domain127    have index := included with i, hi128    have exponentM := monomials.exponent at I, m, i with *129    have exponentN := monomials.exponent at I, n, i with *130    have image := FunctionBetween.apply_closed at v, I, A, i with *131    have ordinary := IsCommRing.ring with ring132    have multiplicative := IsRing.multiplicative with ordinary133    have power := monoidPow.add at A, mul, one, v(i), m(i), n(i) with *134    have exponent := monomialProduct.value at I, m, n, i with *135    have left := monomialWeights.value at I, functionSupport(m, I, 0) ∪ functionSupport(n, I, 0), A, add, zero, neg, mul, one, v, monomialProduct(I, m, n), i with *136    have first := monomialWeights.value at I, functionSupport(m, I, 0) ∪ functionSupport(n, I, 0), A, add, zero, neg, mul, one, v, m, i with *137    have second := monomialWeights.value at I, functionSupport(m, I, 0) ∪ functionSupport(n, I, 0), A, add, zero, neg, mul, one, v, n, i with *138    cc139  have multiply := finiteRingProduct.mul with *140  cc141142theorem monomialEvaluate.character143  shows MonomialCharacter(I, A, mul, one, monomialEvaluate(I, A, add, zero, neg, mul, one, v))144proof145  have function := monomialEvaluate.function at I, A, add, zero, neg, mul, one, v with *146  have unit := monomialEvaluate.one at I, A, add, zero, neg, mul, one, v with *147  unfold MonomialCharacter148  refine ⟨function, unit, ?_⟩149  intros m hm n hn150  exact monomialEvaluate.mul with *151152theorem monomialEvaluate.variable (j : Set)153  requires index : j ∈ I154  shows monomialEvaluate(I, A, add, zero, neg, mul, one, v)(monomialVariable(I, j)) = v(j)155proof156  have member := monomialVariable.member at I, j157  have finite := Finite.singleton at j158  have domain : {j} ⊆ I by simp [Subset, singleton.membership]159  have covers : functionSupport(monomialVariable(I, j), I, 0) ⊆ {j}160    intros i hi161    have data := functionSupport.membership.forward with hi162    have alternatives : i = j ∨ i ≠ j by tauto163    cases alternatives with same | other164    . exact singleton.membership.backward at i, j with same165    . have exponent := monomialVariable.other at I, j, i with *166      exfalso167      exact data.right with exponent168  have value := monomialEvaluate.on_domain at I, A, add, zero, neg, mul, one, v, monomialVariable(I, j), {j} with *169  have weights := monomialWeights.function at I, {j}, A, add, zero, neg, mul, one, v, monomialVariable(I, j) with *170  have product := finiteRingProduct.singleton at A, add, zero, neg, mul, one, monomialWeights(I, {j}, A, add, zero, neg, mul, one, v,  monomialVariable(I, j)), j with *171  have self := singleton.self at j172  have weight := monomialWeights.value at I, {j}, A, add, zero, neg, mul, one, v, monomialVariable(I, j), j with *173  have exponent := monomialVariable.same at I, j with *174  have image := FunctionBetween.apply_closed at v, I, A, j with *175  have ordinary := IsCommRing.ring with ring176  have multiplicative := IsRing.multiplicative with ordinary177  have identity := IsMonoid.right_identity at A, mul, one, v(j) with *178  rwa [value, product, weight, exponent, monoidPow.succ, monoidPow.zero]179180theorem polynomialAt.hom181  shows IsRingHom(polynomialAt(I, A, add, zero, neg, mul, one, v), polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), constantFunction(monomials(I), A, zero), polynomialNeg(I, A, add, zero, neg, mul, one), polynomialMul(I, A, add, zero, neg, mul, one), polynomialConstant(I, A, zero, one), A, add, zero, neg, mul, one)182proof183  have character := monomialEvaluate.character with *184  unfold polynomialAt185  exact polynomialEvaluate.hom with *186187theorem polynomialAt.constant (a : Set)188  requires coefficient : a ∈ A189  shows polynomialAt(I, A, add, zero, neg, mul, one, v)(polynomialConstant(I, A, zero, a)) = a190proof191  have character := monomialEvaluate.character with *192  unfold polynomialAt193  exact polynomialEvaluate.constant with *194195theorem polynomialAt.variable (j : Set)196  requires index : j ∈ I197  shows polynomialAt(I, A, add, zero, neg, mul, one, v)(polynomialVariable(I, A, zero, one, j)) = v(j)198proof199  have function := monomialEvaluate.function at I, A, add, zero, neg, mul, one, v with *200  have monomial := monomialVariable.member at I, j201  have ordinary := IsCommRing.ring with ring202  have multiplicative := IsRing.multiplicative with ordinary203  have oneIn := IsMonoid.unit_in_carrier with multiplicative204  have image := FunctionBetween.apply_closed at v, I, A, j with *205  have value := monomialEvaluate.variable at I, A, add, zero, neg, mul, one, v, j with *206  have term := polynomialEvaluate.term at I, A, add, zero, neg, mul, one, monomialEvaluate(I, A, add, zero, neg, mul, one, v), one, monomialVariable(I, j) with *207  have identity := IsMonoid.left_identity at A, mul, one, v(j) with *208  unfold polynomialAt209  unfold polynomialVariable210  cc211212theorem polynomialAt.surjective213  shows SurjectiveBetween(polynomialAt(I, A, add, zero, neg, mul, one, v), polynomials(I, A, zero), A)214proof215  have hom := polynomialAt.hom at I, A, add, zero, neg, mul, one, v with *216  have function := IsRingHom.function with hom217  have ordinary := IsCommRing.ring with ring218  have zeroIn := IsRing.zero_in_carrier with ordinary219  constructor220  . exact function221  . intros a ha222    have member := polynomialConstant.member at I, A, zero, a with *223    have value := polynomialAt.constant at I, A, add, zero, neg, mul, one, v, a with *224    have edge := FunctionBetween.relates_apply at polynomialAt(I, A, add, zero, neg, mul, one, v), polynomials(I, A, zero), A, polynomialConstant(I, A, zero, a) with *225    witness polynomialConstant(I, A, zero, a)226    constructor227    . exact member228    . rw value at edge229      exact edge230231theorem polynomialAt.kernel_ideal232  shows IsIdeal(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), constantFunction(monomials(I), A, zero), polynomialNeg(I, A, add, zero, neg, mul, one), polynomialMul(I, A, add, zero, neg, mul, one), ringKernel(polynomialAt(I, A, add, zero, neg, mul, one, v), polynomials(I, A, zero), zero))233proof234  have source := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *235  have hom := polynomialAt.hom with *236  exact IsRingHom.kernel_ideal with source, ring, hom237238end Evaluation239-- The certificate-to-unsatisfiability direction over every nontrivial ring.240predicate PolynomialCommonZero (I A add zero neg mul one G v : Set) :=241  FunctionBetween(v, I, A) ∧ (∀ p ∈ G, polynomialAt(I, A, add, zero, neg, mul, one, v)(p) = zero)242243notation scoped PolynomialCommonZero(I, R, G, v) => PolynomialCommonZero(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one, G, v)244245section Certificates246variable (I A add zero neg mul one G : Set)247hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)248hypothesis nontrivial : Nontrivial(A, zero, one)249notation ring R := (A, add, zero, neg, mul, one)250notation ring P := R[I]251252theorem polynomialIdeal.no_common_zero253  requires generators : G ⊆ P254  requires certificate : P[1] ∈ idealSpan(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), G)255  shows ¬(∃ v, PolynomialCommonZero(I, R, G, v))256proof257  intro exists258  obtain ⟨v, common⟩ := exists259  unfold PolynomialCommonZero at common260  have source := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *261  have hom := polynomialAt.hom at I, A, add, zero, neg, mul, one, v with *262  have impossible := idealSpan.unit_obstructs_vanishing with source, ring, hom, nontrivial, generators, certificate263  exact impossible with common.right264265theorem polynomialIdeal.no_common_zero_of_combination (p q a b : Set)266  requires generators : G ⊆ P267  requires hp : p ∈ G268  requires hq : q ∈ G269  requires ha : a ∈ P270  requires hb : b ∈ P271  requires identity : P[a * p + b * q] = P[1]272  shows ¬(∃ v, PolynomialCommonZero(I, R, G, v))273proof274  have source := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *275  have certificate := idealSpan.unit_of_linear_combination2 with source, generators, hp, hq, ha, hb, identity276  exact polynomialIdeal.no_common_zero with *277278end Certificates279