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.

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

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

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.

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

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

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

theorem PolynomialModule.single_apply (R : Type u_1) {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (i : ℕ) (m : M) (n : ℕ) : ((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.

theorem PolynomialModule.lsingle_apply (R : Type u_1) {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (i : ℕ) (m : M) (n : ℕ) : ((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) : (single R i) (r • m) = r • (single R i) m

theorem PolynomialModule.induction_linear {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {motive : PolynomialModule R M → Prop} (f : PolynomialModule R M) (zero : motive 0) (add : ∀ (f g : PolynomialModule R M), motive f → motive g → motive (f + g)) (single : ∀ (a : ℕ) (b : M), motive ((single R a) b)) : motive 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)

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)

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)

@[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 • (single R j) m = (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 • (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.

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.

@[simp]

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

@[simp]

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

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.

@[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) : (map R' f) ((single R i) m) = (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'] [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

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

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) : (eval r) p = Finsupp.sum p fun (i : ℕ) (m : M) => r ^ i • m

@[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) : (eval r) ((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) : (eval r) ((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) : (eval r) (p • q) = Polynomial.eval r p • (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'] [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_1} {M : Type u_2} [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_1} [CommRing R] {S : Type u_6} [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_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)).

@[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) : (comp p) a✝ = (eval p) ((map (Polynomial R) (lsingle R 0)) a✝)

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) : (comp p) ((single R i) m) = p ^ i • (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) : (eval r) ((comp p) q) = (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 p' : Polynomial R) (q : PolynomialModule R M) : (comp p) (p' • q) = p'.comp p • (comp p) q