Grace/Cumulus/Algebra/Polynomial/EvaluationHom.g17

Open in Workbench Download source

Imports

Evaluation

Declarations

Source

1-- Multiplicative monomial values extend canonically to polynomial homomorphisms.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.EvaluationHom8import Evaluation910predicate MonomialCharacter (I A mul one h : Set) :=11  FunctionBetween(h, monomials(I), A) ∧ h(monomialOne(I)) = one ∧12  (∀ m ∈ monomials(I), ∀ n ∈ monomials(I), h(monomialProduct(I, m, n)) = call2(mul, h(m), h(n)))1314predicate EvaluationMultiplies (I A add zero neg mul one h p q : Set) :=15  polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(polynomialProduct(I, A, add, zero, neg, mul, one, p, q)) = call2(mul, polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p), polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(q))1617def evaluationProducts (I A add zero neg mul one h p : Set) : Set :=18  {q ∈ polynomials(I, A, zero) | EvaluationMultiplies(I, A, add, zero, neg, mul, one, h, p, q)}1920-- Sending every monomial to one evaluates every variable at one.21theorem MonomialCharacter.at_one (I A add zero neg mul one : Set)22  requires ring : IsCommRing(A, add, zero, neg, mul, one)23  shows MonomialCharacter(I, A, mul, one, constantFunction(monomials(I), A, one))24proof25  have ordinary := IsCommRing.ring with ring26  have multiplicative := IsRing.multiplicative with ordinary27  have oneIn := IsMonoid.unit_in_carrier with multiplicative28  have function := constantFunction.function at monomials(I), A, one with *29  have unit := monomialOne.member at I30  have unitValue := constantFunction.apply at monomials(I), A, monomialOne(I), one with *31  unfold MonomialCharacter32  refine ⟨function, unitValue, ?_⟩33  intros m hm n hn34  have product := monomialProduct.member with hm, hn35  have left := constantFunction.apply at monomials(I), A, monomialProduct(I, m, n), one with *36  have first := constantFunction.apply at monomials(I), A, m, one with *37  have second := constantFunction.apply at monomials(I), A, n, one with *38  have identity := IsMonoid.left_identity with *39  cc4041section Evaluation42variable (I A add zero neg mul one h : Set)43hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)44hypothesis character : MonomialCharacter(I, A, mul, one, h)45notation ring R := (A, add, zero, neg, mul, one)4647theorem EvaluationMultiplies.zero (p : Set)48  requires member : p ∈ polynomials(I, A, zero)49  shows EvaluationMultiplies(I, A, add, zero, neg, mul, one, h, p, constantFunction(monomials(I), A, zero))50proof51  unfold MonomialCharacter at character52  have product := polynomialProduct.zero_right with *53  have zeroValue := polynomialEvaluate.zero at I, A, add, zero, neg, mul, one, h with *54  have valueP := polynomialEvaluate.in_carrier at I, A, add, zero, neg, mul, one, h, p with *55  have annihilate : polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p) * zero = zero by ring56  unfold EvaluationMultiplies57  cc5859theorem EvaluationMultiplies.swap (p q : Set)60  requires memberP : p ∈ polynomials(I, A, zero)61  requires memberQ : q ∈ polynomials(I, A, zero)62  requires equation : EvaluationMultiplies(I, A, add, zero, neg, mul, one, h, p, q)63  shows EvaluationMultiplies(I, A, add, zero, neg, mul, one, h, q, p)64proof65  unfold MonomialCharacter at character66  have comm := polynomialProduct.commutative at I, A, add, zero, neg, mul, one, p, q with *67  have valueP := polynomialEvaluate.in_carrier at I, A, add, zero, neg, mul, one, h, p with *68  have valueQ := polynomialEvaluate.in_carrier at I, A, add, zero, neg, mul, one, h, q with *69  have commute : polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p) * polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(q) = polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(q) * polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p)70    ring71  unfold EvaluationMultiplies at equation72  unfold EvaluationMultiplies73  cc7475theorem EvaluationMultiplies.add (p q r : Set)76  requires memberP : p ∈ polynomials(I, A, zero)77  requires memberQ : q ∈ polynomials(I, A, zero)78  requires memberR : r ∈ polynomials(I, A, zero)79  requires first : EvaluationMultiplies(I, A, add, zero, neg, mul, one, h, p, q)80  requires second : EvaluationMultiplies(I, A, add, zero, neg, mul, one, h, p, r)81  shows EvaluationMultiplies(I, A, add, zero, neg, mul, one, h, p, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, q, r))82proof83  unfold MonomialCharacter at character84  have pq := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, q with *85  have pr := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, r with *86  have distribute := polynomialProduct.add_right at I, A, add, zero, neg, mul, one, p, q, r with *87  have evaluateSum := polynomialEvaluate.add at I, A, add, zero, neg, mul, one, h, q, r with *88  have evaluateProducts := polynomialEvaluate.add at I, A, add, zero, neg, mul, one, h, polynomialProduct(I, A, add, zero, neg, mul, one, p, q), polynomialProduct(I, A, add, zero, neg, mul, one, p, r) with *89  have valueP := polynomialEvaluate.in_carrier at I, A, add, zero, neg, mul, one, h, p with *90  have valueQ := polynomialEvaluate.in_carrier at I, A, add, zero, neg, mul, one, h, q with *91  have valueR := polynomialEvaluate.in_carrier at I, A, add, zero, neg, mul, one, h, r with *92  have distributeValues : polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p) * (polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(q) + polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(r)) = polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p) * polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(q) + polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p) * polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(r)93    ring94  unfold EvaluationMultiplies at first95  unfold EvaluationMultiplies at second96  unfold EvaluationMultiplies97  cc9899theorem EvaluationMultiplies.terms (a b m n : Set)100  requires coefficientA : a ∈ A101  requires coefficientB : b ∈ A102  requires monomialM : m ∈ monomials(I)103  requires monomialN : n ∈ monomials(I)104  shows EvaluationMultiplies(I, A, add, zero, neg, mul, one, h, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n))105proof106  have data := character107  have values := data.left108  have multiplication := data.right.right with m, monomialM, n, monomialN109  have ordinary := IsCommRing.ring with ring110  have coefficient := IsRing.mul_closed at A, add, zero, neg, mul, one, a, b with *111  have monomial := monomialProduct.member at I, m, n with *112  have product := polynomialProduct.terms at I, A, add, zero, neg, mul, one, a, b, m, n with *113  have left := polynomialEvaluate.term at I, A, add, zero, neg, mul, one, h, a * b, monomialProduct(I, m, n) with *114  have valueA := polynomialEvaluate.term at I, A, add, zero, neg, mul, one, h, a, m with *115  have valueB := polynomialEvaluate.term at I, A, add, zero, neg, mul, one, h, b, n with *116  have imageM := FunctionBetween.apply_closed at h, monomials(I), A, m with *117  have imageN := FunctionBetween.apply_closed at h, monomials(I), A, n with *118  have rearrange : (a * b) * (h(m) * h(n)) = (a * h(m)) * (b * h(n)) by ring119  unfold EvaluationMultiplies120  cc121122theorem EvaluationMultiplies.term (a m q : Set)123  requires coefficient : a ∈ A124  requires monomial : m ∈ monomials(I)125  requires memberQ : q ∈ polynomials(I, A, zero)126  shows EvaluationMultiplies(I, A, add, zero, neg, mul, one, h, polynomialTerm(I, A, zero, a, m), q)127proof128  have ordinary := IsCommRing.ring with ring129  have zeroIn := IsRing.zero_in_carrier with ordinary130  have zeroPolynomial := polynomials.zero at I, A, add, zero, neg, mul, one with *131  have fixed := polynomialTerm.member at I, A, zero, a, m with *132  have base : constantFunction(monomials(I), A, zero) ∈ evaluationProducts(I, A, add, zero, neg, mul, one, h, polynomialTerm(I, A, zero, a, m))133    apply evaluationProducts.membership.backward134    constructor135    . exact zeroPolynomial136    . exact EvaluationMultiplies.zero with *137  have terms : ∀ b ∈ A, ∀ n ∈ monomials(I), polynomialTerm(I, A, zero, b, n) ∈ evaluationProducts(I, A, add, zero, neg, mul, one, h, polynomialTerm(I, A, zero, a, m))138    intros b hb n hn139    have member := polynomialTerm.member at I, A, zero, b, n with *140    apply evaluationProducts.membership.backward141    constructor142    . exact member143    . exact EvaluationMultiplies.terms with *144  have sums : ∀ f ∈ evaluationProducts(I, A, add, zero, neg, mul, one, h, polynomialTerm(I, A, zero, a, m)), ∀ g ∈ evaluationProducts(I, A, add, zero, neg, mul, one, h, polynomialTerm(I, A, zero, a, m)), coefficientAdd(monomials(I), A, add, zero, neg, mul, one, f, g) ∈ evaluationProducts(I, A, add, zero, neg, mul, one, h, polynomialTerm(I, A, zero, a, m))145    intros f hf g hg146    have first := evaluationProducts.membership.forward with hf147    have second := evaluationProducts.membership.forward with hg148    have member := polynomials.add at I, A, add, zero, neg, mul, one, f, g with *149    apply evaluationProducts.membership.backward150    constructor151    . exact member152    . exact EvaluationMultiplies.add with *153  have generated := polynomials.induction at I, A, add, zero, neg, mul, one, evaluationProducts(I, A, add, zero, neg, mul, one, h, polynomialTerm(I, A, zero, a, m)), q with *154  have result := evaluationProducts.membership.forward with generated155  exact result.right156157theorem polynomialEvaluate.mul (p q : Set)158  requires memberP : p ∈ polynomials(I, A, zero)159  requires memberQ : q ∈ polynomials(I, A, zero)160  shows polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(polynomialProduct(I, A, add, zero, neg, mul, one, p, q)) = polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p) * polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(q)161proof162  have ordinary := IsCommRing.ring with ring163  have zeroIn := IsRing.zero_in_carrier with ordinary164  have zeroPolynomial := polynomials.zero at I, A, add, zero, neg, mul, one with *165  have base : constantFunction(monomials(I), A, zero) ∈ evaluationProducts(I, A, add, zero, neg, mul, one, h, q)166    apply evaluationProducts.membership.backward167    constructor168    . exact zeroPolynomial169    . exact EvaluationMultiplies.zero with *170  have terms : ∀ b ∈ A, ∀ n ∈ monomials(I), polynomialTerm(I, A, zero, b, n) ∈ evaluationProducts(I, A, add, zero, neg, mul, one, h, q)171    intros b hb n hn172    have member := polynomialTerm.member at I, A, zero, b, n with *173    apply evaluationProducts.membership.backward174    constructor175    . exact member176    . have forward := EvaluationMultiplies.term at I, A, add, zero, neg, mul, one, h, b, n, q with *177      exact EvaluationMultiplies.swap with *178  have sums : ∀ f ∈ evaluationProducts(I, A, add, zero, neg, mul, one, h, q), ∀ g ∈ evaluationProducts(I, A, add, zero, neg, mul, one, h, q), coefficientAdd(monomials(I), A, add, zero, neg, mul, one, f, g) ∈ evaluationProducts(I, A, add, zero, neg, mul, one, h, q)179    intros f hf g hg180    have first := evaluationProducts.membership.forward with hf181    have second := evaluationProducts.membership.forward with hg182    have member := polynomials.add at I, A, add, zero, neg, mul, one, f, g with *183    apply evaluationProducts.membership.backward184    constructor185    . exact member186    . exact EvaluationMultiplies.add with *187  have generated := polynomials.induction at I, A, add, zero, neg, mul, one, evaluationProducts(I, A, add, zero, neg, mul, one, h, q), p with *188  have result := evaluationProducts.membership.forward with generated189  exact EvaluationMultiplies.swap at190    I, A, add, zero, neg, mul, one, h, q, p with *191192theorem polynomialEvaluate.constant (a : Set)193  requires coefficient : a ∈ A194  shows polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(polynomialConstant(I, A, zero, a)) = a195proof196  unfold MonomialCharacter at character197  have unit := monomialOne.member at I198  have term := polynomialEvaluate.term at I, A, add, zero, neg, mul, one, h, a, monomialOne(I) with *199  have identity : a * one = a by ring200  unfold polynomialConstant201  cc202203theorem polynomialEvaluate.hom204  shows IsRingHom(polynomialEvaluate(I, A, add, zero, neg, mul, one, h), 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)205proof206  have data := character207  unfold MonomialCharacter at data208  have ordinary := IsCommRing.ring with ring209  have multiplicative := IsRing.multiplicative with ordinary210  have oneIn := IsMonoid.unit_in_carrier with multiplicative211  have function := polynomialEvaluate.function at I, A, add, zero, neg, mul, one, h with *212  have preservesZero := polynomialEvaluate.zero at I, A, add, zero, neg, mul, one, h with *213  have preservesOne := polynomialEvaluate.constant with *214  have preservesNeg : ∀ p ∈ polynomials(I, A, zero), polynomialEvaluate(I, A, add, zero, neg, mul, one, h)((polynomialNeg(I, A, add, zero, neg, mul, one))(p)) = -polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p)215    intros p hp216    have operation := polynomialNeg.apply with *217    have value := polynomialEvaluate.neg at I, A, add, zero, neg, mul, one, h, p with *218    cc219  have preservesAdd : ∀ p ∈ polynomials(I, A, zero), ∀ q ∈ polynomials(I, A, zero), polynomialEvaluate(I, A, add, zero, neg, mul, one, h)((polynomialAdd(I, A, add, zero, neg, mul, one))(p, q)) = polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p) + polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(q)220    intros p hp q hq221    have operation := polynomialAdd.apply with hp, hq222    have value := polynomialEvaluate.add at I, A, add, zero, neg, mul, one, h, p, q with *223    cc224  have preservesMul : ∀ p ∈ polynomials(I, A, zero), ∀ q ∈ polynomials(I, A, zero), polynomialEvaluate(I, A, add, zero, neg, mul, one, h)((polynomialMul(I, A, add, zero, neg, mul, one))(p, q)) = polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(p) * polynomialEvaluate(I, A, add, zero, neg, mul, one, h)(q)225    intros p hp q hq226    have operation := polynomialMul.apply with hp, hq227    have value := polynomialEvaluate.mul with hp, hq228    cc229  unfold IsRingHom230  refine ⟨function, preservesZero, preservesOne, preservesNeg, preservesAdd, preservesMul⟩231232end Evaluation233