Grace/Cumulus/Algebra/Polynomial/IdealSupport.g17

Open in Workbench Download source

Imports

Ring

Declarations

Source

1-- Closure of polynomial supports in monomial ideals under the ring operations.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.IdealSupport8import Ring910section Rings11variable (I A add zero neg mul one U : Set)12hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)1314theorem monomialIdealPolynomials.zero15  shows constantFunction(monomials(I), A, zero) ∈ monomialIdealPolynomials(I, A, zero, U)16proof17  have polynomial := polynomials.zero at I, A, add, zero, neg, mul, one with *18  have ordinary := IsCommRing.ring with ring19  have zeroIn := IsRing.zero_in_carrier with ordinary20  apply monomialIdealPolynomials.membership.backward21  refine ⟨polynomial, _⟩22  intros m hm23  have data := functionSupport.membership.forward with hm24  have value := constantFunction.apply at monomials(I), A, m, zero with *25  exfalso26  exact data.right with value2728theorem monomialIdealPolynomials.add (p q : Set)29  requires memberP : p ∈ monomialIdealPolynomials(I, A, zero, U)30  requires memberQ : q ∈ monomialIdealPolynomials(I, A, zero, U)31  shows coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q) ∈ monomialIdealPolynomials(I, A, zero, U)32proof33  have dataP := monomialIdealPolynomials.membership.forward with memberP34  have dataQ := monomialIdealPolynomials.membership.forward with memberQ35  have polynomial := polynomials.add at I, A, add, zero, neg, mul, one, p, q with *36  have functionP := polynomials.function with dataP.left37  have functionQ := polynomials.function with dataQ.left38  have support := coefficientAdd.support at monomials(I), A, add, zero, neg, mul, one, p, q with *39  have unionBound : functionSupport(p, monomials(I), zero) ∪ functionSupport(q, monomials(I), zero) ⊆ U40    have boundP := dataP.right41    have boundQ := dataQ.right42    simp [Subset, union2.membership]43  have bounded := Subset.transitive with support, unionBound44  exact monomialIdealPolynomials.membership.backward with ⟨polynomial, bounded⟩4546theorem monomialIdealPolynomials.neg (p : Set)47  requires memberP : p ∈ monomialIdealPolynomials(I, A, zero, U)48  shows coefficientNeg(monomials(I), A, add, zero, neg, mul, one, p) ∈ monomialIdealPolynomials(I, A, zero, U)49proof50  have data := monomialIdealPolynomials.membership.forward with memberP51  have polynomial := polynomials.neg at I, A, add, zero, neg, mul, one, p with *52  have function := polynomials.function with data.left53  have support := coefficientNeg.support with *54  have bounded := Subset.transitive with support, data.right55  exact monomialIdealPolynomials.membership.backward with ⟨polynomial, bounded⟩5657theorem monomialIdealPolynomials.mul_right (p q : Set)58  requires ideal : MonomialIdeal(I, U)59  requires memberP : p ∈ monomialIdealPolynomials(I, A, zero, U)60  requires memberQ : q ∈ polynomials(I, A, zero)61  shows polynomialProduct(I, A, add, zero, neg, mul, one, p, q) ∈ monomialIdealPolynomials(I, A, zero, U)62proof63  have data := monomialIdealPolynomials.membership.forward with memberP64  have polynomial := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, q with *65  have bounded : functionSupport(polynomialProduct(I, A, add, zero, neg, mul, one, p, q), monomials(I), zero) ⊆ U66    intros m hm67    obtain ⟨u, hu, v, hv, equation⟩ := polynomialProduct.support_factor at I, A, add, zero, neg, mul, one, p, q, m with *68    have supportBound := data.right69    have inIdeal := supportBound with u, hu70    have monomial := functionSupport.membership.forward with hv71    have product := ideal.right with u, inIdeal, v, monomial.left72    rwa equation73  exact monomialIdealPolynomials.membership.backward with ⟨polynomial, bounded⟩7475theorem monomialIdealPolynomials.mul_left (p q : Set)76  requires ideal : MonomialIdeal(I, U)77  requires memberP : p ∈ polynomials(I, A, zero)78  requires memberQ : q ∈ monomialIdealPolynomials(I, A, zero, U)79  shows polynomialProduct(I, A, add, zero, neg, mul, one, p, q) ∈ monomialIdealPolynomials(I, A, zero, U)80proof81  have data := monomialIdealPolynomials.membership.forward with memberQ82  have comm := polynomialProduct.commutative at I, A, add, zero, neg, mul, one, p, q with *83  have absorbed := monomialIdealPolynomials.mul_right at I, A, add, zero, neg, mul, one, U, q, p with *84  rwa comm8586theorem monomialIdealPolynomials.ideal87  requires ideal : MonomialIdeal(I, U)88  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), monomialIdealPolynomials(I, A, zero, U))89proof90  have subset : monomialIdealPolynomials(I, A, zero, U) ⊆ polynomials(I, A, zero)91    intros p hp92    have data := monomialIdealPolynomials.membership.forward with hp93    exact data.left94  have zeroMember := monomialIdealPolynomials.zero at I, A, add, zero, neg, mul, one, U with *95  have addition : ∀ p ∈ monomialIdealPolynomials(I, A, zero, U), ∀ q ∈ monomialIdealPolynomials(I, A, zero, U), (polynomialAdd(I, A, add, zero, neg, mul, one))(p, q) ∈ monomialIdealPolynomials(I, A, zero, U)96    intros p hp q hq97    have dataP := monomialIdealPolynomials.membership.forward with hp98    have dataQ := monomialIdealPolynomials.membership.forward with hq99    have value := polynomialAdd.apply at I, A, add, zero, neg, mul, one, p, q with *100    rw value101    exact monomialIdealPolynomials.add at I, A, add, zero, neg, mul, one, U, p, q with *102  have negation : ∀ p ∈ monomialIdealPolynomials(I, A, zero, U), (polynomialNeg(I, A, add, zero, neg, mul, one))(p) ∈ monomialIdealPolynomials(I, A, zero, U)103    intros p hp104    have data := monomialIdealPolynomials.membership.forward with hp105    have value := polynomialNeg.apply at I, A, add, zero, neg, mul, one, p with *106    rw value107    exact monomialIdealPolynomials.neg at I, A, add, zero, neg, mul, one, U, p with *108  have absorption : ∀ p ∈ polynomials(I, A, zero), ∀ q ∈ monomialIdealPolynomials(I, A, zero, U), (polynomialMul(I, A, add, zero, neg, mul, one))(p, q) ∈ monomialIdealPolynomials(I, A, zero, U) ∧ (polynomialMul(I, A, add, zero, neg, mul, one))(q, p) ∈ monomialIdealPolynomials(I, A, zero, U)109    intros p hp q hq110    have data := monomialIdealPolynomials.membership.forward with hq111    have leftValue := polynomialMul.apply at I, A, add, zero, neg, mul, one, p, q with *112    have rightValue := polynomialMul.apply at I, A, add, zero, neg, mul, one, q, p with *113    constructor114    . rw leftValue115      exact monomialIdealPolynomials.mul_left at I, A, add, zero, neg, mul, one, U, p, q with *116    . rw rightValue117      exact monomialIdealPolynomials.mul_right at I, A, add, zero, neg, mul, one, U, q, p with *118  unfold IsIdeal119  refine ⟨subset, zeroMember, addition, negation, absorption⟩120121end Rings122