PolynomialConvolution

Finite convolution and monomial-ideal absorption over arbitrary variable sets

Open in Workbench View on GitHub

1-- Finite convolution and monomial-ideal absorption over arbitrary variable sets.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 PolynomialConvolution8import Grace.Cumulus.Algebra.Polynomial.IdealSupport910section Polynomials11variable (I A add zero neg mul one : Set)12hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)1314theorem multiply (p q : Set)15  requires memberP : p ∈ polynomials(I, A, zero)16  requires memberQ : q ∈ polynomials(I, A, zero)17  shows polynomialProduct(I, A, add, zero, neg, mul, one, p, q) ∈ polynomials(I, A, zero)18proof19  exact polynomialProduct.member at I, A, add, zero, neg, mul, one, p, q with *2021-- A nonzero product coefficient must have a contributing pair of monomials.22-- Cancellation can remove such coefficients, so this is only one direction.23theorem supported_product_has_factors (p q m : Set)24  requires memberP : p ∈ polynomials(I, A, zero)25  requires memberQ : q ∈ polynomials(I, A, zero)26  requires supported : m ∈ functionSupport(polynomialProduct(I, A, add, zero, neg, mul, one, p, q), monomials(I), zero)27  shows ∃ u ∈ functionSupport(p, monomials(I), zero), ∃ v ∈ functionSupport(q, monomials(I), zero), m = monomialProduct(I, u, v)28proof29  exact polynomialProduct.support_factor at I, A, add, zero, neg, mul, one, p, q, m with *3031theorem zero_product (p : Set)32  requires memberP : p ∈ polynomials(I, A, zero)33  shows polynomialProduct(I, A, add, zero, neg, mul, one, p, constantFunction(monomials(I), A, zero)) = constantFunction(monomials(I), A, zero)34proof35  exact polynomialProduct.zero_right at I, A, add, zero, neg, mul, one, p with *3637theorem ideal_absorbs_product (U p q : Set)38  requires ideal : MonomialIdeal(I, U)39  requires memberP : p ∈ monomialIdealPolynomials(I, A, zero, U)40  requires memberQ : q ∈ polynomials(I, A, zero)41  shows polynomialProduct(I, A, add, zero, neg, mul, one, p, q) ∈ monomialIdealPolynomials(I, A, zero, U)42proof43  exact monomialIdealPolynomials.mul_right at I, A, add, zero, neg, mul, one, U, p, q with *4445-- Combine multiplication closure with the finite generators from Dickson.46theorem finite_generators_cover_product (U p q : Set)47  requires variables : Finite(I)48  requires ideal : MonomialIdeal(I, U)49  requires memberP : p ∈ monomialIdealPolynomials(I, A, zero, U)50  requires memberQ : q ∈ polynomials(I, A, zero)51  shows ∃ B, Finite(B) ∧ B ⊆ U ∧52    (∀ m ∈ functionSupport(polynomialProduct(I, A, add, zero, neg, mul, one, p, q), monomials(I), zero), ∃ b ∈ B, MonomialDivides(I, b, m))53proof54  have data := monomialIdealPolynomials.membership.forward with memberP55  have product := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, q with *56  have inIdeal := monomialIdealPolynomials.mul_right at I, A, add, zero, neg, mul, one, U, p, q with *57  obtain ⟨B, finite, subset, description⟩ := monomialIdealPolynomials.finite_description at I, A, zero, U with *58  have equivalence := description with polynomialProduct(I, A, add, zero, neg, mul, one, p, q), product59  refine ⟨B, finite, subset, _⟩60  tauto6162end Polynomials63