[Merged by Bors] - feat: derivations of (univariate) polynomials#6023
[Merged by Bors] - feat: derivations of (univariate) polynomials#6023
Conversation
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
| map_one_eq_zero' := derivative_one | ||
| leibniz' f g := by simp [mul_comm, add_comm, derivative_mul] | ||
|
|
||
| variable [AddCommMonoid A] [Module R A] [Module (Polynomial R) A] |
There was a problem hiding this comment.
Indexing a typeclass on a non-carrier type will eventually cause pain.
For example, we might one day have another ring S with R ≃+* S and wish to use some result which includes the term Module (Polynomial R) A in a proof that discusses Module (Polynomial S) A.
I wonder could we avoid doing this by introducing a PolynomialAlgebra typeclass along the lines of:
class PolynomialAlgebra (R P : Type _) [CommSemiring R] [Semiring P] extends Algebra R P :=
(X : P)
-- TODO add axioms that are equivalent to the map that sends `Polynomial.X` to `PolynomialAlgebra.X` extending to a full algebra equivalence: `R[X] ≃ₐ[R] P`Alternatively we could introduce a typeclass for this specific situation since we know a module over R[X] is "the same as" a module over R together with an R-linear endomorphism (scalar action of X):
class PolynomialModule (R M : Type _) [Semiring R] [AddCommMonoid M] extends Module R M :=
(X : M →ₗ[R] M)There was a problem hiding this comment.
Note that @kbuzzard is just copying what we already did for MvPolynomial in this PR, not that that invalidates your comment.
There was a problem hiding this comment.
Good point, I think we can live with this for now but I predict one day we'll want something like PolynomialAlgebra or PolynomialModule.
|
bors merge |
An R-derivation from `R[X]` is determined by its value on `X`. Joint work with Richard Hill, who needs this stuff for his work on power series. We followed `MvPolynomial.Derivation` . Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Oliver Nash <github@olivernash.org>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
An R-derivation from `R[X]` is determined by its value on `X`. Joint work with Richard Hill, who needs this stuff for his work on power series. We followed `MvPolynomial.Derivation` . Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Oliver Nash <github@olivernash.org>
An R-derivation from `R[X]` is determined by its value on `X`. Joint work with Richard Hill, who needs this stuff for his work on power series. We followed `MvPolynomial.Derivation` . Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Oliver Nash <github@olivernash.org>
An R-derivation from `R[X]` is determined by its value on `X`. Joint work with Richard Hill, who needs this stuff for his work on power series. We followed `MvPolynomial.Derivation` . Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Oliver Nash <github@olivernash.org>
An R-derivation from
R[X]is determined by its value onX. Joint work with Richard Hill, who needs this stuff for his work on power series. We followedMvPolynomial.Derivation.