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.

structure PolynomialModule (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup 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 (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.

• ofCoeff :: (
• coeff : ℕ →₀ M

  The coefficients ℕ →₀ M of an element of the additive monoid algebra M[X].

• )

theorem PolynomialModule.coeff_ofCoeff {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (x : ℕ →₀ M) : { coeff := x }.coeff = x

theorem PolynomialModule.ofCoeff_coeff {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (x : PolynomialModule R M) : { coeff := x.coeff } = x

def PolynomialModule.coeffEquiv (R : Type u_2) {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] : PolynomialModule R M ≃ (ℕ →₀ M)

PolynomialModule.coeff as an equiv.

Equations

• PolynomialModule.coeffEquiv R = { toFun := PolynomialModule.coeff, invFun := PolynomialModule.ofCoeff R, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem PolynomialModule.coeffEquiv_apply (R : Type u_2) {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (self : PolynomialModule R M) : (coeffEquiv R) self = self.coeff

@[simp]

theorem PolynomialModule.coeffEquiv_symm_apply (R : Type u_2) {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (coeff : ℕ →₀ M) : (coeffEquiv R).symm coeff = { coeff := coeff }

theorem PolynomialModule.forall {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {P : PolynomialModule R M → Prop} : (∀ (p : PolynomialModule R M), P p) ↔ ∀ (q : ℕ →₀ M), P { coeff := q }

theorem PolynomialModule.exists {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {P : PolynomialModule R M → Prop} : (∃ (p : PolynomialModule R M), P p) ↔ ∃ (q : ℕ →₀ M), P { coeff := q }

theorem PolynomialModule.coeff_injective {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] : Function.Injective coeff

theorem PolynomialModule.ofCoeff_injective {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] : Function.Injective (ofCoeff R)

@[simp]

theorem PolynomialModule.coeff_inj {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {x y : PolynomialModule R M} : x.coeff = y.coeff ↔ x = y

theorem PolynomialModule.ofCoeff_inj {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {x y : ℕ →₀ M} : { coeff := x } = { coeff := y } ↔ x = y

theorem PolynomialModule.ext {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {x y : PolynomialModule R M} : x.coeff = y.coeff → x = y

Alias of the forward direction of PolynomialModule.coeff_inj.

theorem PolynomialModule.ext_iff {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {x y : PolynomialModule R M} : x = y ↔ x.coeff = y.coeff

@[implicit_reducible]

instance PolynomialModule.instInhabited {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] : Inhabited (PolynomialModule R M)

Equations

• PolynomialModule.instInhabited = { default := (PolynomialModule.coeffEquiv R).symm.1 default }

instance PolynomialModule.instNontrivial {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [Nontrivial M] : Nontrivial (PolynomialModule R M)

@[implicit_reducible]

instance PolynomialModule.instUnique {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [Subsingleton M] : Unique (PolynomialModule R M)

Equations

• PolynomialModule.instUnique = { default := (PolynomialModule.coeffEquiv R).symm default, uniq := ⋯ }

@[implicit_reducible]

instance PolynomialModule.instDecidableEq {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq M] : DecidableEq (PolynomialModule R M)

Equations

• PolynomialModule.instDecidableEq = (PolynomialModule.coeffEquiv R).decidableEq

@[implicit_reducible]

noncomputable instance PolynomialModule.instAddCommGroup {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] : AddCommGroup (PolynomialModule R M)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PolynomialModule.coeffAddEquiv {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] : PolynomialModule R M ≃+ (ℕ →₀ M)

PolynomialModule.coeff as an AddEquiv.

Equations

• PolynomialModule.coeffAddEquiv = (PolynomialModule.coeffEquiv R).addEquiv

@[simp]

theorem PolynomialModule.coeffAddEquiv_apply {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (self : PolynomialModule R M) : coeffAddEquiv self = self.coeff

@[simp]

theorem PolynomialModule.coeffAddEquiv_symm_apply {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (coeff : ℕ →₀ M) : coeffAddEquiv.symm coeff = { coeff := coeff }

@[simp]

theorem PolynomialModule.coeff_zero {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] : coeff 0 = 0

@[simp]

theorem PolynomialModule.ofCoeff_zero {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] : { coeff := 0 } = 0

@[simp]

theorem PolynomialModule.coeff_eq_zero {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {x : PolynomialModule R M} : x.coeff = 0 ↔ x = 0

@[simp]

theorem PolynomialModule.ofCoeff_eq_zero {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {x : ℕ →₀ M} : { coeff := x } = 0 ↔ x = 0

@[simp]

theorem PolynomialModule.coeff_add {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (x y : PolynomialModule R M) : (x + y).coeff = x.coeff + y.coeff

@[simp]

theorem PolynomialModule.ofCoeff_add {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (x y : ℕ →₀ M) : { coeff := x + y } = { coeff := x } + { coeff := y }

@[simp]

theorem PolynomialModule.coeff_sum {ι : Type u_1} {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (s : Finset ι) (f : ι → PolynomialModule R M) : (∑ i ∈ s, f i).coeff = ∑ i ∈ s, (f i).coeff

@[simp]

theorem PolynomialModule.ofCoeff_sum {ι : Type u_1} {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (s : Finset ι) (f : ι → ℕ →₀ M) : { coeff := ∑ i ∈ s, f i } = ∑ i ∈ s, { coeff := f i }

@[simp]

theorem PolynomialModule.coeff_finsuppSum {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] (f : ι →₀ N) (g : ι → N → PolynomialModule R M) : (f.sum g).coeff = f.sum fun (i : ι) (n : N) => (g i n).coeff

@[simp]

theorem PolynomialModule.ofCoeff_finsuppSum {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] (f : ι →₀ N) (g : ι → N → ℕ →₀ M) : { coeff := f.sum g } = f.sum fun (i : ι) (n : N) => { coeff := g i n }

noncomputable def PolynomialModule.single (R : Type u_2) {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (n : ℕ) (m : M) : PolynomialModule R M

MonoidAlgebra.single n m for m : M, r : R is the element rm : PolynomialModule R M.

Equations

• PolynomialModule.single R n m = { coeff := Finsupp.single n m }

@[simp]

theorem PolynomialModule.coeff_single {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (n : ℕ) (m : M) : (single R n m).coeff = Finsupp.single n m

@[simp]

theorem PolynomialModule.ofCoeff_single {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (n : ℕ) (m : M) : { coeff := Finsupp.single n m } = single R n m

@[deprecated PolynomialModule.coeff_single (since := "2026-06-18")]

theorem PolynomialModule.single_apply {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (n : ℕ) (m : M) : (single R n m).coeff = Finsupp.single n m

Alias of PolynomialModule.coeff_single.

@[simp]

theorem PolynomialModule.single_zero {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (n : ℕ) : single R n 0 = 0

@[simp]

theorem PolynomialModule.single_add {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (n : ℕ) (m₁ m₂ : M) : single R n (m₁ + m₂) = single R n m₁ + single R n m₂

@[implicit_reducible]

noncomputable instance PolynomialModule.instModule {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {S : Type u_5} [CommSemiring S] [Module S M] : Module S (PolynomialModule R M)

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

Equations

• PolynomialModule.instModule = Equiv.module S (PolynomialModule.coeffEquiv R)

instance PolynomialModule.instIsScalarTower {R : Type u_2} [CommRing R] {S : Type u_5} [CommSemiring S] [Algebra S R] (M : Type u) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower S R M] : IsScalarTower S R (PolynomialModule R M)

noncomputable def PolynomialModule.coeffLinearEquiv (R : Type u_2) {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (S : Type u_5) [CommSemiring S] [Module S M] : PolynomialModule R M ≃ₗ[S] ℕ →₀ M

PolynomialModule.coeff as a linear equiv.

Equations

• PolynomialModule.coeffLinearEquiv R S = Equiv.linearEquiv S (PolynomialModule.coeffEquiv R)

@[simp]

theorem PolynomialModule.coeffLinearEquiv_symm_apply (R : Type u_2) {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (S : Type u_5) [CommSemiring S] [Module S M] (a✝ : ℕ →₀ M) : (coeffLinearEquiv R S).symm a✝ = { coeff := a✝ }

@[simp]

theorem PolynomialModule.coeffLinearEquiv_apply (R : Type u_2) {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (S : Type u_5) [CommSemiring S] [Module S M] (a✝ : PolynomialModule R M) : (coeffLinearEquiv R S) a✝ = a✝.coeff

noncomputable def PolynomialModule.lsingle (R : Type u_2) {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (i : ℕ) : M →ₗ[R] PolynomialModule R M

PolynomialModule.single as a linear map.

Equations

• PolynomialModule.lsingle R i = ↑(PolynomialModule.coeffLinearEquiv R R).symm ∘ₗ Finsupp.lsingle i

theorem PolynomialModule.lsingle_apply {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (i : ℕ) (m : M) (n : ℕ) : ((lsingle R i) m).coeff n = if i = n then m else 0

theorem PolynomialModule.single_smul {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (i : ℕ) (r : R) (m : M) : single R i (r • m) = r • single R i m

theorem PolynomialModule.induction_linear {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {p : PolynomialModule R M → Prop} (x : PolynomialModule R M) (zero : p 0) (add : ∀ (x y : PolynomialModule R M), p x → p y → p (x + y)) (single : ∀ (n : ℕ) (m : M), p (single R n m)) : p x

@[implicit_reducible]

noncomputable instance PolynomialModule.polynomialModule {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] : Module (Polynomial R) (PolynomialModule R M)

Equations

• One or more equations did not get rendered due to their size.

theorem PolynomialModule.smul_def {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (f : Polynomial R) (m : PolynomialModule R M) : f • m = ((Polynomial.aeval (↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R))) f) m

instance PolynomialModule.isScalarTower' {R : Type u_2} [CommRing R] {S : Type u_5} [CommSemiring S] [Algebra S R] (M : Type u) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower S R M] : IsScalarTower S (Polynomial R) (PolynomialModule R M)

@[simp]

theorem PolynomialModule.monomial_smul_single {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (i : ℕ) (r : R) (j : ℕ) (m : M) : (Polynomial.monomial i) r • single R j m = single R (i + j) (r • m)

@[simp]

theorem PolynomialModule.monomial_smul_lsingle {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (i : ℕ) (r : R) (j : ℕ) (m : M) : (Polynomial.monomial i) r • (lsingle R j) m = (lsingle R (i + j)) (r • m)

@[simp]

theorem PolynomialModule.monomial_smul_apply {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (i : ℕ) (r : R) (g : PolynomialModule R M) (n : ℕ) : ((Polynomial.monomial i) r • g).coeff n = if i ≤ n then r • g.coeff (n - i) else 0

@[simp]

theorem PolynomialModule.smul_single_apply {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (i : ℕ) (f : Polynomial R) (m : M) (n : ℕ) : (f • single R i m).coeff n = if i ≤ n then f.coeff (n - i) • m else 0

theorem PolynomialModule.smul_apply {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (f : Polynomial R) (g : PolynomialModule R M) (n : ℕ) : (f • g).coeff n = ∑ x ∈ Finset.antidiagonal n, f.coeff x.1 • g.coeff x.2

noncomputable def PolynomialModule.equivPolynomialSelf {R : Type u_2} [CommRing R] : PolynomialModule R R ≃ₗ[Polynomial R] Polynomial R

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PolynomialModule.equivPolynomial {R : Type u_2} [CommRing R] {S : Type u_6} [CommRing S] [Algebra R S] : PolynomialModule R S ≃ₗ[R] Polynomial S

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PolynomialModule.equivPolynomialSelf_apply_eq {R : Type u_2} [CommRing R] (p : PolynomialModule R R) : equivPolynomialSelf p = equivPolynomial p

@[simp]

theorem PolynomialModule.equivPolynomial_single {R : Type u_2} [CommRing R] {S : Type u_6} [CommRing S] [Algebra R S] (n : ℕ) (x : S) : equivPolynomial (single R n x) = (Polynomial.monomial n) x

@[simp]

theorem PolynomialModule.equivPolynomial_symm_monomial {R : Type u_2} [CommRing R] {S : Type u_6} [CommRing S] [Algebra R S] (n : ℕ) (x : S) : equivPolynomial.symm ((Polynomial.monomial n) x) = single R n x

@[simp]

theorem PolynomialModule.equivPolynomial_symm_one {R : Type u_2} [CommRing R] {S : Type u_6} [CommRing S] [Algebra R S] : equivPolynomial.symm 1 = single R 0 1

theorem PolynomialModule.hom_ext {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {M' : Type u_7} [AddCommGroup M'] [Module R M'] {f g : PolynomialModule R M →ₗ[R] M'} (h : ∀ (a : ℕ), f ∘ₗ lsingle R a = g ∘ₗ lsingle R a) : f = g

Two R-linear maps from PolynomialModule R M which are equal after pre-composition with every lsingle R a are equal.

theorem PolynomialModule.hom_ext_iff {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] {M' : Type u_7} [AddCommGroup M'] [Module R M'] {f g : PolynomialModule R M →ₗ[R] M'} : f = g ↔ ∀ (a : ℕ), f ∘ₗ lsingle R a = g ∘ₗ lsingle R a

noncomputable def PolynomialModule.map {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (R' : Type u_6) {M' : Type u_7} [CommRing R'] [AddCommGroup M'] [Module R' M'] [Module R M'] (f : M →ₗ[R] M') : PolynomialModule R M →ₗ[R] PolynomialModule R' M'

The image of a polynomial under a linear map.

Equations

• PolynomialModule.map R' f = ↑(PolynomialModule.coeffLinearEquiv R' R).symm ∘ₗ Finsupp.mapRange.linearMap f ∘ₗ ↑(PolynomialModule.coeffLinearEquiv R R)

@[simp]

theorem PolynomialModule.map_single {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (R' : Type u_6) {M' : Type u_7} [CommRing R'] [AddCommGroup M'] [Module R' M'] [Module R M'] (f : M →ₗ[R] M') (i : ℕ) (m : M) : (map R' f) (single R i m) = single R' i (f m)

@[simp]

theorem PolynomialModule.map_lsingle {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (R' : Type u_6) {M' : Type u_7} [CommRing R'] [AddCommGroup M'] [Module R' M'] [Module R M'] (f : M →ₗ[R] M') (i : ℕ) (m : M) : (map R' f) ((lsingle R i) m) = (lsingle R' i) (f m)

theorem PolynomialModule.map_smul {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (R' : Type u_6) {M' : Type u_7} [CommRing R'] [AddCommGroup M'] [Module R' M'] [Module R M'] [Algebra R R'] [IsScalarTower R R' M'] (f : M →ₗ[R] M') (p : Polynomial R) (q : PolynomialModule R M) : (map R' f) (p • q) = Polynomial.map (algebraMap R R') p • (map R' f) q

def PolynomialModule.eval {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (r : R) : PolynomialModule R M →ₗ[R] M

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

Equations

• PolynomialModule.eval r = { toFun := fun (p : PolynomialModule R M) => p.coeff.sum fun (i : ℕ) (m : M) => r ^ i • m, map_add' := ⋯, map_smul' := ⋯ }

theorem PolynomialModule.eval_apply {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (r : R) (p : PolynomialModule R M) : (eval r) p = p.coeff.sum fun (i : ℕ) (m : M) => r ^ i • m

@[simp]

theorem PolynomialModule.eval_single {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (r : R) (i : ℕ) (m : M) : (eval r) (single R i m) = r ^ i • m

@[simp]

theorem PolynomialModule.eval_lsingle {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (r : R) (i : ℕ) (m : M) : (eval r) ((lsingle R i) m) = r ^ i • m

@[simp]

theorem PolynomialModule.eval_smul {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (p : Polynomial R) (q : PolynomialModule R M) (r : R) : (eval r) (p • q) = Polynomial.eval r p • (eval r) q

@[simp]

theorem PolynomialModule.eval_map {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (R' : Type u_6) {M' : Type u_7} [CommRing R'] [AddCommGroup M'] [Module R' M'] [Module R M'] [Algebra R R'] [IsScalarTower R R' M'] (f : M →ₗ[R] M') (q : PolynomialModule R M) (r : R) : (eval ((algebraMap R R') r)) ((map R' f) q) = f ((eval r) q)

@[simp]

theorem PolynomialModule.eval_map' {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) (q : PolynomialModule R M) (r : R) : (eval r) ((map R f) q) = f ((eval r) q)

@[simp]

theorem PolynomialModule.aeval_equivPolynomial {R : Type u_2} [CommRing R] {S : Type u_8} [CommRing S] [Algebra S R] (f : PolynomialModule S S) (x : R) : (Polynomial.aeval x) (equivPolynomial f) = (eval x) ((map R (Algebra.linearMap S R)) f)

noncomputable def PolynomialModule.comp {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (p : Polynomial R) : PolynomialModule R M →ₗ[R] PolynomialModule R M

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

Equations

• PolynomialModule.comp p = ↑R (PolynomialModule.eval p) ∘ₗ PolynomialModule.map (Polynomial R) (PolynomialModule.lsingle R 0)

@[simp]

theorem PolynomialModule.comp_apply {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (p : Polynomial R) (x : PolynomialModule R M) : (comp p) x = (eval p) ((map (Polynomial R) (lsingle R 0)) x)

theorem PolynomialModule.comp_single {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (p : Polynomial R) (i : ℕ) (m : M) : (comp p) (single R i m) = p ^ i • single R 0 m

theorem PolynomialModule.comp_eval {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (p : Polynomial R) (q : PolynomialModule R M) (r : R) : (eval r) ((comp p) q) = (eval (Polynomial.eval r p)) q

theorem PolynomialModule.comp_smul {R : Type u_2} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (p p' : Polynomial R) (q : PolynomialModule R M) : (comp p) (p' • q) = p'.comp p • (comp p) q