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) [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.

Equations

• PolynomialModule R M = (ℕ →₀ M)

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

Equations

• instInhabitedPolynomialModule R M = Finsupp.instInhabited

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

Equations

• instAddCommGroupPolynomialModule R M = Finsupp.instAddCommGroup

noncomputable instance PolynomialModule.instModule (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.

Equations

• PolynomialModule.instModule R = Finsupp.module ℕ M

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

Equations

• PolynomialModule.instFunLike R = Finsupp.instFunLike

instance PolynomialModule.instCoeFunForallNat (R : Type u_1) {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] : CoeFun (PolynomialModule R M) fun (x : PolynomialModule R M) => ℕ → M

Equations

• PolynomialModule.instCoeFunForallNat R = Finsupp.instCoeFun

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

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

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.

Equations

• PolynomialModule.single R i = Finsupp.singleAddHom i

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

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.

Equations

• PolynomialModule.lsingle R i = Finsupp.lsingle i

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

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

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

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)

Equations

• PolynomialModule.polynomialModule = inferInstanceAs (Module (Polynomial R) (Module.AEval' (Finsupp.lmapDomain M R Nat.succ)))

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

instance PolynomialModule.instIsScalarTower {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)

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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

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

@[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 f.coeff (n - i) • m else 0

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 = ∑ x ∈ Finset.antidiagonal n, f.coeff x.1 • g x.2

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.

Equations

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

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.

Equations

• PolynomialModule.equivPolynomial = let __src := (Polynomial.toFinsuppIso S).symm; { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯, right_inv := ⋯ }

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.

Equations

• PolynomialModule.map R' f = Finsupp.mapRange.linearMap f

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

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

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 : M) => r ^ i • m

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.

Equations

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

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

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

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

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

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

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

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

Equations

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

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

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

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) = p'.comp p • (PolynomialModule.comp p) q