# mathlibdocumentation

data.polynomial.module

# 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.

@[protected, instance]
def polynomial_module.inhabited (R : Type u_1) (M : Type u_2) [comm_ring R] [ M] :
@[nolint]
def polynomial_module (R : Type u_1) (M : Type u_2) [comm_ring R] [ M] :
Type u_2

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 on polynomial_module R R[X]
• R[X] acts on polynomial_module R R[X] as R[Y] acting on R[X][Y]
• R acts on polynomial_module R[X] R[X]
• R[X] acts on polynomial_module R[X] R[X] as R[X] acting on R[X][Y]
• R[X][X] acts on polynomial_module R[X] R[X] as R[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
Instances for polynomial_module
@[protected, instance]
noncomputable def polynomial_module.add_comm_group (R : Type u_1) (M : Type u_2) [comm_ring R] [ M] :
@[protected, nolint, instance]
noncomputable def polynomial_module.module (R : Type u_1) {M : Type u_2} [comm_ring R] [ M] {S : Type u_3} [ R] [ M] [ M] :
M)

This is required to have the is_scalar_tower S R M instance to avoid diamonds.

Equations
@[protected, instance]
def polynomial_module.has_coe_to_fun (R : Type u_1) {M : Type u_2} [comm_ring R] [ M] :
(λ (_x : , → M)
Equations
noncomputable def polynomial_module.single (R : Type u_1) {M : Type u_2} [comm_ring R] [ M] (i : ) :
M →+

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
theorem polynomial_module.single_apply (R : Type u_1) {M : Type u_2} [comm_ring R] [ M] (i : ) (m : M) (n : ) :
( m) n = ite (i = n) m 0
noncomputable def polynomial_module.lsingle (R : Type u_1) {M : Type u_2} [comm_ring R] [ M] (i : ) :

polynomial_module.single as a linear map.

Equations
theorem polynomial_module.lsingle_apply (R : Type u_1) {M : Type u_2} [comm_ring R] [ M] (i : ) (m : M) (n : ) :
( m) n = ite (i = n) m 0
theorem polynomial_module.single_smul (R : Type u_1) {M : Type u_2} [comm_ring R] [ M] (i : ) (r : R) (m : M) :
(r m) = r m
theorem polynomial_module.induction_linear {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] {P : → Prop} (f : M) (h0 : P 0) (hadd : ∀ (f g : , P fP gP (f + g)) (hsingle : ∀ (a : ) (b : M), P ( b)) :
P f
@[protected, instance]
noncomputable def polynomial_module.polynomial_module {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] :
Equations
@[protected, instance]
def polynomial_module.is_scalar_tower {R : Type u_1} [comm_ring R] {S : Type u_3} [ R] (M : Type u) [ M] [ M] [ M] :
M)
@[protected, instance]
def polynomial_module.is_scalar_tower' {R : Type u_1} [comm_ring R] {S : Type u_3} [ R] (M : Type u) [ M] [ M] [ M] :
M)
@[simp]
theorem polynomial_module.monomial_smul_single {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (i : ) (r : R) (j : ) (m : M) :
r m = (i + j)) (r m)
@[simp]
theorem polynomial_module.monomial_smul_apply {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (i : ) (r : R) (g : M) (n : ) :
( r g) n = ite (i n) (r g (n - i)) 0
@[simp]
theorem polynomial_module.smul_single_apply {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (i : ) (f : polynomial R) (m : M) (n : ) :
(f m) n = ite (i n) (f.coeff (n - i) m) 0
theorem polynomial_module.smul_apply {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (f : polynomial R) (g : M) (n : ) :
(f g) n = (λ (x : × ), f.coeff x.fst g x.snd)
noncomputable def polynomial_module.equiv_polynomial_self {R : Type u_1} [comm_ring R] :

polynomial R R is isomorphic to R[X] as an R[X] module.

Equations
noncomputable def polynomial_module.equiv_polynomial {R : Type u_1} [comm_ring R] {S : Type u_2} [comm_ring S] [ S] :

polynomial R S is isomorphic to S[X] as an R module.

Equations
noncomputable def polynomial_module.map {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (R' : Type u_4) {M' : Type u_5} [comm_ring R'] [add_comm_group M'] [module R' M'] [ R'] [ M'] [ R' M'] (f : M →ₗ[R] M') :

The image of a polynomial under a linear map.

Equations
@[simp]
theorem polynomial_module.map_single {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (R' : Type u_4) {M' : Type u_5} [comm_ring R'] [add_comm_group M'] [module R' M'] [ R'] [ M'] [ R' M'] (f : M →ₗ[R] M') (i : ) (m : M) :
f) ( m) = i) (f m)
theorem polynomial_module.map_smul {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (R' : Type u_4) {M' : Type u_5} [comm_ring R'] [add_comm_group M'] [module R' M'] [ R'] [ M'] [ R' M'] (f : M →ₗ[R] M') (p : polynomial R) (q : M) :
f) (p q) = polynomial.map R') p f) q
def polynomial_module.eval {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (r : R) :

Evaulate a polynomial p : polynomial_module R M at r : R.

Equations
theorem polynomial_module.eval_apply {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (r : R) (p : M) :
= (λ (i : ) (m : M), r ^ i m)
@[simp]
theorem polynomial_module.eval_single {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (r : R) (i : ) (m : M) :
( m) = r ^ i m
theorem polynomial_module.eval_smul {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (p : polynomial R) (q : M) (r : R) :
(p q) =
@[simp]
theorem polynomial_module.eval_map {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (R' : Type u_4) {M' : Type u_5} [comm_ring R'] [add_comm_group M'] [module R' M'] [ R'] [ M'] [ R' M'] (f : M →ₗ[R] M') (q : M) (r : R) :
(polynomial_module.eval ( R') r)) ( f) q) = f q)
@[simp]
theorem polynomial_module.eval_map' {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (f : M →ₗ[R] M) (q : M) (r : R) :
( q) = f q)
@[simp]
theorem polynomial_module.comp_apply {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (p : polynomial R) (ᾰ : M) :
= ( ᾰ)
noncomputable def polynomial_module.comp {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (p : polynomial R) :

comp p q is the composition of p : R[X] and q : M[X] as q(p(x)).

Equations
theorem polynomial_module.comp_single {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (p : polynomial R) (i : ) (m : M) :
( m) = p ^ i m
theorem polynomial_module.comp_eval {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (p : polynomial R) (q : M) (r : R) :
q) = q
theorem polynomial_module.comp_smul {R : Type u_1} {M : Type u_2} [comm_ring R] [ M] (p p' : polynomial R) (q : M) :
(p' q) = p'.comp p