mathlib3 documentation

data.polynomial.module

Polynomial module #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]
@[nolint]
def polynomial_module (R : Type u_1) (M : Type u_2) [comm_ring R] [add_comm_group M] [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 (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 :

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] [add_comm_group M] [module R M] :
@[protected, nolint, instance]
noncomputable def polynomial_module.module (R : Type u_1) {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] {S : Type u_3} [comm_semiring S] [algebra S R] [module S M] [is_scalar_tower S R M] :

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

Equations
noncomputable def polynomial_module.single (R : Type u_1) {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (i : ) :

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] [add_comm_group M] [module R M] (i : ) (m : M) (n : ) :
((polynomial_module.single R i) m) n = ite (i = n) m 0
noncomputable def polynomial_module.lsingle (R : Type u_1) {M : Type u_2} [comm_ring R] [add_comm_group M] [module 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] [add_comm_group M] [module R M] (i : ) (m : M) (n : ) :
((polynomial_module.lsingle R i) m) n = ite (i = n) m 0
theorem polynomial_module.single_smul (R : Type u_1) {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (i : ) (r : R) (m : M) :
theorem polynomial_module.induction_linear {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] {P : polynomial_module R M Prop} (f : polynomial_module R M) (h0 : P 0) (hadd : (f g : polynomial_module R M), P f P g P (f + g)) (hsingle : (a : ) (b : M), P ((polynomial_module.single R a) b)) :
P f
@[protected, instance]
@[protected, instance]
@[simp]
theorem polynomial_module.monomial_smul_single {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (i : ) (r : R) (j : ) (m : M) :
@[simp]
theorem polynomial_module.monomial_smul_apply {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (i : ) (r : R) (g : polynomial_module R M) (n : ) :
((polynomial.monomial i) 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] [add_comm_group M] [module R M] (i : ) (f : polynomial R) (m : M) (n : ) :
(f (polynomial_module.single R i) 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] [add_comm_group M] [module R M] (f : polynomial R) (g : polynomial_module R M) (n : ) :
(f g) n = (finset.nat.antidiagonal n).sum (λ (x : × ), f.coeff x.fst g x.snd)
noncomputable def polynomial_module.map {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (R' : Type u_4) {M' : Type u_5} [comm_ring R'] [add_comm_group M'] [module R' M'] [algebra R R'] [module R M'] [is_scalar_tower R 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] [add_comm_group M] [module R M] (R' : Type u_4) {M' : Type u_5} [comm_ring R'] [add_comm_group M'] [module R' M'] [algebra R R'] [module R M'] [is_scalar_tower R R' M'] (f : M →ₗ[R] M') (i : ) (m : M) :
theorem polynomial_module.map_smul {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (R' : Type u_4) {M' : Type u_5} [comm_ring R'] [add_comm_group M'] [module R' M'] [algebra R R'] [module R M'] [is_scalar_tower R R' M'] (f : M →ₗ[R] M') (p : polynomial R) (q : polynomial_module R M) :
def polynomial_module.eval {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module 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] [add_comm_group M] [module R M] (r : R) (p : polynomial_module R M) :
(polynomial_module.eval r) p = finsupp.sum p (λ (i : ) (m : M), r ^ i m)
@[simp]
theorem polynomial_module.eval_single {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (r : R) (i : ) (m : M) :
@[simp]
theorem polynomial_module.eval_lsingle {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (r : R) (i : ) (m : M) :
@[simp]
theorem polynomial_module.eval_map {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (R' : Type u_4) {M' : Type u_5} [comm_ring R'] [add_comm_group M'] [module R' M'] [algebra R R'] [module R M'] [is_scalar_tower R R' M'] (f : M →ₗ[R] M') (q : polynomial_module R M) (r : R) :
@[simp]
noncomputable def polynomial_module.comp {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (p : polynomial R) :

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

Equations