Grace/Cumulus/Algebra/Polynomial/MonomialGeneration.g17

Open in Workbench Download source

Imports

Monomial · CoefficientInduction

Declarations

Source

1-- Monomial induction from the unit, variables, and multiplication (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.MonomialGeneration8import Monomial9import CoefficientInduction1011theorem monomialSingle.member (I j : Set, n : Nat)12  shows coefficientSingle(I, ℕ, 0, n, j) ∈ monomials(I)13proof14  have zeroIn := nat.omega.forward with Naturals.constructor.zero15  have nIn := nat.omega.forward at n with *16  have map := CoefficientMap.single at I, ℕ, 0, n, j with *17  exact monomials.contains with map1819theorem monomialSingle.zero (I j : Set)20  shows coefficientSingle(I, ℕ, 0, 0, j) = monomialOne(I)21proof22  have zeroIn := nat.omega.forward with Naturals.constructor.zero23  have function := coefficientSingle.function at I, ℕ, 0, 0, j with *24  have unit := monomialOne.member at I25  have unitFunction := monomials.function with unit26  apply FunctionBetween.ext with function, unitFunction27  intros i hi28  have value := coefficientSingle.value at I, ℕ, 0, 0, j, i with *29  have selected := singleValue.zero at ℕ, 0, j, i with *30  have unitValue := monomialOne.value with hi31  cc3233theorem monomialSingle.succ (I j : Set, n : Nat)34  requires index : j ∈ I35  shows coefficientSingle(I, ℕ, 0, n + 1, j) = monomialProduct(I, monomialVariable(I, j), coefficientSingle(I, ℕ, 0, n, j))36proof37  have zeroIn := nat.omega.forward with Naturals.constructor.zero38  have nIn := nat.omega.forward at n with *39  have successorIn := nat.omega.forward at n + 1 with *40  have first := monomialSingle.member at I, j, n + 1 with *41  have second := monomialSingle.member at I, j, n with *42  have variable := monomialVariable.member at I, j43  have product := monomialProduct.member at I, monomialVariable(I, j), coefficientSingle(I, ℕ, 0, n, j) with *44  apply monomials.ext with first, product45  intros i hi46  have value := monomialProduct.value at I, monomialVariable(I, j), coefficientSingle(I, ℕ, 0, n, j), i with *47  rw value48  have alternatives : i = j ∨ i ≠ j by tauto49  cases alternatives with same | different50  . rw same51    have left := coefficientSingle.same at I, ℕ, 0, n + 1, j with *52    have right := coefficientSingle.same at I, ℕ, 0, n, j with *53    have variableValue := monomialVariable.same at I, j with *54    rw [left, right, variableValue]55    exact add.commutative with *56  . have left := coefficientSingle.other at I, ℕ, 0, n + 1, j, i with *57    have right := coefficientSingle.other at I, ℕ, 0, n, j, i with *58    have variableValue := monomialVariable.other with *59    rw [left, right, variableValue]60    symm61    exact add.right_unit with *6263theorem monomialErase.member (I m j : Set)64  requires member : m ∈ monomials(I)65  shows coefficientErase(I, ℕ, 0, m, j) ∈ monomials(I)66proof67  have zeroIn := nat.omega.forward with Naturals.constructor.zero68  have map := monomials.map with member69  have function := CoefficientMap.function with map70  have finite := CoefficientMap.finite_support with map71  have erased := coefficientErase.function at I, ℕ, 0, m, j with *72  have support := coefficientErase.support at I, ℕ, 0, m, j with *73  have bounded : functionSupport(coefficientErase(I, ℕ, 0, m, j), I, 0) ⊆ functionSupport(m, I, 0)74    intros i hi75    have data := support with i, hi76    have difference := difference.membership.forward with data77    exact difference.left78  have finiteSupport := Finite.subset with finite, bounded79  apply monomials.contains80  unfold CoefficientMap81  refine ⟨erased, finiteSupport⟩8283theorem monomialErase.restore (I m j : Set)84  requires member : m ∈ monomials(I)85  requires index : j ∈ I86  shows monomialProduct(I, coefficientSingle(I, ℕ, 0, m(j), j), coefficientErase(I, ℕ, 0, m, j)) = m87proof88  have zeroIn := nat.omega.forward with Naturals.constructor.zero89  have function := monomials.function with member90  have exponent := monomials.exponent with *91  have exponentIn := nat.omega.forward at m(j) with *92  have single := monomialSingle.member at I, j, m(j) with *93  have erased := monomialErase.member at I, m, j with *94  have product := monomialProduct.member at I, coefficientSingle(I, ℕ, 0, m(j), j), coefficientErase(I, ℕ, 0, m, j) with *95  apply monomials.ext with product, member96  intros i hi97  have natural := monomials.exponent at I, m, i with *98  have value := monomialProduct.value at I, coefficientSingle(I, ℕ, 0, m(j), j), coefficientErase(I, ℕ, 0, m, j), i with *99  rw value100  have alternatives : i = j ∨ i ≠ j by tauto101  cases alternatives with same | different102  . rw same103    have left := coefficientSingle.same at I, ℕ, 0, m(j), j with *104    have right := coefficientErase.same at I, ℕ, 0, m, j with *105    rw [left, right]106    exact add.right_unit with *107  . have left := coefficientSingle.other at I, ℕ, 0, m(j), j, i with *108    have right := coefficientErase.other with zeroIn, function, different109    rw [left, right]110    exact add.left_unit with *111112section Generation113variable (I T : Set)114hypothesis unit : monomialOne(I) ∈ T115hypothesis variables : ∀ j ∈ I, monomialVariable(I, j) ∈ T116hypothesis products : ∀ m ∈ T, ∀ n ∈ T, monomialProduct(I, m, n) ∈ T117118theorem monomials.single_generated (j : Set, n : Nat)119  requires index : j ∈ I120  shows coefficientSingle(I, ℕ, 0, n, j) ∈ T121proof122  induction n123  | zero =>124    rw monomialSingle.zero125    exact unit126  | succ(k) using ih =>127    have variable := variables with j, index128    have next := products with monomialVariable(I, j), variable, coefficientSingle(I, ℕ, 0, k, j), ih129    have equation := monomialSingle.succ at I, j, k with *130    have successor := add.right_one at k with *131    rw successor at equation132    rw equation133    exact next134135theorem monomials.generated_list (xs : List(I))136  shows ∀ m ∈ monomials(I), functionSupport(m, I, 0) ⊆ listSupport{I}(xs) → m ∈ T137proof138  induction xs139  | List.nil =>140    intros f member covers141    have function := monomials.function with member142    have zeroIn := nat.omega.forward with Naturals.constructor.zero143    rw listSupport at covers144    have zeroFunction := constantFunction.function at I, ℕ, 0 with *145    have equal : f = constantFunction(I, ℕ, 0)146      apply FunctionBetween.ext with function, zeroFunction147      intros i hi148      have absent : ¬(i ∈ functionSupport(f, I, 0))149        intro supported150        have impossible := covers with i, supported151        exact set.empty with impossible152      have vanishes := functionSupport.outside with *153      have value := constantFunction.apply at I, ℕ, i, 0 with *154      cc155    rw equal156    unfold monomialOne at unit157    exact unit158  | List.cons(j, tail) using ih =>159    intros f member covers160    have function := monomials.function with member161    have zeroIn := nat.omega.forward with Naturals.constructor.zero162    have index : j ∈ I by assumption163    rw listSupport at covers164    have erased := coefficientErase.function at I, ℕ, 0, f, j with *165    have support := coefficientErase.support at I, ℕ, 0, f, j with *166    have smaller : functionSupport(coefficientErase(I, ℕ, 0, f, j), I, 0) ⊆ listSupport{I}(tail)167      intros i hi168      have data := support with i, hi169      have difference := difference.membership.forward with data170      have covered := covers with i, difference.left171      have alternatives := insert.membership.forward with covered172      cases alternatives with equal | old173      . have singleton : i ∈ {j}174          simp175        exfalso176        exact difference.right with singleton177      . exact old178    have erasedMember := monomialErase.member at I, f, j with *179    have rest := ih with coefficientErase(I, ℕ, 0, f, j), erasedMember, smaller180    have exponent := monomials.exponent with member, index181    have single := monomials.single_generated with *182    have next := products with coefficientSingle(I, ℕ, 0, f(j), j), single, coefficientErase(I, ℕ, 0, f, j), rest183    have restore := monomialErase.restore with member, index184    rwa restore at next185186theorem monomials.induction (m : Set)187  requires member : m ∈ monomials(I)188  shows m ∈ T189proof190  have map := monomials.map with member191  have finite := CoefficientMap.finite_support with map192  have subset := functionSupport.subset at m, I, 0193  obtain ⟨xs, list, covers⟩ := Finite.cover_in with finite, subset194  have generated := monomials.generated_list with *195  exact generated with m, member, covers196197end Generation198