Grace/Cumulus/Algebra/Polynomial/CoefficientMap.g17

Open in Workbench Download source

Imports

Constants · Terms

Declarations

Source

1-- Mapping sparse polynomial coefficients through a ring homomorphism (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.CoefficientMap8import Constants9import Terms1011theorem polynomials.compose (I A z B o f p : Set)12  requires function : f : A → B13  requires zero : f(z) = o14  requires polynomial : p ∈ polynomials(I, A, z)15  shows compose(f, p, monomials(I), A, B) ∈ polynomials(I, B, o)16proof17  have values := polynomials.function with polynomial18  have mapped := compose.function with values, function19  have finite := polynomials.finite_support with polynomial20  have subset : functionSupport(compose(f, p, monomials(I), A, B), monomials(I), o) ⊆ functionSupport(p, monomials(I), z)21    intros m member22    obtain ⟨monomial, nonzero⟩ := functionSupport.membership.forward with member23    have value := compose.apply at f, p, monomials(I), A, B, m with *24    apply functionSupport.membership.backward25    refine ⟨monomial, ?_⟩26    intro vanishes27    apply nonzero28    cc29  have support := Finite.subset with finite, subset30  have map : CoefficientMap(compose(f, p, monomials(I), A, B), monomials(I), B, o)31    unfold CoefficientMap32    refine ⟨mapped, support⟩33  exact polynomials.contains with *3435defgraph polynomialMap (I A z B o f : Set) (p ∈ polynomials(I, A, z)) : polynomials(I, B, o) := compose(f, p, monomials(I), A, B)36requires function : f : A → B37requires zero : f(z) = o38proof39  exact polynomials.compose with *4041notation scoped polynomialMap(I, R, S, f) => polynomialMap(I, R.carrier, R.zero, S.carrier, S.zero, f)4243theorem polynomialMap.coefficient (I A z B o f p m : Set)44  requires function : f : A → B45  requires zero : f(z) = o46  requires polynomial : p ∈ polynomials(I, A, z)47  requires monomial : m ∈ monomials(I)48  shows polynomialMap(I, A, z, B, o, f)(p)(m) = f(p(m))49proof50  have values := polynomials.function with polynomial51  have mapped := polynomialMap.value at I, A, z, B, o, f, p with *52  have value := compose.apply at f, p, monomials(I), A, B, m with *53  cc5455theorem polynomialMap.member (I A z B o f p : Set)56  requires function : f : A → B57  requires zero : f(z) = o58  requires polynomial : p ∈ polynomials(I, A, z)59  shows polynomialMap(I, A, z, B, o, f)(p) ∈ polynomials(I, B, o)60proof61  have map := polynomialMap.function at I, A, z, B, o, f with *62  exact FunctionBetween.apply_closed with *6364section Rings65variable (I A add z neg mul one B plus o minus times unit f : Set)66notation ring R := (A, add, z, neg, mul, one)67notation ring S := (B, plus, o, minus, times, unit)68notation ring P := R[I]69notation ring Q := S[I]70hypothesis source : IsCommRing(R)71hypothesis target : IsCommRing(S)72hypothesis hom : IsRingHom(f, R, S)7374theorem polynomialMap.add (p q : Set)75  requires left : p ∈ P76  requires right : q ∈ P77  shows polynomialMap(I, A, z, B, o, f)(P[p + q]) = Q[polynomialMap(I, A, z, B, o, f)(p) + polynomialMap(I, A, z, B, o, f)(q)]78proof79  have function := IsRingHom.function with hom80  have zero := IsRingHom.zero with hom81  have sourceRing := polynomials.comm_ring at I, A, add, z, neg, mul, one with *82  have targetRing := polynomials.comm_ring at I, B, plus, o, minus, times, unit with *83  have sourceOrdinary := IsCommRing.ring with sourceRing84  have targetOrdinary := IsCommRing.ring with targetRing85  have sum := IsRing.add_closed with sourceOrdinary, left, right86  have mappedSum := polynomialMap.member at I, A, z, B, o, f, P[p + q] with *87  have mappedLeft := polynomialMap.member at I, A, z, B, o, f, p with *88  have mappedRight := polynomialMap.member at I, A, z, B, o, f, q with *89  have targetSum := IsRing.add_closed with targetOrdinary, mappedLeft,90    mappedRight91  have sourceValue := polynomialAdd.apply at I, A, add, z, neg, mul, one, p, q with *92  have targetValue := polynomialAdd.apply at I, B, plus, o, minus, times, unit, polynomialMap(I, A, z, B, o, f)(p), polynomialMap(I, A, z, B, o, f)(q) with *93  have pFunction := polynomials.function with left94  have qFunction := polynomials.function with right95  have fpFunction := polynomials.function with mappedLeft96  have fqFunction := polynomials.function with mappedRight97  apply polynomials.ext with mappedSum, targetSum98  intros m monomial99  have pIn := polynomials.coefficient at I, A, z, p, m with *100  have qIn := polynomials.coefficient at I, A, z, q, m with *101  have sumCoefficient := polynomialMap.coefficient at I, A, z, B, o, f, P[p + q], m with *102  have pCoefficient := polynomialMap.coefficient at I, A, z, B, o, f, p, m with *103  have qCoefficient := polynomialMap.coefficient at I, A, z, B, o, f, q, m with *104  have sourceCoefficient := coefficientAdd.value at monomials(I), A, add, z, neg, mul, one, p, q, m with *105  have targetCoefficient := coefficientAdd.value at monomials(I), B, plus, o, minus, times, unit, polynomialMap(I, A, z, B, o, f)(p), polynomialMap(I, A, z, B, o, f)(q), m with *106  have preserved := IsRingHom.add with hom, pIn, qIn107  cc108109theorem polynomialMap.coefficient_add (p q : Set)110  requires left : p ∈ P111  requires right : q ∈ P112  shows polynomialMap(I, R, S, f)(coefficientAdd(monomials(I), A, add, z, neg, mul, one, p, q)) = coefficientAdd(monomials(I), B, plus, o, minus, times, unit, polynomialMap(I, R, S, f)(p), polynomialMap(I, R, S, f)(q))113proof114  have function := IsRingHom.function with hom115  have zero := IsRingHom.zero with hom116  have mappedLeft := polynomialMap.member at I, A, z, B, o, f, p with *117  have mappedRight := polynomialMap.member at I, A, z, B, o, f, q with *118  have first := polynomialAdd.apply at I, A, add, z, neg, mul, one, p, q with *119  have second := polynomialAdd.apply at I, B, plus, o, minus, times, unit, polynomialMap(I, R, S, f)(p), polynomialMap(I, R, S, f)(q) with *120  have value := polynomialMap.add at I, A, add, z, neg, mul, one, B, plus, o, minus, times, unit, f, p, q with *121  cc122123theorem polynomialMap.zero124  shows polynomialMap(I, A, z, B, o, f)(P[0]) = Q[0]125proof126  have function := IsRingHom.function with hom127  have zero := IsRingHom.zero with hom128  have sourceMember := polynomials.zero at I, A, add, z, neg, mul, one with *129  have targetMember := polynomials.zero at I, B, plus, o, minus, times, unit with *130  have mapped := polynomialMap.member with *131  have zeroIn : R[0] ∈ R by typecheck132  have targetZero : S[0] ∈ S by typecheck133  apply polynomials.ext with mapped, targetMember134  intros m monomial135  have coefficient := polynomialMap.coefficient with *136  have left := constantFunction.apply at monomials(I), A, m, z with *137  have right := constantFunction.apply at monomials(I), B, m, o with *138  cc139140theorem polynomialMap.term (a m : Set)141  requires coefficient : a ∈ R142  requires monomial : m ∈ monomials(I)143  shows polynomialMap(I, A, z, B, o, f)(polynomialTerm(I, A, z, a, m)) = polynomialTerm(I, B, o, f(a), m)144proof145  have function := IsRingHom.function with hom146  have zero := IsRingHom.zero with hom147  have zeroIn : R[0] ∈ R by typecheck148  have targetZero : S[0] ∈ S by typecheck149  have image := IsRingHom.closed with hom, coefficient150  have term := polynomialTerm.member at I, A, z, a, m with *151  have targetTerm := polynomialTerm.member at I, B, o, f(a), m with *152  have mapped := polynomialMap.member at I, A, z, B, o, f, polynomialTerm(I, A, z, a, m) with *153  apply polynomials.ext with mapped, targetTerm154  intros n hn155  have value := polynomialMap.coefficient at I, A, z, B, o, f, polynomialTerm(I, A, z, a, m), n with *156  have alternatives : n = m ∨ n ≠ m by tauto157  cases alternatives with same | different158  . rw same159    have left := polynomialTerm.same at I, A, z, a, m with *160    have right := polynomialTerm.same at I, B, o, f(a), m with *161    rw same at value162    cc163  . have left := polynomialTerm.other at I, A, z, a, m, n with *164    have right := polynomialTerm.other at I, B, o, f(a), m, n with *165    cc166167theorem polynomialMap.constant (a : Set)168  requires coefficient : a ∈ R169  shows polynomialMap(I, A, z, B, o, f)(polynomialConstant(I, A, z, a)) = polynomialConstant(I, B, o, f(a))170proof171  have monomial := monomialOne.member at I172  have value := polynomialMap.term with *173  unfold polynomialConstant174  cc175176theorem polynomialMap.variable (j : Set)177  shows polynomialMap(I, A, z, B, o, f)(polynomialVariable(I, A, z, one, j)) = polynomialVariable(I, B, o, unit, j)178proof179  have coefficient : R[1] ∈ R by typecheck180  have monomial := monomialVariable.member at I, j181  have value := polynomialMap.term with *182  have oneValue := IsRingHom.one with hom183  unfold polynomialVariable184  cc185186end Rings187