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.

source

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

Instances For

source

noncomputable instance instInhabitedPolynomialModule (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] :

Inhabited (PolynomialModule R M)

source

noncomputable instance instAddCommGroupPolynomialModule (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] :

AddCommGroup (PolynomialModule R M)

source

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

Module S (PolynomialModule R M)

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

source

instance PolynomialModule.funLike (R : Type u_1) {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] :

FunLike (PolynomialModule R M) ℕ fun x => M

source

instance PolynomialModule.instCoeFunPolynomialModuleForAllNat (R : Type u_1) {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] :

CoeFun (PolynomialModule R M) fun x => ℕ → M

source

theorem PolynomialModule.zero_apply (R : Type u_1) {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (i : ℕ) :

↑0 i = 0

source

theorem PolynomialModule.add_apply (R : Type u_1) {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (g₁ : PolynomialModule R M) (g₂ : PolynomialModule R M) (a : ℕ) :

↑(g₁ + g₂) a = ↑g₁ a + ↑g₂ a

source

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

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

source

theorem PolynomialModule.single_apply (R : Type u_1) {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (i : ℕ) (m : M) (n : ℕ) :

↑(↑(PolynomialModule.single R i) m) n = if i = n then m else 0

source

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

M →ₗ[R] PolynomialModule R M

PolynomialModule.single as a linear map.

Instances For

source

theorem PolynomialModule.lsingle_apply (R : Type u_1) {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (i : ℕ) (m : M) (n : ℕ) :

↑(↑(PolynomialModule.lsingle R i) m) n = if i = n then m else 0

source

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

↑(PolynomialModule.single R i) (r • m) = r • ↑(PolynomialModule.single R i) m

source

theorem PolynomialModule.induction_linear {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {P : PolynomialModule R M → Prop} (f : PolynomialModule R M) (h0 : P 0) (hadd : (f g : PolynomialModule R M) → P f → P g → P (f + g)) (hsingle : (a : ℕ) → (b : M) → P (↑(PolynomialModule.single R a) b)) :

P f

source

@[semireducible]

noncomputable instance PolynomialModule.polynomialModule {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] :

Module (Polynomial R) (PolynomialModule R M)

source

instance PolynomialModule.instIsScalarTowerPolynomialModuleToSMulToSemiringToCommSemiringToSMulToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidInstAddCommGroupPolynomialModuleToSMulZeroClassToZeroToCommMonoidWithZeroToSMulWithZeroToMonoidWithZeroToMulActionWithZeroToAddCommMonoidInstModulePolynomialModuleToSemiringToAddCommMonoidInstAddCommGroupPolynomialModuleToSMulToSMulZeroClassToZeroToCommMonoidWithZeroToSMulWithZeroToMonoidWithZeroToSemiringToMulActionWithZeroInstModulePolynomialModuleToSemiringToAddCommMonoidInstAddCommGroupPolynomialModule {R : Type u_1} [CommRing R] {S : Type u_3} [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)

source

instance PolynomialModule.isScalarTower' {R : Type u_1} [CommRing R] {S : Type u_3} [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)

source

@[simp]

theorem PolynomialModule.monomial_smul_single {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (i : ℕ) (r : R) (j : ℕ) (m : M) :

↑(Polynomial.monomial i) r • ↑(PolynomialModule.single R j) m = ↑(PolynomialModule.single R (i + j)) (r • m)

source

@[simp]

theorem PolynomialModule.monomial_smul_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (i : ℕ) (r : R) (g : PolynomialModule R M) (n : ℕ) :

↑(↑(Polynomial.monomial i) r • g) n = if i ≤ n then r • ↑g (n - i) else 0

source

@[simp]

theorem PolynomialModule.smul_single_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (i : ℕ) (f : Polynomial R) (m : M) (n : ℕ) :

↑(f • ↑(PolynomialModule.single R i) m) n = if i ≤ n then Polynomial.coeff f (n - i) • m else 0

source

theorem PolynomialModule.smul_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (f : Polynomial R) (g : PolynomialModule R M) (n : ℕ) :

↑(f • g) n = Finset.sum (Finset.Nat.antidiagonal n) fun x => Polynomial.coeff f x.fst • ↑g x.snd

source

noncomputable def PolynomialModule.equivPolynomialSelf {R : Type u_1} [CommRing R] :

PolynomialModule R R ≃ₗ[Polynomial R] Polynomial R

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

Instances For

source

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

PolynomialModule R S ≃ₗ[R] Polynomial S

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

Instances For

source

noncomputable def PolynomialModule.map {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (R' : Type u_4) {M' : Type u_5} [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.

Instances For

source

@[simp]

theorem PolynomialModule.map_single {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (R' : Type u_4) {M' : Type u_5} [CommRing R'] [AddCommGroup M'] [Module R' M'] [Module R M'] (f : M →ₗ[R] M') (i : ℕ) (m : M) :

↑(PolynomialModule.map R' f) (↑(PolynomialModule.single R i) m) = ↑(PolynomialModule.single R' i) (↑f m)

source

theorem PolynomialModule.map_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (R' : Type u_4) {M' : Type u_5} [CommRing R'] [AddCommGroup M'] [Module R' M'] [Algebra R R'] [Module R M'] [IsScalarTower R R' M'] (f : M →ₗ[R] M') (p : Polynomial R) (q : PolynomialModule R M) :

↑(PolynomialModule.map R' f) (p • q) = Polynomial.map (algebraMap R R') p • ↑(PolynomialModule.map R' f) q

source

theorem PolynomialModule.eval_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (r : R) (p : PolynomialModule R M) :

↑(PolynomialModule.eval r) p = Finsupp.sum p fun i m => r ^ i • m

source

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

PolynomialModule R M →ₗ[R] M

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

Instances For

source

@[simp]

theorem PolynomialModule.eval_single {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (r : R) (i : ℕ) (m : M) :

↑(PolynomialModule.eval r) (↑(PolynomialModule.single R i) m) = r ^ i • m

source

@[simp]

theorem PolynomialModule.eval_lsingle {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (r : R) (i : ℕ) (m : M) :

↑(PolynomialModule.eval r) (↑(PolynomialModule.lsingle R i) m) = r ^ i • m

source

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

↑(PolynomialModule.eval r) (p • q) = Polynomial.eval r p • ↑(PolynomialModule.eval r) q

source

@[simp]

theorem PolynomialModule.eval_map {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (R' : Type u_4) {M' : Type u_5} [CommRing R'] [AddCommGroup M'] [Module R' M'] [Algebra R R'] [Module R M'] [IsScalarTower R R' M'] (f : M →ₗ[R] M') (q : PolynomialModule R M) (r : R) :

↑(PolynomialModule.eval (↑(algebraMap R R') r)) (↑(PolynomialModule.map R' f) q) = ↑f (↑(PolynomialModule.eval r) q)

source

@[simp]

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

↑(PolynomialModule.eval r) (↑(PolynomialModule.map R f) q) = ↑f (↑(PolynomialModule.eval r) q)

source

@[simp]

theorem PolynomialModule.comp_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (p : Polynomial R) :

∀ (a : PolynomialModule R M), ↑(PolynomialModule.comp p) a = ↑(PolynomialModule.eval p) (↑(PolynomialModule.map (Polynomial R) (PolynomialModule.lsingle R 0)) a)

source

noncomputable def PolynomialModule.comp {R : Type u_1} {M : Type u_2} [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)).

Instances For

source

theorem PolynomialModule.comp_single {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (p : Polynomial R) (i : ℕ) (m : M) :

↑(PolynomialModule.comp p) (↑(PolynomialModule.single R i) m) = p ^ i • ↑(PolynomialModule.single R 0) m

source

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

↑(PolynomialModule.eval r) (↑(PolynomialModule.comp p) q) = ↑(PolynomialModule.eval (Polynomial.eval r p)) q

source

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

↑(PolynomialModule.comp p) (p' • q) = Polynomial.comp p' p • ↑(PolynomialModule.comp p) q