Grace/Cumulus/Algebra/Polynomial/Monomial.g17

Open in Workbench Download source

Imports

CoefficientSingle

Declarations

Source

1-- Monomials as finitely supported natural-valued exponent maps (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.Monomial8import CoefficientSingle910def monomials (I : Set) : Set := coefficientMaps(I, ℕ, 0)11def monomialOne (I : Set) : Set := constantFunction(I, ℕ, 0)12def monomialVariable (I j : Set) : Set := coefficientSingle(I, ℕ, 0, 1, j)1314theorem monomials.map (I m : Set)15  requires member : m ∈ monomials(I)16  shows CoefficientMap(m, I, ℕ, 0)17proof18  unfold monomials at member19  have data := coefficientMaps.membership.forward with member20  exact data.right2122theorem monomials.contains (I m : Set)23  requires map : CoefficientMap(m, I, ℕ, 0)24  shows m ∈ monomials(I)25proof26  unfold monomials27  exact coefficientMaps.contains with map2829theorem monomials.function (I m : Set)30  requires member : m ∈ monomials(I)31  shows m : I → ℕ32proof33  have map := monomials.map with member34  exact CoefficientMap.function with map3536theorem monomials.exponent (I m i : Set)37  requires member : m ∈ monomials(I)38  requires index : i ∈ I39  shows Nat(m(i))40proof41  have function := monomials.function with member42  have value := FunctionBetween.apply_closed with function, index43  exact nat.omega.backward with value4445theorem monomials.ext (I m n : Set)46  requires left : m ∈ monomials(I)47  requires right : n ∈ monomials(I)48  requires exponents : ∀ i ∈ I, m(i) = n(i)49  shows m = n50proof51  have functionM := monomials.function with left52  have functionN := monomials.function with right53  exact FunctionBetween.ext with functionM, functionN, exponents5455theorem monomialOne.value (I i : Set)56  requires index : i ∈ I57  shows monomialOne(I)(i) = 058proof59  have zeroIn := nat.omega.forward with Naturals.constructor.zero60  unfold monomialOne61  exact constantFunction.apply with *6263theorem monomialOne.member (I : Set)64  shows monomialOne(I) ∈ monomials(I)65proof66  have zeroIn := nat.omega.forward with Naturals.constructor.zero67  have function : monomialOne(I) : I → ℕ68    unfold monomialOne69    exact constantFunction.function with *70  have support : functionSupport(monomialOne(I), I, 0) = ∅71    ext i72    constructor73    . intro member74      have data := functionSupport.membership.forward with member75      have value := monomialOne.value with data.left76      have contradiction := data.right with value77      tauto78    . intro member79      simp80  apply monomials.contains81  unfold CoefficientMap82  refine ⟨function, ?_⟩83  rw support84  exact Finite.empty8586theorem monomialVariable.member (I j : Set)87  shows monomialVariable(I, j) ∈ monomials(I)88proof89  have zeroIn := nat.omega.forward with Naturals.constructor.zero90  have oneNat := Naturals.constructor.succ with Naturals.constructor.zero91  have oneIn := nat.omega.forward with oneNat92  have map := CoefficientMap.single at I, ℕ, 0, 1, j with *93  apply monomials.contains94  unfold monomialVariable95  exact map9697theorem monomialVariable.same (I j : Set)98  requires index : j ∈ I99  shows monomialVariable(I, j)(j) = 1100proof101  have zeroIn := nat.omega.forward with Naturals.constructor.zero102  have oneNat := Naturals.constructor.succ with Naturals.constructor.zero103  have oneIn := nat.omega.forward with oneNat104  unfold monomialVariable105  exact coefficientSingle.same with *106107theorem monomialVariable.other (I j i : Set)108  requires index : i ∈ I109  requires different : i ≠ j110  shows monomialVariable(I, j)(i) = 0111proof112  have zeroIn := nat.omega.forward with Naturals.constructor.zero113  have oneNat := Naturals.constructor.succ with Naturals.constructor.zero114  have oneIn := nat.omega.forward with oneNat115  unfold monomialVariable116  exact coefficientSingle.other with *117118defgraph monomialProduct (I m n : Set) (i ∈ I) : ℕ := m(i) + n(i)119requires left : m ∈ monomials(I)120requires right : n ∈ monomials(I)121proof122  have mNat := monomials.exponent at I, m, i with *123  have nNat := monomials.exponent at I, n, i with *124  have sumNat : Nat(m(i) + n(i)) by typecheck125  exact nat.omega.forward with sumNat126127theorem monomialProduct.support (I m n : Set)128  requires left : m ∈ monomials(I)129  requires right : n ∈ monomials(I)130  shows functionSupport(monomialProduct(I, m, n), I, 0) = functionSupport(m, I, 0) ∪ functionSupport(n, I, 0)131proof132  ext i133  constructor134  . intro member135    have data := functionSupport.membership.forward with member136    have value := monomialProduct.value at I, m, n, i with *137    have mNat := monomials.exponent at I, m, i with *138    have nNat := monomials.exponent at I, n, i with *139    have zeroSum : m(i) = 0 → n(i) = 0 → m(i) + n(i) = 0140      intros mZero nZero141      rw [mZero, nZero]142      compute143    have nonzeroSum : m(i) + n(i) ≠ 0144      intro equal145      have impossible : monomialProduct(I, m, n)(i) = 0 by cc146      exact data.right with impossible147    have memM := functionSupport.membership at m, I, 0, i148    have memN := functionSupport.membership at n, I, 0, i149    apply union2.membership.backward150    tauto151  . intro member152    have alternatives := union2.membership.forward with member153    have memM := functionSupport.membership at m, I, 0, i154    have memN := functionSupport.membership at n, I, 0, i155    have index : i ∈ I by tauto156    have mNat := monomials.exponent at I, m, i with *157    have nNat := monomials.exponent at I, n, i with *158    have value := monomialProduct.value at I, m, n, i with *159    have bothZero := add.eq_zero at n(i), m(i) with *160    have nonzero : monomialProduct(I, m, n)(i) ≠ 0161      intro equal162      have sumZero : m(i) + n(i) = 0 by cc163      have zeros := bothZero with sumZero164      tauto165    exact functionSupport.membership.backward with ⟨index, nonzero⟩166167theorem monomialProduct.member (I m n : Set)168  requires left : m ∈ monomials(I)169  requires right : n ∈ monomials(I)170  shows monomialProduct(I, m, n) ∈ monomials(I)171proof172  have mapM := monomials.map with left173  have mapN := monomials.map with right174  have finiteM := CoefficientMap.finite_support with mapM175  have finiteN := CoefficientMap.finite_support with mapN176  have finite := Finite.union with finiteM, finiteN177  have support := monomialProduct.support with left, right178  have function := monomialProduct.function at I, m, n with *179  apply monomials.contains180  unfold CoefficientMap181  refine ⟨function, ?_⟩182  rwa support183184theorem monomialProduct.commutative (I m n : Set)185  requires left : m ∈ monomials(I)186  requires right : n ∈ monomials(I)187  shows monomialProduct(I, m, n) = monomialProduct(I, n, m)188proof189  have productM := monomialProduct.member at I, m, n with *190  have productN := monomialProduct.member at I, n, m with *191  apply monomials.ext with productM, productN192  intros i hi193  have mNat := monomials.exponent at I, m, i with *194  have nNat := monomials.exponent at I, n, i with *195  have leftValue := monomialProduct.value at I, m, n, i with *196  have rightValue := monomialProduct.value at I, n, m, i with *197  rw [leftValue, rightValue]198  exact add.commutative with *199200theorem monomialProduct.associative (I m n p : Set)201  requires first : m ∈ monomials(I)202  requires second : n ∈ monomials(I)203  requires third : p ∈ monomials(I)204  shows monomialProduct(I, monomialProduct(I, m, n), p) = monomialProduct(I, m, monomialProduct(I, n, p))205proof206  have mn := monomialProduct.member at I, m, n with *207  have np := monomialProduct.member at I, n, p with *208  have left := monomialProduct.member at I, monomialProduct(I, m, n), p with *209  have right := monomialProduct.member at I, m, monomialProduct(I, n, p) with *210  apply monomials.ext with left, right211  intros i hi212  have mNat := monomials.exponent at I, m, i with *213  have nNat := monomials.exponent at I, n, i with *214  have pNat := monomials.exponent at I, p, i with *215  have mnValue := monomialProduct.value at I, m, n, i with *216  have npValue := monomialProduct.value at I, n, p, i with *217  have leftValue := monomialProduct.value at I, monomialProduct(I, m, n), p, i with *218  have rightValue := monomialProduct.value at I, m, monomialProduct(I, n, p), i with *219  rw [leftValue, rightValue, mnValue, npValue]220  exact add.associative with *221222theorem monomialProduct.one (I m : Set)223  requires member : m ∈ monomials(I)224  shows monomialProduct(I, m, monomialOne(I)) = m225proof226  have unit := monomialOne.member at I227  have product := monomialProduct.member at I, m, monomialOne(I) with *228  apply monomials.ext with product, member229  intros i hi230  have mNat := monomials.exponent at I, m, i with *231  have value := monomialProduct.value at I, m, monomialOne(I), i with *232  have unitValue := monomialOne.value at I, i with *233  rw [value, unitValue]234  exact add.right_unit at m(i) with *235236theorem monomialProduct.cancel (I m n p : Set)237  requires first : m ∈ monomials(I)238  requires second : n ∈ monomials(I)239  requires third : p ∈ monomials(I)240  requires equal : monomialProduct(I, m, n) = monomialProduct(I, m, p)241  shows n = p242proof243  apply monomials.ext with second, third244  intros i hi245  have mNat := monomials.exponent at I, m, i with *246  have nNat := monomials.exponent at I, n, i with *247  have pNat := monomials.exponent at I, p, i with *248  have leftValue := monomialProduct.value at I, m, n, i with *249  have rightValue := monomialProduct.value at I, m, p, i with *250  have sums : m(i) + n(i) = m(i) + p(i) by cc251  exact add.left_cancel with mNat, sums252253defunique monomialPairProduct (I p : Set) (result ∈ monomials(I)) :=254  ∃ m ∈ monomials(I), ∃ n ∈ monomials(I), p = (m, n) ∧ result = monomialProduct(I, m, n)255requires pair : p ∈ monomials(I) × monomials(I)256proof257  obtain ⟨bound, m, hm, n, hn, shape⟩ := product.membership.forward with pair258  have member := monomialProduct.member with hm, hn259  refine ⟨monomialProduct(I, m, n), member, m, hm, n, hn, shape, rfl⟩260uniqueness261  intros u hu first v hv second262  obtain ⟨m, hm, n, hn, shapeU, valueU⟩ := first263  obtain ⟨q, hq, r, hr, shapeV, valueV⟩ := second264  have pairs : (m, n) = (q, r) by cc265  have coordinates := orderedPair.injective with pairs266  cc267268defgraph monomialMul (I : Set) (p ∈ monomials(I) × monomials(I)) : monomials(I) := monomialPairProduct(I, p)269proof270  have selected := monomialPairProduct.selected with member271  exact selected.left272273theorem monomialMul.apply (I m n : Set)274  requires left : m ∈ monomials(I)275  requires right : n ∈ monomials(I)276  shows (monomialMul(I))(m, n) = monomialProduct(I, m, n)277proof278  have pair := product.pair at m, n, monomials(I), monomials(I) with *279  have selected := monomialPairProduct.selected with pair280  obtain ⟨q, hq, r, hr, shape, output⟩ := selected.right281  have coordinates := orderedPair.injective with shape282  have value := monomialMul.value with pair283  unfold call2284  cc285286theorem monomials.comm_monoid (I : Set)287  shows IsCommMonoid(monomials(I), monomialMul(I), monomialOne(I))288proof289  have operation := monomialMul.function at I290  have unit := monomialOne.member at I291  have associative : Associative(monomials(I), monomialMul(I))292    intros m hm n hn p hp293    have mn := monomialProduct.member with hm, hn294    have np := monomialProduct.member with hn, hp295    have leftInner := monomialMul.apply with hm, hn296    have rightInner := monomialMul.apply with hn, hp297    rw [leftInner, rightInner]298    have leftOuter := monomialMul.apply at I, monomialProduct(I, m, n), p with *299    have rightOuter := monomialMul.apply at I, m, monomialProduct(I, n, p) with *300    rw [leftOuter, rightOuter]301    exact monomialProduct.associative with *302  have identity : Identity(monomials(I), monomialMul(I), monomialOne(I))303    unfold Identity304    refine ⟨unit, ?_⟩305    intros m hm306    have leftValue := monomialMul.apply at I, monomialOne(I), m with *307    have rightValue := monomialMul.apply at I, m, monomialOne(I) with *308    have comm := monomialProduct.commutative at I, monomialOne(I), m with *309    have identity := monomialProduct.one with hm310    constructor311    . cc312    . cc313  have commutative : Commutative(monomials(I), monomialMul(I))314    intros m hm n hn315    have leftValue := monomialMul.apply with hm, hn316    have rightValue := monomialMul.apply with hn, hm317    have comm := monomialProduct.commutative with hm, hn318    cc319  unfold IsCommMonoid320  refine ⟨?_, commutative⟩321  unfold IsMonoid322  refine ⟨?_, identity⟩323  unfold IsSemigroup324  refine ⟨?_, associative⟩325  exact operation326327theorem monomialVariable.injective (I j k : Set)328  requires first : j ∈ I329  requires second : k ∈ I330  requires equal : monomialVariable(I, j) = monomialVariable(I, k)331  shows j = k332proof333  have alternatives : j = k ∨ j ≠ k by tauto334  cases alternatives with same | different335  . exact same336  . have valueJ := monomialVariable.same with first337    have valueK := monomialVariable.other with first, different338    have impossible : 0 = 1 by cc339    exfalso340    exact Naturals.disjoint.zero.succ at 0 with impossible341