Grace/Cumulus/Algebra/Polynomial/Divisibility.g17

Open in Workbench Download source

Imports

Monomial

Declarations

Source

1-- Coordinatewise monomial divisibility and quotient monomials (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.Divisibility8import Monomial910predicate MonomialDivides (I m n : Set) := ∀ i ∈ I, m(i) ≤ n(i)1112theorem MonomialDivides.reflexive (I m : Set)13  requires member : m ∈ monomials(I)14  shows MonomialDivides(I, m, m)15proof16  intros i hi17  have natural := monomials.exponent with *18  exact LessEqual.reflexive with *1920theorem MonomialDivides.transitive (I m n p : Set)21  requires memberM : m ∈ monomials(I)22  requires memberN : n ∈ monomials(I)23  requires third : p ∈ monomials(I)24  requires left : MonomialDivides(I, m, n)25  requires right : MonomialDivides(I, n, p)26  shows MonomialDivides(I, m, p)27proof28  intros i hi29  have mNat := monomials.exponent at I, m, i with *30  have nNat := monomials.exponent at I, n, i with *31  have pNat := monomials.exponent at I, p, i with *32  have mn := left with i, hi33  have np := right with i, hi34  exact LessEqual.transitive with *3536theorem MonomialDivides.antisymmetric (I m n : Set)37  requires memberM : m ∈ monomials(I)38  requires memberN : n ∈ monomials(I)39  requires left : MonomialDivides(I, m, n)40  requires right : MonomialDivides(I, n, m)41  shows m = n42proof43  apply monomials.ext with memberM, memberN44  intros i hi45  have mNat := monomials.exponent at I, m, i with *46  have nNat := monomials.exponent at I, n, i with *47  have mn := left with i, hi48  have nm := right with i, hi49  exact LessEqual.antisymmetric with *5051theorem MonomialDivides.insert (I j m n : Set)52  requires previous : MonomialDivides(I, m, n)53  requires coordinate : m(j) ≤ n(j)54  shows MonomialDivides(insert(j, I), m, n)55proof56  intros i hi57  have alternatives := insert.membership.forward with hi58  cases alternatives with equal | old59  . rw equal60    exact coordinate61  . exact previous with i, old6263defunique naturalDifference (a b : Nat) (k ∈ ℕ) := a + k = b64requires bounded : a ≤ b65proof66  obtain ⟨k, natural, equation⟩ := bounded67  have member := nat.omega.forward with natural68  refine ⟨k, member, equation⟩69uniqueness70  intros u hu memberM v hv memberN71  have equal : a + u = a + v by cc72  exact add.left_cancel with equal7374theorem naturalDifference.natural (a b : Nat)75  requires bounded : a ≤ b76  shows Nat(naturalDifference(a, b))77proof78  have selected := naturalDifference.selected at a, b with *79  exact nat.omega.backward with selected.left8081theorem naturalDifference.add (a b : Nat)82  requires bounded : a ≤ b83  shows a + naturalDifference(a, b) = b84proof85  have selected := naturalDifference.selected at a, b with *86  exact selected.right8788defgraph monomialQuotient (I m n : Set) (i ∈ I) : ℕ := naturalDifference(m(i), n(i))89requires memberM : m ∈ monomials(I)90requires memberN : n ∈ monomials(I)91requires divides : MonomialDivides(I, m, n)92proof93  have mNat := monomials.exponent at I, m, i with *94  have nNat := monomials.exponent at I, n, i with *95  have bounded := divides with i, member96  have selected := naturalDifference.selected at m(i), n(i) with *97  exact selected.left9899theorem monomialQuotient.equation (I m n i : Set)100  requires memberM : m ∈ monomials(I)101  requires memberN : n ∈ monomials(I)102  requires divides : MonomialDivides(I, m, n)103  requires index : i ∈ I104  shows m(i) + monomialQuotient(I, m, n)(i) = n(i)105proof106  have value := monomialQuotient.value at I, m, n, i with *107  have mNat := monomials.exponent at I, m, i with *108  have nNat := monomials.exponent at I, n, i with *109  have bounded := divides with i, index110  rw value111  exact naturalDifference.add with *112113theorem monomialQuotient.support (I m n : Set)114  requires memberM : m ∈ monomials(I)115  requires memberN : n ∈ monomials(I)116  requires divides : MonomialDivides(I, m, n)117  shows functionSupport(monomialQuotient(I, m, n), I, 0) ⊆ functionSupport(n, I, 0)118proof119  have function := monomialQuotient.function at I, m, n with *120  intros i hi121  have data := functionSupport.membership.forward with hi122  have mNat := monomials.exponent at I, m, i with *123  have valueIn := FunctionBetween.apply_closed at monomialQuotient(I, m, n), I, ℕ, i with *124  have qNat := nat.omega.backward with valueIn125  have equation := monomialQuotient.equation at I, m, n, i with *126  have nonzero : n(i) ≠ 0127    intro zeroValue128    rw zeroValue at equation129    have zeros := add.eq_zero at monomialQuotient(I, m, n)(i), m(i) with *130    have both := zeros with equation131    exact data.right with both.right132  exact functionSupport.membership.backward with ⟨data.left, nonzero⟩133134theorem monomialQuotient.member (I m n : Set)135  requires memberM : m ∈ monomials(I)136  requires memberN : n ∈ monomials(I)137  requires divides : MonomialDivides(I, m, n)138  shows monomialQuotient(I, m, n) ∈ monomials(I)139proof140  have map := monomials.map with memberN141  have finite := CoefficientMap.finite_support with map142  have support := monomialQuotient.support with *143  have finiteQ := Finite.subset with finite, support144  have function := monomialQuotient.function at I, m, n with *145  apply monomials.contains146  unfold CoefficientMap147  refine ⟨function, finiteQ⟩148149theorem monomialQuotient.product (I m n : Set)150  requires memberM : m ∈ monomials(I)151  requires memberN : n ∈ monomials(I)152  requires divides : MonomialDivides(I, m, n)153  shows monomialProduct(I, m, monomialQuotient(I, m, n)) = n154proof155  have quotient := monomialQuotient.member with *156  have product := monomialProduct.member at I, m, monomialQuotient(I, m, n) with *157  apply monomials.ext with product, memberN158  intros i hi159  have value := monomialProduct.value at I, m, monomialQuotient(I, m, n), i with *160  rw value161  exact monomialQuotient.equation with *162163theorem MonomialDivides.product (I m q : Set)164  requires memberM : m ∈ monomials(I)165  requires memberN : q ∈ monomials(I)166  shows MonomialDivides(I, m, monomialProduct(I, m, q))167proof168  intros i hi169  have mNat := monomials.exponent at I, m, i with *170  have qNat := monomials.exponent at I, q, i with *171  have value := monomialProduct.value at I, m, q, i with *172  rw value173  exact LessEqual.add_right with *174175theorem MonomialDivides.iff_factor (I m n : Set)176  requires memberM : m ∈ monomials(I)177  requires memberN : n ∈ monomials(I)178  shows MonomialDivides(I, m, n) ↔ ∃ q ∈ monomials(I), monomialProduct(I, m, q) = n179proof180  constructor181  . intro divides182    have quotient := monomialQuotient.member with *183    have product := monomialQuotient.product with *184    refine ⟨monomialQuotient(I, m, n), quotient, product⟩185  . intro factored186    obtain ⟨q, member, equation⟩ := factored187    have divides := MonomialDivides.product at I, m, q with *188    rwa equation at divides189