Grace/Cumulus/Algebra/Polynomial.g17

Open in Workbench Download source

Imports

MonomialIdeal · FactorTheorem · Ring.SumExtension

Declarations

Source

1-- Polynomial coefficient carriers, constants, and variables (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.Polynomial8import MonomialIdeal9import FactorTheorem10import Ring.SumExtension1112-- This base module constructs the carrier, constants, and variables.13-- Polynomial.Ring builds the commutative ring using finite convolution.14def polynomials (I A z : Set) : Set := coefficientMaps(monomials(I), A, z)15def polynomialTerm (I A z a m : Set) : Set := coefficientSingle(monomials(I), A, z, a, m)16def polynomialConstant (I A z a : Set) : Set := polynomialTerm(I, A, z, a, monomialOne(I))17def polynomialVariable (I A z unit j : Set) : Set := polynomialTerm(I, A, z, unit, monomialVariable(I, j))1819notation scoped polynomialVariable(I, R, j) => polynomialVariable(I, R.carrier, R.zero, R.one, j)2021notation scoped polynomialConstant(I, R, a) => polynomialConstant(I, R.carrier, R.zero, a)2223theorem polynomials.map (I A z p : Set)24  requires member : p ∈ polynomials(I, A, z)25  shows CoefficientMap(p, monomials(I), A, z)26proof27  unfold polynomials at member28  have data := coefficientMaps.membership.forward with member29  exact data.right3031theorem polynomials.contains (I A z p : Set)32  requires map : CoefficientMap(p, monomials(I), A, z)33  shows p ∈ polynomials(I, A, z)34proof35  unfold polynomials36  exact coefficientMaps.contains with map3738theorem polynomials.function (I A z p : Set)39  requires member : p ∈ polynomials(I, A, z)40  shows p : monomials(I) → A41proof42  have map := polynomials.map with member43  exact CoefficientMap.function with map4445theorem polynomials.coefficient (I A z p m : Set)46  requires member : p ∈ polynomials(I, A, z)47  requires monomial : m ∈ monomials(I)48  shows p(m) ∈ A49proof50  have function := polynomials.function with member51  exact FunctionBetween.apply_closed with function, monomial5253theorem polynomials.finite_support (I A z p : Set)54  requires member : p ∈ polynomials(I, A, z)55  shows Finite(functionSupport(p, monomials(I), z))56proof57  have map := polynomials.map with member58  exact CoefficientMap.finite_support with map5960theorem polynomials.ext (I A z p q : Set)61  requires left : p ∈ polynomials(I, A, z)62  requires right : q ∈ polynomials(I, A, z)63  requires coefficients : ∀ m ∈ monomials(I), p(m) = q(m)64  shows p = q65proof66  have functionP := polynomials.function with left67  have functionQ := polynomials.function with right68  exact FunctionBetween.ext with functionP, functionQ, coefficients6970theorem polynomialTerm.member (I A z a m : Set)71  requires zeroIn : z ∈ A72  requires coefficient : a ∈ A73  shows polynomialTerm(I, A, z, a, m) ∈ polynomials(I, A, z)74proof75  have map := CoefficientMap.single at monomials(I), A, z, a, m with *76  apply polynomials.contains77  unfold polynomialTerm78  exact map7980theorem polynomialTerm.same (I A z a m : Set)81  requires zeroIn : z ∈ A82  requires coefficient : a ∈ A83  requires monomial : m ∈ monomials(I)84  shows polynomialTerm(I, A, z, a, m)(m) = a85proof86  unfold polynomialTerm87  exact coefficientSingle.same with *8889theorem polynomialTerm.other (I A z a m n : Set)90  requires zeroIn : z ∈ A91  requires coefficient : a ∈ A92  requires monomial : n ∈ monomials(I)93  requires different : n ≠ m94  shows polynomialTerm(I, A, z, a, m)(n) = z95proof96  unfold polynomialTerm97  exact coefficientSingle.other with *9899theorem polynomialConstant.member (I A z a : Set)100  requires zeroIn : z ∈ A101  requires coefficient : a ∈ A102  shows polynomialConstant(I, A, z, a) ∈ polynomials(I, A, z)103proof104  unfold polynomialConstant105  exact polynomialTerm.member with *106107theorem polynomialConstant.coefficient (I A z a : Set)108  requires zeroIn : z ∈ A109  requires coefficient : a ∈ A110  shows polynomialConstant(I, A, z, a)(monomialOne(I)) = a111proof112  have unit := monomialOne.member at I113  unfold polynomialConstant114  exact polynomialTerm.same with *115116theorem polynomialConstant.injective (I A z a b : Set)117  requires zeroIn : z ∈ A118  requires left : a ∈ A119  requires right : b ∈ A120  requires equal : polynomialConstant(I, A, z, a) = polynomialConstant(I, A, z, b)121  shows a = b122proof123  have valueA := polynomialConstant.coefficient at I, A, z, a with *124  have valueB := polynomialConstant.coefficient at I, A, z, b with *125  cc126127theorem polynomialVariable.member (I A z unit j : Set)128  requires zeroIn : z ∈ A129  requires unitIn : unit ∈ A130  shows polynomialVariable(I, A, z, unit, j) ∈ polynomials(I, A, z)131proof132  unfold polynomialVariable133  exact polynomialTerm.member with *134135theorem polynomialVariable.coefficient (I A z unit j : Set)136  requires zeroIn : z ∈ A137  requires unitIn : unit ∈ A138  shows polynomialVariable(I, A, z, unit, j)(monomialVariable(I, j)) = unit139proof140  have monomial := monomialVariable.member at I, j141  unfold polynomialVariable142  exact polynomialTerm.same with *143144theorem polynomialTerm.index_injective (I A z a m n : Set)145  requires zeroIn : z ∈ A146  requires coefficient : a ∈ A147  requires first : m ∈ monomials(I)148  requires second : n ∈ monomials(I)149  requires nonzero : a ≠ z150  requires equal : polynomialTerm(I, A, z, a, m) = polynomialTerm(I, A, z, a, n)151  shows m = n152proof153  have alternatives : m = n ∨ m ≠ n by tauto154  cases alternatives with same | different155  . exact same156  . have valueM := polynomialTerm.same at I, A, z, a, m with *157    have valueN := polynomialTerm.other at I, A, z, a, n, m with *158    have impossible : a = z by cc159    exfalso160    exact nonzero with impossible161162theorem polynomialVariable.injective (I A z unit j k : Set)163  requires zeroIn : z ∈ A164  requires unitIn : unit ∈ A165  requires nonzero : unit ≠ z166  requires first : j ∈ I167  requires second : k ∈ I168  requires equal : polynomialVariable(I, A, z, unit, j) = polynomialVariable(I, A, z, unit, k)169  shows j = k170proof171  have monomialJ := monomialVariable.member at I, j172  have monomialK := monomialVariable.member at I, k173  unfold polynomialVariable at equal174  have equalMonomials := polynomialTerm.index_injective with *175  exact monomialVariable.injective with *176177section Rings178variable (I A add zero neg mul one : Set)179hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)180181theorem polynomials.zero182  shows constantFunction(monomials(I), A, zero) ∈ polynomials(I, A, zero)183proof184  have map := CoefficientMap.zero at monomials(I), A, add, zero, neg, mul, one with *185  exact polynomials.contains with map186187theorem polynomials.add (p q : Set)188  requires left : p ∈ polynomials(I, A, zero)189  requires right : q ∈ polynomials(I, A, zero)190  shows coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q) ∈ polynomials(I, A, zero)191proof192  have mapP := polynomials.map with left193  have mapQ := polynomials.map with right194  have combined := CoefficientMap.add with ring, mapP, mapQ195  exact polynomials.contains with combined196197theorem polynomials.neg (p : Set)198  requires member : p ∈ polynomials(I, A, zero)199  shows coefficientNeg(monomials(I), A, add, zero, neg, mul, one, p) ∈ polynomials(I, A, zero)200proof201  have map := polynomials.map with member202  have negative := CoefficientMap.neg with ring, map203  exact polynomials.contains with negative204205theorem polynomials.scale (a p : Set)206  requires scalar : a ∈ A207  requires member : p ∈ polynomials(I, A, zero)208  shows coefficientScale(monomials(I), A, add, zero, neg, mul, one, a, p) ∈ polynomials(I, A, zero)209proof210  have map := polynomials.map with member211  have scaled := CoefficientMap.scale with ring, scalar, map212  exact polynomials.contains with scaled213214end Rings215-- Polynomials whose nonzero coefficients lie in a monomial ideal.216def monomialIdealPolynomials (V A z U : Set) : Set :=217  {p ∈ polynomials(V, A, z) | functionSupport(p, monomials(V), z) ⊆ U}218219theorem monomialIdealPolynomials.finite_description (V A z U : Set)220  requires variables : Finite(V)221  requires ideal : MonomialIdeal(V, U)222  shows ∃ B, Finite(B) ∧ B ⊆ U ∧ (∀ p ∈ polynomials(V, A, z),223    p ∈ monomialIdealPolynomials(V, A, z, U) ↔224    (∀ m ∈ functionSupport(p, monomials(V), z), ∃ b ∈ B, MonomialDivides(V, b, m)))225proof226  obtain ⟨B, finite, included, equation⟩ := MonomialIdeal.finite_generated with variables, ideal227  refine ⟨B, finite, included, _⟩228  intros p polynomial229  constructor230  . intro member231    have data := monomialIdealPolynomials.membership.forward with member232    have bounded := data.right233    intros m hm234    have inIdeal := bounded with m, hm235    rw equation at inIdeal236    have span := monomialSpan.membership.forward with inIdeal237    exact span.right238  . intro covered239    have bounded : functionSupport(p, monomials(V), z) ⊆ U240      intros m hm241      have support := functionSupport.membership.forward with hm242      have generator := covered with m, hm243      rw equation244      apply monomialSpan.membership.backward245      constructor246      . exact support.left247      . exact generator248    exact monomialIdealPolynomials.membership.backward with ⟨polynomial, bounded⟩249