Polynomial module #
In this file, we define the polynomial module for an R
-module M
, i.e. the R[X]
-module M[X]
.
This is defined as an type alias polynomial_module R M := ℕ →₀ M
, since there might be different
module structures on ℕ →₀ M
of interest. See the docstring of polynomial_module
for details.
The R[X]
-module M[X]
for an R
-module M
.
This is isomorphic (as an R
-module) to polynomial M
when M
is a ring.
We require all the module instances module S (polynomial_module R M)
to factor through R
except
module R[X] (polynomial_module R M)
.
In this constraint, we have the following instances for example :
R
acts onpolynomial_module R R[X]
R[X]
acts onpolynomial_module R R[X]
asR[Y]
acting onR[X][Y]
R
acts onpolynomial_module R[X] R[X]
R[X]
acts onpolynomial_module R[X] R[X]
asR[X]
acting onR[X][Y]
R[X][X]
acts onpolynomial_module R[X] R[X]
asR[X][Y]
acting on itself
This is also the reason why R
is included in the alias, or else there will be two different
instances of module R[X] (polynomial_module R[X])
.
See https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2315065.20polynomial.20modules for the full discussion.
Equations
- polynomial_module R M = (ℕ →₀ M)
This is required to have the is_scalar_tower S R M
instance to avoid diamonds.
Equations
Equations
The monomial m * x ^ i
. This is defeq to finsupp.single_add_hom
, and is redefined here
so that it has the desired type signature.
Equations
polynomial_module.single
as a linear map.
Equations
polynomial R R
is isomorphic to R[X]
as an R[X]
module.
Equations
- polynomial_module.equiv_polynomial_self = {to_fun := (polynomial.to_finsupp_iso R).symm.to_fun, map_add' := _, map_smul' := _, inv_fun := (polynomial.to_finsupp_iso R).symm.inv_fun, left_inv := _, right_inv := _}
polynomial R S
is isomorphic to S[X]
as an R
module.
Equations
- polynomial_module.equiv_polynomial = {to_fun := (polynomial.to_finsupp_iso S).symm.to_fun, map_add' := _, map_smul' := _, inv_fun := (polynomial.to_finsupp_iso S).symm.inv_fun, left_inv := _, right_inv := _}
The image of a polynomial under a linear map.
Equations
Evaulate a polynomial p : polynomial_module R M
at r : R
.
Equations
- polynomial_module.eval r = {to_fun := λ (p : polynomial_module R M), finsupp.sum p (λ (i : ℕ) (m : M), r ^ i • m), map_add' := _, map_smul' := _}
comp p q
is the composition of p : R[X]
and q : M[X]
as q(p(x))
.