Grace/Cumulus/Algebra/Polynomial/Terms.g17

Open in Workbench Download source

Imports

Unit · CoefficientInduction

Declarations

Source

1-- Multiplication of monomial terms and structural polynomial induction (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.Terms8import Unit9import CoefficientInduction1011theorem polynomialTerm.support (I A zero a m : Set)12  requires zeroIn : zero ∈ A13  requires coefficient : a ∈ A14  shows functionSupport(polynomialTerm(I, A, zero, a, m), monomials(I), zero) ⊆ {m}15proof16  unfold polynomialTerm17  exact coefficientSingle.support with *1819theorem polynomialProduct.terms (I A add zero neg mul one a b m n : Set)20  requires ring : IsCommRing(A, add, zero, neg, mul, one)21  requires coefficientA : a ∈ A22  requires coefficientB : b ∈ A23  requires monomialM : m ∈ monomials(I)24  requires monomialN : n ∈ monomials(I)25  shows polynomialProduct(I, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n)) = polynomialTerm(I, A, zero, call2(mul, a, b), monomialProduct(I, m, n))26proof27  have ordinary := IsCommRing.ring with ring28  have zeroIn := IsRing.zero_in_carrier with ordinary29  have memberP := polynomialTerm.member at I, A, zero, a, m with *30  have memberQ := polynomialTerm.member at I, A, zero, b, n with *31  have supportP := polynomialTerm.support at I, A, zero, a, m with *32  have supportQ := polynomialTerm.support at I, A, zero, b, n with *33  have singletons : {m} × {n} = {(m, n)}34    ext t35    constructor36    . intro ht37      obtain ⟨bound, u, hu, v, hv, shape⟩ := product.membership.forward with ht38      have equalU := singleton.membership.forward with hu39      have equalV := singleton.membership.forward with hv40      apply singleton.membership.backward41      cc42    . intro ht43      have shape := singleton.membership.forward with ht44      rw shape45      have hm := singleton.self at m46      have hn := singleton.self at n47      exact product.pair with hm, hn48  have covers : convolutionPairs(I, zero, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n)) ⊆ {(m, n)}49    unfold convolutionPairs50    rw ← singletons51    exact product.monotone with supportP, supportQ52  have pair := product.pair at m, n, monomials(I), monomials(I) with *53  have domain : {(m, n)} ⊆ monomials(I) × monomials(I) by simp [Subset, singleton.membership]54  have finite := Finite.singleton at (m, n)55  have weights := boundedConvolutionWeights.function at I, {(m, n)}, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n) with *56  have bounded := polynomialProduct.on_domain with ring, memberP, memberQ, domain, finite, covers57  have pushed := finitePushforward.singleton at monomials(I), A, add, zero, neg, mul, one, monomialMul(I), boundedConvolutionWeights(I, {(m, n)}, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n)), (m, n) with *58  have singleton := singleton.self at (m, n)59  have weight := boundedConvolutionWeights.pair at I, {(m, n)}, A, add, zero, neg, mul, one, polynomialTerm(I, A, zero, a, m), polynomialTerm(I, A, zero, b, n), m, n with *60  have valueP := polynomialTerm.same at I, A, zero, a, m with *61  have valueQ := polynomialTerm.same at I, A, zero, b, n with *62  have index := monomialMul.apply at I, m, n with *63  unfold call2 at index64  rw [← bounded, pushed, weight, valueP, valueQ, index]65  unfold polynomialTerm66  rfl6768-- The property is represented by a set S; no extra induction axiom is used.69theorem polynomials.induction (I A add zero neg mul one S p : Set)70  requires ring : IsCommRing(A, add, zero, neg, mul, one)71  requires member : p ∈ polynomials(I, A, zero)72  requires base : constantFunction(monomials(I), A, zero) ∈ S73  requires terms : ∀ a ∈ A, ∀ m ∈ monomials(I), polynomialTerm(I, A, zero, a, m) ∈ S74  requires sums : ∀ f ∈ S, ∀ g ∈ S, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, f, g) ∈ S75  shows p ∈ S76proof77  have map := polynomials.map with member78  have step : ∀ a ∈ A, ∀ m ∈ monomials(I), ∀ f ∈ S, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, coefficientSingle(monomials(I), A, zero, a, m), f) ∈ S79    intros a ha m hm f hf80    have term := terms with a, ha, m, hm81    have result := sums with polynomialTerm(I, A, zero, a, m), term, f, hf82    unfold polynomialTerm at result83    exact result84  exact coefficientMaps.induction with *85