# Documentation

Mathlib.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 a type alias PolynomialModule R M := ℕ →₀ M, since there might be different module structures on ℕ →₀ M of interest. See the docstring of PolynomialModule for details.

def PolynomialModule (R : Type u_1) (M : Type u_2) [] [] [Module R M] :
Type u_2

The R[X]-module M[X] for an R-module M. This is isomorphic (as an R-module) to M[X] when M is a ring.

We require all the module instances Module S (PolynomialModule R M) to factor through R except Module R[X] (PolynomialModule R M). In this constraint, we have the following instances for example :

• R acts on PolynomialModule R R[X]
• R[X] acts on PolynomialModule R R[X] as R[Y] acting on R[X][Y]
• R acts on PolynomialModule R[X] R[X]
• R[X] acts on PolynomialModule R[X] R[X] as R[X] acting on R[X][Y]
• R[X][X] acts on PolynomialModule 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] (PolynomialModule R[X]).

See https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2315065.20polynomial.20modules for the full discussion.

Instances For
noncomputable instance instInhabitedPolynomialModule (R : Type u_1) (M : Type u_2) [] [] [Module R M] :
noncomputable instance instAddCommGroupPolynomialModule (R : Type u_1) (M : Type u_2) [] [] [Module R M] :

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

instance PolynomialModule.funLike (R : Type u_1) {M : Type u_2} [] [] [Module R M] :
FunLike () fun x => M
instance PolynomialModule.instCoeFunPolynomialModuleForAllNat (R : Type u_1) {M : Type u_2} [] [] [Module R M] :
CoeFun () fun x => M
theorem PolynomialModule.zero_apply (R : Type u_1) {M : Type u_2} [] [] [Module R M] (i : ) :
0 i = 0
theorem PolynomialModule.add_apply (R : Type u_1) {M : Type u_2} [] [] [Module R M] (g₁ : ) (g₂ : ) (a : ) :
↑(g₁ + g₂) a = g₁ a + g₂ a
noncomputable def PolynomialModule.single (R : Type u_1) {M : Type u_2} [] [] [Module R M] (i : ) :
M →+

The monomial m * x ^ i. This is defeq to Finsupp.singleAddHom, and is redefined here so that it has the desired type signature.

Instances For
theorem PolynomialModule.single_apply (R : Type u_1) {M : Type u_2} [] [] [Module R M] (i : ) (m : M) (n : ) :
↑(↑() m) n = if i = n then m else 0
noncomputable def PolynomialModule.lsingle (R : Type u_1) {M : Type u_2} [] [] [Module R M] (i : ) :

PolynomialModule.single as a linear map.

Instances For
theorem PolynomialModule.lsingle_apply (R : Type u_1) {M : Type u_2} [] [] [Module R M] (i : ) (m : M) (n : ) :
↑(↑() m) n = if i = n then m else 0
theorem PolynomialModule.single_smul (R : Type u_1) {M : Type u_2} [] [] [Module R M] (i : ) (r : R) (m : M) :
↑() (r m) = r ↑() m
theorem PolynomialModule.induction_linear {R : Type u_1} {M : Type u_2} [] [] [Module R M] {P : Prop} (f : ) (h0 : P 0) (hadd : (f g : ) → P fP gP (f + g)) (hsingle : (a : ) → (b : M) → P (↑() b)) :
P f
@[semireducible]
noncomputable instance PolynomialModule.polynomialModule {R : Type u_1} {M : Type u_2} [] [] [Module R M] :
Module () ()
instance PolynomialModule.isScalarTower' {R : Type u_1} [] {S : Type u_3} [] [Algebra S R] (M : Type u) [] [Module R M] [Module S M] [] :
@[simp]
theorem PolynomialModule.monomial_smul_single {R : Type u_1} {M : Type u_2} [] [] [Module R M] (i : ) (r : R) (j : ) (m : M) :
↑() r ↑() m = ↑(PolynomialModule.single R (i + j)) (r m)
@[simp]
theorem PolynomialModule.monomial_smul_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] (i : ) (r : R) (g : ) (n : ) :
↑(↑() r g) n = if i n then r g (n - i) else 0
@[simp]
theorem PolynomialModule.smul_single_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] (i : ) (f : ) (m : M) (n : ) :
↑(f ↑() m) n = if i n then Polynomial.coeff f (n - i) m else 0
theorem PolynomialModule.smul_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] (f : ) (g : ) (n : ) :
↑(f g) n = Finset.sum () fun x => Polynomial.coeff f x.fst g x.snd
noncomputable def PolynomialModule.equivPolynomialSelf {R : Type u_1} [] :

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

Instances For
noncomputable def PolynomialModule.equivPolynomial {R : Type u_1} [] {S : Type u_4} [] [Algebra R S] :

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

Instances For
noncomputable def PolynomialModule.map {R : Type u_1} {M : Type u_2} [] [] [Module R M] (R' : Type u_4) {M' : Type u_5} [CommRing R'] [] [Module R' M'] [Module R M'] (f : M →ₗ[R] M') :

The image of a polynomial under a linear map.

Instances For
@[simp]
theorem PolynomialModule.map_single {R : Type u_1} {M : Type u_2} [] [] [Module R M] (R' : Type u_4) {M' : Type u_5} [CommRing R'] [] [Module R' M'] [Module R M'] (f : M →ₗ[R] M') (i : ) (m : M) :
↑() (↑() m) = ↑() (f m)
theorem PolynomialModule.map_smul {R : Type u_1} {M : Type u_2} [] [] [Module R M] (R' : Type u_4) {M' : Type u_5} [CommRing R'] [] [Module R' M'] [Algebra R R'] [Module R M'] [IsScalarTower R R' M'] (f : M →ₗ[R] M') (p : ) (q : ) :
↑() (p q) = Polynomial.map (algebraMap R R') p ↑() q
theorem PolynomialModule.eval_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] (r : R) (p : ) :
↑() p = Finsupp.sum p fun i m => r ^ i m
def PolynomialModule.eval {R : Type u_1} {M : Type u_2} [] [] [Module R M] (r : R) :

Evaluate a polynomial p : PolynomialModule R M at r : R.

Instances For
@[simp]
theorem PolynomialModule.eval_single {R : Type u_1} {M : Type u_2} [] [] [Module R M] (r : R) (i : ) (m : M) :
↑() (↑() m) = r ^ i m
@[simp]
theorem PolynomialModule.eval_lsingle {R : Type u_1} {M : Type u_2} [] [] [Module R M] (r : R) (i : ) (m : M) :
↑() (↑() m) = r ^ i m
theorem PolynomialModule.eval_smul {R : Type u_1} {M : Type u_2} [] [] [Module R M] (p : ) (q : ) (r : R) :
↑() (p q) = ↑() q
@[simp]
theorem PolynomialModule.eval_map {R : Type u_1} {M : Type u_2} [] [] [Module R M] (R' : Type u_4) {M' : Type u_5} [CommRing R'] [] [Module R' M'] [Algebra R R'] [Module R M'] [IsScalarTower R R' M'] (f : M →ₗ[R] M') (q : ) (r : R) :
↑(PolynomialModule.eval (↑(algebraMap R R') r)) (↑() q) = f (↑() q)
@[simp]
theorem PolynomialModule.eval_map' {R : Type u_1} {M : Type u_2} [] [] [Module R M] (f : M →ₗ[R] M) (q : ) (r : R) :
↑() (↑() q) = f (↑() q)
@[simp]
theorem PolynomialModule.comp_apply {R : Type u_1} {M : Type u_2} [] [] [Module R M] (p : ) :
∀ (a : ), ↑() a = ↑() (↑() a)
noncomputable def PolynomialModule.comp {R : Type u_1} {M : Type u_2} [] [] [Module R M] (p : ) :

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

Instances For
theorem PolynomialModule.comp_single {R : Type u_1} {M : Type u_2} [] [] [Module R M] (p : ) (i : ) (m : M) :
↑() (↑() m) = p ^ i ↑() m
theorem PolynomialModule.comp_eval {R : Type u_1} {M : Type u_2} [] [] [Module R M] (p : ) (q : ) (r : R) :
↑() (↑() q) = ↑() q
theorem PolynomialModule.comp_smul {R : Type u_1} {M : Type u_2} [] [] [Module R M] (p : ) (p' : ) (q : ) :
↑() (p' q) = ↑() q