data.polynomial.module - mathlib3 docs

source

@[protected, instance]

def polynomial_module.inhabited (R : Type u_1) (M : Type u_2) [comm_ring R] [add_comm_group M] [module R M] :

inhabited (polynomial_module R M)

source

@[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 :

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

polynomial_module R M = (ℕ →₀ M)

Instances for polynomial_module

source

@[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] :

add_comm_group (polynomial_module R M)

source

@[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] :

module S (polynomial_module R M)

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

Equations

polynomial_module.module R = finsupp.module ℕ M

source

@[protected, instance]

def polynomial_module.has_coe_to_fun (R : Type u_1) {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] :

has_coe_to_fun (polynomial_module R M) (λ (_x : polynomial_module R M), ℕ → M)

Equations

polynomial_module.has_coe_to_fun R = finsupp.has_coe_to_fun

source

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

M →+ polynomial_module R 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

polynomial_module.single R i = finsupp.single_add_hom i

source

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

source

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

M →ₗ[R] polynomial_module R M

polynomial_module.single as a linear map.

Equations

polynomial_module.lsingle R i = finsupp.lsingle i

source

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

source

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) :

⇑(polynomial_module.single R i) (r • m) = r • ⇑(polynomial_module.single R i) m

source

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

source

@[protected, instance]

noncomputable def polynomial_module.polynomial_module {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] :

module (polynomial R) (polynomial_module R M)

Equations

polynomial_module.polynomial_module = module_polynomial_of_endo (finsupp.lmap_domain M R nat.succ)

source

@[protected, instance]

def polynomial_module.is_scalar_tower {R : Type u_1} [comm_ring R] {S : Type u_3} [comm_semiring S] [algebra S R] (M : Type u) [add_comm_group M] [module R M] [module S M] [is_scalar_tower S R M] :

is_scalar_tower S R (polynomial_module R M)

source

@[protected, instance]

def polynomial_module.is_scalar_tower' {R : Type u_1} [comm_ring R] {S : Type u_3} [comm_semiring S] [algebra S R] (M : Type u) [add_comm_group M] [module R M] [module S M] [is_scalar_tower S R M] :

is_scalar_tower S (polynomial R) (polynomial_module R M)

source

@[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) :

⇑(polynomial.monomial i) r • ⇑(polynomial_module.single R j) m = ⇑(polynomial_module.single R (i + j)) (r • m)

source

@[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

source

@[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

source

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)

source

noncomputable def polynomial_module.equiv_polynomial_self {R : Type u_1} [comm_ring R] :

polynomial_module R R ≃ₗ[polynomial R] polynomial R

polynomial_module 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 := _}

source

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

polynomial_module R S ≃ₗ[R] polynomial S

polynomial_module 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 := _}

source

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') :

polynomial_module R M →ₗ[R] polynomial_module R' M'

The image of a polynomial under a linear map.

Equations

polynomial_module.map R' f = finsupp.map_range.linear_map f

source

@[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) :

⇑(polynomial_module.map R' f) (⇑(polynomial_module.single R i) m) = ⇑(polynomial_module.single R' i) (⇑f m)

source

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) :

⇑(polynomial_module.map R' f) (p • q) = polynomial.map (algebra_map R R') p • ⇑(polynomial_module.map R' f) q

source

def polynomial_module.eval {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (r : R) :

polynomial_module R M →ₗ[R] M

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' := _}

source

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)

source

@[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) :

⇑(polynomial_module.eval r) (⇑(polynomial_module.single R i) m) = r ^ i • m

source

@[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) :

⇑(polynomial_module.eval r) (⇑(polynomial_module.lsingle R i) m) = r ^ i • m

source

theorem polynomial_module.eval_smul {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (p : polynomial R) (q : polynomial_module R M) (r : R) :

⇑(polynomial_module.eval r) (p • q) = polynomial.eval r p • ⇑(polynomial_module.eval r) q

source

@[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) :

⇑(polynomial_module.eval (⇑(algebra_map R R') r)) (⇑(polynomial_module.map R' f) q) = ⇑f (⇑(polynomial_module.eval r) q)

source

@[simp]

theorem polynomial_module.eval_map' {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (f : M →ₗ[R] M) (q : polynomial_module R M) (r : R) :

⇑(polynomial_module.eval r) (⇑(polynomial_module.map R f) q) = ⇑f (⇑(polynomial_module.eval r) q)

source

@[simp]

theorem polynomial_module.comp_apply {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (p : polynomial R) (ᾰ : polynomial_module R M) :

⇑(polynomial_module.comp p) ᾰ = ⇑(polynomial_module.eval p) (⇑(polynomial_module.map (polynomial R) (polynomial_module.lsingle R 0)) ᾰ)

source

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) :

polynomial_module R M →ₗ[R] polynomial_module R M

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

Equations

polynomial_module.comp p = (linear_map.restrict_scalars R (polynomial_module.eval p)).comp (polynomial_module.map (polynomial R) (polynomial_module.lsingle R 0))

source

theorem polynomial_module.comp_single {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (p : polynomial R) (i : ℕ) (m : M) :

⇑(polynomial_module.comp p) (⇑(polynomial_module.single R i) m) = p ^ i • ⇑(polynomial_module.single R 0) m

source

theorem polynomial_module.comp_eval {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (p : polynomial R) (q : polynomial_module R M) (r : R) :

⇑(polynomial_module.eval r) (⇑(polynomial_module.comp p) q) = ⇑(polynomial_module.eval (polynomial.eval r p)) q

source

theorem polynomial_module.comp_smul {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] (p p' : polynomial R) (q : polynomial_module R M) :

⇑(polynomial_module.comp p) (p' • q) = p'.comp p • ⇑(polynomial_module.comp p) q

mathlib3 documentation

Polynomial module #