Grace/Cumulus/Algebra/Polynomial/MonomialShift.g17

Open in Workbench Download source

Imports

Ring · Terms

Declarations

Source

1-- Multiplication by a monomial shifts coefficients without collisions (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.MonomialShift8import Ring9import Terms1011def monomialShiftCorrect (I A add z neg mul one t m : Set) : Set :=12  {p ∈ polynomials(I, A, z) | polynomialProduct(I, A, add, z, neg, mul, one, polynomialTerm(I, A, z, one, t), p)(monomialProduct(I, t, m)) = p(m)}1314section Shift15variable (I A add z neg mul one t m : Set)16notation ring R := (A, add, z, neg, mul, one)17notation ring P := R[I]18hypothesis ring : IsCommRing(R)19hypothesis monomial : t ∈ monomials(I)20hypothesis target : m ∈ monomials(I)2122theorem monomialShiftCorrect.zero23  shows P[0] ∈ monomialShiftCorrect(I, A, add, z, neg, mul, one, t, m)24proof25  have zeroIn : R[0] ∈ R by typecheck26  have oneIn : R[1] ∈ R by typecheck27  have zeroPoly := polynomials.zero at I, A, add, z, neg, mul, one with *28  have term := polynomialTerm.member at I, A, z, one, t with *29  have shifted := monomialProduct.member at I, t, m with *30  have product := polynomialProduct.zero_right at I, A, add, z, neg, mul, one, polynomialTerm(I, A, z, one, t) with *31  have left := constantFunction.apply at monomials(I), A, monomialProduct(I, t, m), z with *32  have right := constantFunction.apply at monomials(I), A, m, z with *33  apply monomialShiftCorrect.membership.backward34  refine ⟨zeroPoly, ?_⟩35  cc3637theorem monomialShiftCorrect.term (a n : Set)38  requires coefficient : a ∈ R39  requires index : n ∈ monomials(I)40  shows polynomialTerm(I, A, z, a, n) ∈ monomialShiftCorrect(I, A, add, z, neg, mul, one, t, m)41proof42  have zeroIn : R[0] ∈ R by typecheck43  have oneIn : R[1] ∈ R by typecheck44  have member := polynomialTerm.member at I, A, z, a, n with *45  have shifted := monomialProduct.member at I, t, m with *46  have product := polynomialProduct.terms at I, A, add, z, neg, mul, one, one, a, t, n with *47  have unit : R[1 * a] = a by ring48  rw unit at product49  apply monomialShiftCorrect.membership.backward50  refine ⟨member, ?_⟩51  rw product52  have alternatives : m = n ∨ m ≠ n by tauto53  cases alternatives with equal | different54  . rw equal55    have shiftedN := monomialProduct.member at I, t, n with *56    have left := polynomialTerm.same at I, A, z, a, monomialProduct(I, t, n) with *57    have right := polynomialTerm.same at I, A, z, a, n with *58    cc59  . have distinct : monomialProduct(I, t, m) ≠ monomialProduct(I, t, n)60      intro equal61      have cancelled := monomialProduct.cancel with *62      exact different with cancelled63    have left := polynomialTerm.other at I, A, z, a, monomialProduct(I, t, n), monomialProduct(I, t, m) with *64    have right := polynomialTerm.other at I, A, z, a, n, m with *65    cc6667theorem monomialShiftCorrect.add (p q : Set)68  requires first : p ∈ monomialShiftCorrect(I, A, add, z, neg, mul, one, t, m)69  requires second : q ∈ monomialShiftCorrect(I, A, add, z, neg, mul, one, t, m)70  shows coefficientAdd(monomials(I), A, add, z, neg, mul, one, p, q) ∈ monomialShiftCorrect(I, A, add, z, neg, mul, one, t, m)71proof72  have left := monomialShiftCorrect.membership.forward with first73  have right := monomialShiftCorrect.membership.forward with second74  have zeroIn : R[0] ∈ R by typecheck75  have oneIn : R[1] ∈ R by typecheck76  have term := polynomialTerm.member at I, A, z, one, t with *77  have shifted := monomialProduct.member at I, t, m with *78  have sum := polynomials.add at I, A, add, z, neg, mul, one, p, q with *79  have productP := polynomialProduct.member at I, A, add, z, neg, mul, one, polynomialTerm(I, A, z, one, t), p with *80  have productQ := polynomialProduct.member at I, A, add, z, neg, mul, one, polynomialTerm(I, A, z, one, t), q with *81  have functionP := polynomials.function with left.left82  have functionQ := polynomials.function with right.left83  have functionProductP := polynomials.function with productP84  have functionProductQ := polynomials.function with productQ85  have distributes := polynomialProduct.add_right at I, A, add, z, neg, mul, one, polynomialTerm(I, A, z, one, t), p, q with *86  have value := coefficientAdd.value at monomials(I), A, add, z, neg, mul, one, p, q, m with *87  have productValue := coefficientAdd.value at monomials(I), A, add, z, neg, mul, one, polynomialProduct(I, A, add, z, neg, mul, one, polynomialTerm(I, A, z, one, t), p), polynomialProduct(I, A, add, z, neg, mul, one, polynomialTerm(I, A, z, one, t), q), monomialProduct(I, t, m) with *88  apply monomialShiftCorrect.membership.backward89  refine ⟨sum, ?_⟩90  cc9192theorem polynomialProduct.monomial_shift (p : Set)93  requires polynomial : p ∈ P94  shows polynomialProduct(I, A, add, z, neg, mul, one, polynomialTerm(I, A, z, one, t), p)(monomialProduct(I, t, m)) = p(m)95proof96  have base := monomialShiftCorrect.zero at I, A, add, z, neg, mul, one, t, m with *97  have terms : ∀ a ∈ A, ∀ n ∈ monomials(I), polynomialTerm(I, A, z, a, n) ∈ monomialShiftCorrect(I, A, add, z, neg, mul, one, t, m)98    intros a ha n hn99    exact monomialShiftCorrect.term with *100  have sums : ∀ u ∈ monomialShiftCorrect(I, A, add, z, neg, mul, one, t, m), ∀ v ∈ monomialShiftCorrect(I, A, add, z, neg, mul, one, t, m), coefficientAdd(monomials(I), A, add, z, neg, mul, one, u, v) ∈ monomialShiftCorrect(I, A, add, z, neg, mul, one, t, m)101    intros u hu v hv102    exact monomialShiftCorrect.add with *103  have member := polynomials.induction with *104  have data := monomialShiftCorrect.membership.forward with member105  exact data.right106107end Shift108theorem polynomialProduct.monomial_outside (I A add z neg mul one t m p : Set)109  requires ring : IsCommRing(A, add, z, neg, mul, one)110  requires monomial : t ∈ monomials(I)111  requires target : m ∈ monomials(I)112  requires polynomial : p ∈ polynomials(I, A, z)113  requires absent : ∀ n ∈ monomials(I), m ≠ monomialProduct(I, t, n)114  shows polynomialProduct(I, A, add, z, neg, mul, one, polynomialTerm(I, A, z, one, t), p)(m) = z115proof116  have ordinary := IsCommRing.ring with ring117  have zeroIn := IsRing.zero_in_carrier with ordinary118  have multiplicative := IsRing.multiplicative with ordinary119  have oneIn := IsMonoid.unit_in_carrier with multiplicative120  have term := polynomialTerm.member at I, A, z, one, t with *121  have bound := polynomialTerm.support at I, A, z, one, t with *122  by_contra nonzero123  have supported : m ∈ functionSupport(polynomialProduct(I, A, add, z, neg, mul, one, polynomialTerm(I, A, z, one, t), p), monomials(I), z)124    exact functionSupport.membership.backward with ⟨target, nonzero⟩125  obtain ⟨u, hu, n, hn, equal⟩ := polynomialProduct.support_factor at I, A, add, z, neg, mul, one, polynomialTerm(I, A, z, one, t), p, m with *126  have singleton := bound with u, hu127  have same := singleton.membership.forward with singleton128  have data := functionSupport.membership.forward with hn129  have different := absent with n, data.left130  apply different131  cc132133-- A variable multiple has no term with zero exponent in that variable.134theorem polynomialProduct.variable_zero (I A add z neg mul one j m p : Set)135  requires ring : IsCommRing(A, add, z, neg, mul, one)136  requires index : j ∈ I137  requires target : m ∈ monomials(I)138  requires polynomial : p ∈ polynomials(I, A, z)139  requires exponent : m(j) = 0140  shows polynomialProduct(I, A, add, z, neg, mul, one, polynomialVariable(I, A, z, one, j), p)(m) = z141proof142  have variable := monomialVariable.member at I, j143  have absent : ∀ n ∈ monomials(I), m ≠ monomialProduct(I, monomialVariable(I, j), n)144    intros n hn equal145    have nNat := monomials.exponent with hn146    have variableValue := monomialVariable.same at I, j with *147    have productValue := monomialProduct.value at I, monomialVariable(I, j), n, j with *148    have impossible : 0 = succ(n(j))149      have sum : 0 = 1 + n(j) by cc150      rwa [add, add] at sum151    exact Naturals.disjoint.zero.succ at n(j) with impossible152  unfold polynomialVariable153  exact polynomialProduct.monomial_outside with *154