Grace/Cumulus/Algebra/Polynomial/Origin.g17

Open in Workbench Download source

Imports

Constants

Declarations

Source

1-- Constant coefficients and the evaluation homomorphism at the origin (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.Origin8import Constants910theorem monomialProduct.one_factors (I m n : Set)11  requires memberM : m ∈ monomials(I)12  requires memberN : n ∈ monomials(I)13  requires productOne : monomialProduct(I, m, n) = monomialOne(I)14  shows m = monomialOne(I) ∧ n = monomialOne(I)15proof16  have unit := monomialOne.member at I17  have first : m = monomialOne(I)18    apply monomials.ext with memberM, unit19    intros i hi20    have mNat := monomials.exponent at I, m, i with *21    have nNat := monomials.exponent at I, n, i with *22    have value := monomialProduct.value at I, m, n, i with *23    have zeroValue := monomialOne.value with hi24    have sumZero : m(i) + n(i) = 0 by cc25    have zeroRule := add.eq_zero_left at n(i), m(i) with *26    have vanishes := zeroRule with sumZero27    cc28  have second : n = monomialOne(I)29    have comm := monomialProduct.commutative at I, m, n with *30    have rightUnit := monomialProduct.one at I, n with *31    cc32  refine ⟨first, second⟩3334defgraph polynomialAtOrigin (I A zero : Set) (p ∈ polynomials(I, A, zero)) : A := p(monomialOne(I))35proof36  have unit := monomialOne.member at I37  exact polynomials.coefficient with *3839theorem polynomialProduct.constant_coefficient (I A add zero neg mul one p q : Set)40  requires ring : IsCommRing(A, add, zero, neg, mul, one)41  requires memberP : p ∈ polynomials(I, A, zero)42  requires memberQ : q ∈ polynomials(I, A, zero)43  shows polynomialProduct(I, A, add, zero, neg, mul, one, p, q)(monomialOne(I)) = call2(mul, p(monomialOne(I)), q(monomialOne(I)))44proof45  have unit := monomialOne.member at I46  have pair := product.pair at monomialOne(I), monomialOne(I), monomials(I), monomials(I) with *47  have singletonSubset : {(monomialOne(I), monomialOne(I))} ⊆ monomials(I) × monomials(I) by simp48  have supportDomain := convolutionPairs.subset at I, zero, p, q49  have domain : convolutionPairs(I, zero, p, q) ∪ {(monomialOne(I), monomialOne(I))} ⊆ monomials(I) × monomials(I)50    simp51  have finitePairs := convolutionPairs.finite with memberP, memberQ52  have finiteSingleton := Finite.singleton at (monomialOne(I), monomialOne(I))53  have finite := Finite.union with finitePairs, finiteSingleton54  have covers : convolutionPairs(I, zero, p, q) ⊆ convolutionPairs(I, zero, p, q) ∪ {(monomialOne(I), monomialOne(I))}55    simp56  have singleton := singleton.self at (monomialOne(I), monomialOne(I))57  have source : (monomialOne(I), monomialOne(I)) ∈ convolutionPairs(I, zero, p, q) ∪ {(monomialOne(I), monomialOne(I))}58    simp59  have weights := boundedConvolutionWeights.function at I, convolutionPairs(I, zero, p, q) ∪ {(monomialOne(I), monomialOne(I))}, A, add, zero, neg, mul, one, p, q with *60  have imageValue := monomialMul.apply at I, monomialOne(I), monomialOne(I) with *61  unfold call2 at imageValue62  have unitLaw := monomialProduct.one at I, monomialOne(I) with *63  have image : monomialMul(I)((monomialOne(I), monomialOne(I))) = monomialOne(I) by cc64  have unique : ∀ t ∈ convolutionPairs(I, zero, p, q) ∪ {(monomialOne(I), monomialOne(I))}, monomialMul(I)(t) = monomialOne(I) → t = (monomialOne(I), monomialOne(I))65    intros t ht equality66    have included := domain67    have pairMember := included with t, ht68    obtain ⟨bound, m, hm, n, hn, shape⟩ := product.membership.forward with pairMember69    have value := monomialMul.apply at I, m, n with *70    unfold call2 at value71    have productOne : monomialProduct(I, m, n) = monomialOne(I) by cc72    have factors := monomialProduct.one_factors at I, m, n with *73    cc74  have isolated := finitePushforward.unique_fiber at convolutionPairs(I, zero, p, q) ∪ {(monomialOne(I), monomialOne(I))}, monomials(I), A, add, zero, neg, mul, one, monomialMul(I), boundedConvolutionWeights(I, convolutionPairs(I, zero, p, q) ∪ {(monomialOne(I), monomialOne(I))}, A, add, zero, neg, mul, one, p, q), (monomialOne(I), monomialOne(I)), monomialOne(I) with *75  have bounded := polynomialProduct.on_domain with ring, memberP, memberQ, domain, finite, covers76  have coefficient := boundedConvolutionWeights.pair at I, convolutionPairs(I, zero, p, q) ∪ {(monomialOne(I), monomialOne(I))}, A, add, zero, neg, mul, one, p, q, monomialOne(I), monomialOne(I) with *77  cc7879theorem polynomialAtOrigin.constant (I A zero a : Set)80  requires zeroIn : zero ∈ A81  requires coefficient : a ∈ A82  shows polynomialAtOrigin(I, A, zero)(polynomialConstant(I, A, zero, a)) = a83proof84  have member := polynomialConstant.member at I, A, zero, a with *85  have value := polynomialAtOrigin.value at I, A, zero, polynomialConstant(I, A, zero, a) with *86  have coefficientValue := polynomialConstant.coefficient at I, A, zero, a with *87  cc8889theorem polynomialAtOrigin.coefficients (I A zero a : Set)90  requires zeroIn : zero ∈ A91  requires coefficient : a ∈ A92  shows polynomialAtOrigin(I, A, zero)(polynomialCoefficients(I, A, zero)(a)) = a93proof94  have value := polynomialCoefficients.value at I, A, zero, a with *95  rw value96  exact polynomialAtOrigin.constant with *9798theorem polynomialAtOrigin.variable (I A zero one j : Set)99  requires zeroIn : zero ∈ A100  requires oneIn : one ∈ A101  requires index : j ∈ I102  shows polynomialAtOrigin(I, A, zero)(polynomialVariable(I, A, zero, one, j)) = zero103proof104  have member := polynomialVariable.member at I, A, zero, one, j with *105  have unit := monomialOne.member at I106  have different : monomialOne(I) ≠ monomialVariable(I, j)107    intro equal108    have unitValue := monomialOne.value at I, j with *109    have variableValue := monomialVariable.same at I, j with *110    have impossible : (0:Nat) = (1:Nat) by cc111    exact Naturals.disjoint.zero.succ at 0 with impossible112  have coefficient : polynomialVariable(I, A, zero, one, j)(monomialOne(I)) = zero113    unfold polynomialVariable114    exact polynomialTerm.other with *115  have value := polynomialAtOrigin.value at I, A, zero, polynomialVariable(I, A, zero, one, j) with *116  cc117118section Rings119variable (I A add zero neg mul one : Set)120hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)121notation ring R := (A, add, zero, neg, mul, one)122123theorem polynomialAtOrigin.hom124  shows IsRingHom(polynomialAtOrigin(I, A, zero), polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), constantFunction(monomials(I), A, zero), polynomialNeg(I, A, add, zero, neg, mul, one), polynomialMul(I, A, add, zero, neg, mul, one), polynomialConstant(I, A, zero, one), A, add, zero, neg, mul, one)125proof126  have ordinary := IsCommRing.ring with ring127  have zeroIn := IsRing.zero_in_carrier with ordinary128  have multiplicative := IsRing.multiplicative with ordinary129  have oneIn := IsMonoid.unit_in_carrier with multiplicative130  have unit := monomialOne.member at I131  have function := polynomialAtOrigin.function at I, A, zero132  have zeroPolynomial := polynomials.zero at I, A, add, zero, neg, mul, one with *133  have zeroValue := polynomialAtOrigin.value at I, A, zero, constantFunction(monomials(I), A, zero) with *134  have zeroCoefficient := constantFunction.apply at monomials(I), A, monomialOne(I), zero with *135  have preservesZero : polynomialAtOrigin(I, A, zero)(constantFunction(monomials(I), A, zero)) = zero by cc136  have preservesOne := polynomialAtOrigin.constant at I, A, zero, one with *137  have preservesNeg : ∀ p ∈ polynomials(I, A, zero), polynomialAtOrigin(I, A, zero)((polynomialNeg(I, A, add, zero, neg, mul, one))(p)) = -polynomialAtOrigin(I, A, zero)(p)138    intros p hp139    have functionP := polynomials.function with hp140    have negative := polynomials.neg with hp141    have operation := polynomialNeg.apply with hp142    have source := polynomialAtOrigin.value at I, A, zero, coefficientNeg(monomials(I), A, add, zero, neg, mul, one, p) with *143    have coefficient := coefficientNeg.value at monomials(I), A, add, zero, neg, mul, one, p, monomialOne(I) with *144    have value := polynomialAtOrigin.value at I, A, zero, p with *145    cc146  have preservesAdd : ∀ p ∈ polynomials(I, A, zero), ∀ q ∈ polynomials(I, A, zero), polynomialAtOrigin(I, A, zero)((polynomialAdd(I, A, add, zero, neg, mul, one))(p, q)) = polynomialAtOrigin(I, A, zero)(p) + polynomialAtOrigin(I, A, zero)(q)147    intros p hp q hq148    have functionP := polynomials.function with hp149    have functionQ := polynomials.function with hq150    have member := polynomials.add with hp, hq151    have operation := polynomialAdd.apply with hp, hq152    have source := polynomialAtOrigin.value at I, A, zero, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q) with *153    have coefficient := coefficientAdd.value at monomials(I), A, add, zero, neg, mul, one, p, q, monomialOne(I) with *154    have valueP := polynomialAtOrigin.value at I, A, zero, p with *155    have valueQ := polynomialAtOrigin.value at I, A, zero, q with *156    cc157  have preservesMul : ∀ p ∈ polynomials(I, A, zero), ∀ q ∈ polynomials(I, A, zero), polynomialAtOrigin(I, A, zero)((polynomialMul(I, A, add, zero, neg, mul, one))(p, q)) = polynomialAtOrigin(I, A, zero)(p) * polynomialAtOrigin(I, A, zero)(q)158    intros p hp q hq159    have functionP := polynomials.function with hp160    have functionQ := polynomials.function with hq161    have member := polynomialProduct.member with hp, hq162    have operation := polynomialMul.apply with hp, hq163    have source := polynomialAtOrigin.value at I, A, zero, polynomialProduct(I, A, add, zero, neg, mul, one, p, q) with *164    have coefficient := polynomialProduct.constant_coefficient with hp, hq165    have valueP := polynomialAtOrigin.value at I, A, zero, p with *166    have valueQ := polynomialAtOrigin.value at I, A, zero, q with *167    cc168  unfold IsRingHom169  refine ⟨function, preservesZero, preservesOne, preservesNeg, preservesAdd, preservesMul⟩170171theorem polynomialAtOrigin.kernel_ideal172  shows IsIdeal(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), constantFunction(monomials(I), A, zero), polynomialNeg(I, A, add, zero, neg, mul, one), polynomialMul(I, A, add, zero, neg, mul, one), ringKernel(polynomialAtOrigin(I, A, zero), polynomials(I, A, zero), zero))173proof174  have source := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *175  have hom := polynomialAtOrigin.hom at I, A, add, zero, neg, mul, one with *176  exact IsRingHom.kernel_ideal with source, ring, hom177178end Rings179180theorem polynomialAtOrigin.surjective (I A zero : Set)181  requires zeroIn : zero ∈ A182  shows SurjectiveBetween(polynomialAtOrigin(I, A, zero), polynomials(I, A, zero), A)183proof184  have function := polynomialAtOrigin.function at I, A, zero185  constructor186  . exact function187  . intros a ha188    have member := polynomialConstant.member at I, A, zero, a with *189    have value := polynomialAtOrigin.constant at I, A, zero, a with *190    have edge := FunctionBetween.relates_apply with *191    refine ⟨polynomialConstant(I, A, zero, a), member, _⟩192    rwa value at edge193194theorem polynomialAtOrigin.kernel_membership (I A zero p : Set)195  shows p ∈ ringKernel(polynomialAtOrigin(I, A, zero), polynomials(I, A, zero), zero) ↔ p ∈ polynomials(I, A, zero) ∧ p(monomialOne(I)) = zero196proof197  constructor198  . intro member199    have data := ringKernel.membership.forward with member200    have value := polynomialAtOrigin.value at I, A, zero, p with *201    constructor202    . exact data.left203    . cc204  . intro data205    have value := polynomialAtOrigin.value at I, A, zero, p with *206    apply ringKernel.membership.backward207    constructor208    . exact data.left209    . cc210211section Quotient212variable (I A add zero neg mul one : Set)213hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)214215theorem polynomialAtOrigin.quotient_iso216  shows IsRingIso(quotientMap(polynomialAtOrigin(I, A, zero), polynomials(I, A, zero), A, idealRelation(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), polynomialNeg(I, A, add, zero, neg, mul, one), ringKernel(polynomialAtOrigin(I, A, zero), polynomials(I, A, zero), zero))),217    (polynomials(I, A, zero) ⧸ idealRelation(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), polynomialNeg(I, A, add, zero, neg, mul, one), ringKernel(polynomialAtOrigin(I, A, zero), polynomials(I, A, zero), zero))),218    quotientBinary(polynomials(I, A, zero), idealRelation(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), polynomialNeg(I, A, add, zero, neg, mul, one), ringKernel(polynomialAtOrigin(I, A, zero), polynomials(I, A, zero), zero)), polynomialAdd(I, A, add, zero, neg, mul, one)), ⟦constantFunction(monomials(I), A, zero)⟧[polynomials(I, A, zero), idealRelation(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), polynomialNeg(I, A, add, zero, neg, mul, one), ringKernel(polynomialAtOrigin(I, A, zero), polynomials(I, A, zero), zero))],219    quotientUnary(polynomials(I, A, zero), idealRelation(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), polynomialNeg(I, A, add, zero, neg, mul, one), ringKernel(polynomialAtOrigin(I, A, zero), polynomials(I, A, zero), zero)), polynomialNeg(I, A, add, zero, neg, mul, one)), quotientBinary(polynomials(I, A, zero), idealRelation(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), polynomialNeg(I, A, add, zero, neg, mul, one), ringKernel(polynomialAtOrigin(I, A, zero), polynomials(I, A, zero), zero)), polynomialMul(I, A, add, zero, neg, mul, one)), ⟦polynomialConstant(I, A, zero, one)⟧[polynomials(I, A, zero), idealRelation(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), polynomialNeg(I, A, add, zero, neg, mul, one), ringKernel(polynomialAtOrigin(I, A, zero), polynomials(I, A, zero), zero))],220    A, add, zero, neg, mul, one)221proof222  have ordinary := IsCommRing.ring with ring223  have zeroIn := IsRing.zero_in_carrier with ordinary224  have source := polynomials.comm_ring at I, A, add, zero, neg, mul, one with *225  have hom := polynomialAtOrigin.hom at I, A, add, zero, neg, mul, one with *226  have onto := polynomialAtOrigin.surjective at I, A, zero with *227  exact idealQuotient.first_isomorphism with source, ring, hom, onto228229end Quotient230