[Merged by Bors] - feat(Algebra/Polynomial/Derivation): coefficient-wise derivation on a polynomial#14702
[Merged by Bors] - feat(Algebra/Polynomial/Derivation): coefficient-wise derivation on a polynomial#14702Command-Master wants to merge 31 commits intomasterfrom
Conversation
PR summary 9deed4ebc9Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
There was a problem hiding this comment.
/--
The `R`-derivation from `A[X]` to `M[X]` which applies the derivative to each
of the coefficients.
-/
def coeffwise : Derivation R A[X] (PolynomialModule A M) where
__ := (PolynomialModule.map A d.toLinearMap).comp
PolynomialModule.equivPolynomial.symm.toLinearMap
map_one_eq_zero' := show (Finsupp.single 0 1).mapRange (d : A → M) d.map_zero = 0 by simp
leibniz' p q := by
dsimp
induction p using Polynomial.induction_on' with
| h_add => simp only [add_mul, map_add, add_smul, smul_add, add_add_add_comm, *]
| h_monomial n a =>
induction q using Polynomial.induction_on' with
| h_add => simp only [mul_add, map_add, add_smul, smul_add, add_add_add_comm, *]
| h_monomial m b =>
refine Finsupp.ext fun i ↦ ?_
dsimp [PolynomialModule.equivPolynomial, PolynomialModule.map]
simp only [toFinsupp_mul, toFinsupp_monomial, AddMonoidAlgebra.single_mul_single]
show d _ = _ + _
erw [Finsupp.mapRange.linearMap_apply, Finsupp.mapRange.linearMap_apply]
rw [Finsupp.mapRange_single, Finsupp.mapRange_single]
erw [PolynomialModule.monomial_smul_single, PolynomialModule.monomial_smul_single]
simp only [AddMonoidAlgebra.single_apply, apply_ite d, leibniz, map_zero, coeFn_coe,
PolynomialModule.single_apply, ite_add_zero, add_comm m n]
@[simp]
lemma coeffwise_apply (p : A[X]) (i) :
d.coeffwise p i = d (coeff p i) := rfl
@[simp]
lemma coeffwise_monomial (n) (x : A) :
d.coeffwise (monomial n x) = .single A n (d x) := Finsupp.ext fun _ ↦ by
simp [coeff_monomial, apply_ite d, PolynomialModule.single_apply]
@[simp]
lemma coeffwise_X :
d.coeffwise (X : A[X]) = 0 := Finsupp.ext fun _ ↦ by
simp [← monomial_one_one_eq_X]
theorem apply_eval_eq (x : A) (p : A[X]) :
d (eval x p) = PolynomialModule.eval x (d.coeffwise p) + eval x (derivative p) • d x := by
induction p using Polynomial.induction_on' with
| h_add => simp_all only [eval_add, map_add, add_smul]; abel
| h_monomial n a =>
simp only [eval_monomial, leibniz, leibniz_pow, coeffwise_monomial,
PolynomialModule.eval_single, derivative_monomial, ← mul_smul, nsmul_eq_smul_cast A]
rw [add_comm]
congr 2
ringThis seems like a better approach. Note that you would need to relax the typeclass arguments on PolynomialModule.map to make this work.
By the way it would be nice if you can identify the missing lemmas and remove those erws.
|
How could the typeclass parameters of |
|
You're right. Then that's the thing to do if you really care about semirings. |
|
I added the lemmas. I'm not sure about changing the definition - it makes |
|
I don't think that matters much, unless you absolutely need semirings. Someone else who needs semirings may generalise |
Co-authored-by: erdOne <36414270+erdOne@users.noreply.github.com>
|
This PR/issue depends on: |
| The `R`-derivation from `A[X]` to `M[X]` which applies the derivative to each | ||
| of the coefficients. | ||
| -/ | ||
| def mapCoeffs : Derivation R A[X] (PolynomialModule A M) where |
There was a problem hiding this comment.
This name is ambiguous in that one could also derive the a multivariate polynomial coefficient-wise. What about something like this?
| def mapCoeffs : Derivation R A[X] (PolynomialModule A M) where | |
| def polynomialCoeffs : Derivation R A[X] (PolynomialModule A M) where |
There was a problem hiding this comment.
Should I also change the file name, or is it ok?
There was a problem hiding this comment.
Thinking about it a bit more, I don't love polynomialCoeffs - it feels weird to write D.polynomialCoeffs p
There was a problem hiding this comment.
I would personally just call it Derivation.Polynomial, but I don't know 🤷
There was a problem hiding this comment.
Perhaps just Derivation.poly? Or is that too confusing?
There was a problem hiding this comment.
Oh I see. I guess it can go back there
There was a problem hiding this comment.
@semorrison @erdOne could we get your opinions on this?
There was a problem hiding this comment.
In #14967 I also import RingTheory.Derivation.DifferentialRing to this file, so I think it's good to keep as a separate file
There was a problem hiding this comment.
How bad do you think this name is? I'm unable to think of any alternative I like
There was a problem hiding this comment.
I guess it's fine, but let's not resolve this conversation in case someone thinks of a better name
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
|
Thanks! bors merge |
… polynomial (#14702) Define `Derivation.coeffwise`, which applies the derivation to the a polynomial coefficient-wise.
|
Build failed:
|
|
bors merge |
|
🔒 Permission denied Existing reviewers: click here to make Command-Master a reviewer |
|
maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde. |
|
bors merge |
… polynomial (#14702) Define `Derivation.coeffwise`, which applies the derivation to the a polynomial coefficient-wise.
|
Pull request successfully merged into master. Build succeeded: |
Define
Derivation.coeffwise, which applies the derivation to the a polynomial coefficient-wise.Finsuppsmul lemmas to polynomials #14701