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.

We also define, given an element a in an R-algebra A and an A-module M, an R[X]-module Module.AEval R M a, which is a type synonym of M with the action of a polynomial f given by f • m = Polynomial.aeval a f • m. In particular X • m = a • m.

In the special case that A = M →ₗ[R] M and φ : M →ₗ[R] M, the module Module.AEval R M a is abbreviated Module.AEval' φ. In this module we have X • m = ↑φ m.

def Module.AEval (R : Type u_1) (M : Type u_2) {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] : A → Type u_2

Suppose a is an element of an R-algebra A and M is an A-module. Loosely speaking, Module.AEval R M a is the R[X]-module with elements m : M, where the action of a polynomial $f$ is given by $f • m = f(a) • m$.

More precisely, Module.AEval R M a has elements Module.AEval.of R M a m for m : M, and the action of f is f • (of R M a m) = of R M a ((aeval a f) • m).

Equations

• Module.AEval R M x = M

instance Module.AEval.instAddCommGroup {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommGroup M] [Module A M] [Module R M] [IsScalarTower R A M] : AddCommGroup (Module.AEval R M a)

Equations

• Module.AEval.instAddCommGroup a = inferInstanceAs (AddCommGroup M)

instance Module.AEval.instAddCommMonoid {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] : AddCommMonoid (Module.AEval R M a)

Equations

• Module.AEval.instAddCommMonoid a = inferInstanceAs (AddCommMonoid M)

instance Module.AEval.instModuleOrig {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] : Module R (Module.AEval R M a)

Equations

• Module.AEval.instModuleOrig a = inferInstanceAs (Module R M)

instance Module.AEval.instFiniteOrig {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [Module.Finite R M] : Module.Finite R (Module.AEval R M a)

Equations

• ⋯ = ⋯

instance Module.AEval.instModulePolynomial {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] : Module (Polynomial R) (Module.AEval R M a)

Equations

• Module.AEval.instModulePolynomial a = Module.compHom M (Polynomial.aeval a).toRingHom

def Module.AEval.of (R : Type u_1) {A : Type u_2} (M : Type u_3) [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] : M ≃ₗ[R] Module.AEval R M a

The canonical linear equivalence between M and Module.AEval R M a as an R-module.

Equations

• Module.AEval.of R M a = LinearEquiv.refl R M

theorem Module.AEval.of_aeval_smul {R : Type u_1} {A : Type u_3} {M : Type u_2} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (f : Polynomial R) (m : M) : (Module.AEval.of R M a) ((Polynomial.aeval a) f • m) = f • (Module.AEval.of R M a) m

@[simp]

theorem Module.AEval.of_symm_smul {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (f : Polynomial R) (m : Module.AEval R M a) : (LinearEquiv.symm (Module.AEval.of R M a)) (f • m) = (Polynomial.aeval a) f • (LinearEquiv.symm (Module.AEval.of R M a)) m

@[simp]

theorem Module.AEval.C_smul {R : Type u_3} {A : Type u_1} {M : Type u_2} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (t : R) (m : Module.AEval R M a) : Polynomial.C t • m = t • m

theorem Module.AEval.X_smul_of {R : Type u_3} {A : Type u_2} {M : Type u_1} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (m : M) : Polynomial.X • (Module.AEval.of R M a) m = (Module.AEval.of R M a) (a • m)

theorem Module.AEval.of_symm_X_smul {R : Type u_3} {A : Type u_1} {M : Type u_2} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (m : Module.AEval R M a) : (LinearEquiv.symm (Module.AEval.of R M a)) (Polynomial.X • m) = a • (LinearEquiv.symm (Module.AEval.of R M a)) m

instance Module.AEval.instIsScalarTowerOrigPolynomial {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] : IsScalarTower R (Polynomial R) (Module.AEval R M a)

Equations

• ⋯ = ⋯

instance Module.AEval.instFinitePolynomial {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [Module.Finite R M] : Module.Finite (Polynomial R) (Module.AEval R M a)

Equations

• ⋯ = ⋯

def LinearMap.ofAEval {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] {N : Type u_4} [AddCommMonoid N] [Module R N] [Module (Polynomial R) N] [IsScalarTower R (Polynomial R) N] (f : M →ₗ[R] N) (hf : ∀ (m : M), f (a • m) = Polynomial.X • f m) : Module.AEval R M a →ₗ[Polynomial R] N

Construct an R[X]-linear map out of AEval R M a from a R-linear map out of M.

Equations

• LinearMap.ofAEval a f hf = let __spread.0 := f ∘ₗ ↑(LinearEquiv.symm (Module.AEval.of R M a)); { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }

theorem Module.AEval.annihilator_eq_ker_aeval {R : Type u_3} {A : Type u_2} {M : Type u_1} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [FaithfulSMul A M] : Module.annihilator (Polynomial R) (Module.AEval R M a) = RingHom.ker (Polynomial.aeval a)

@[simp]

theorem Module.AEval.annihilator_top_eq_ker_aeval {R : Type u_3} {A : Type u_2} {M : Type u_1} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [FaithfulSMul A M] : Submodule.annihilator ⊤ = RingHom.ker (Polynomial.aeval a)

def Module.AEval.comapSubmodule (R : Type u_1) {A : Type u_2} (M : Type u_3) [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] : CompleteLatticeHom (Submodule (Polynomial R) (Module.AEval R M a)) (Submodule R M)

We can turn an R[X]-submodule into an R-submodule by forgetting the action of X.

Equations

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

@[simp]

theorem Module.AEval.mem_comapSubmodule {R : Type u_2} {A : Type u_3} {M : Type u_1} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] {q : Submodule (Polynomial R) (Module.AEval R M a)} {x : M} : x ∈ (Module.AEval.comapSubmodule R M a) q ↔ (Module.AEval.of R M a) x ∈ q

@[simp]

theorem Module.AEval.comapSubmodule_le_comap {R : Type u_2} {A : Type u_3} {M : Type u_1} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] {q : Submodule (Polynomial R) (Module.AEval R M a)} : (Module.AEval.comapSubmodule R M a) q ≤ Submodule.comap ((Algebra.lsmul R R M) a) ((Module.AEval.comapSubmodule R M a) q)

def Module.AEval.mapSubmodule {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] {p : Submodule R M} (hp : p ≤ Submodule.comap ((Algebra.lsmul R R M) a) p) : Submodule (Polynomial R) (Module.AEval R M a)

An R-submodule which is stable under the action of a can be promoted to an R[X]-submodule.

Equations

• Module.AEval.mapSubmodule a hp = { toAddSubmonoid := AddSubmonoid.map (Module.AEval.of R M a) p.toAddSubmonoid, smul_mem' := ⋯ }

@[simp]

theorem Module.AEval.mem_mapSubmodule {R : Type u_3} {A : Type u_1} {M : Type u_2} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] {p : Submodule R M} (hp : p ≤ Submodule.comap ((Algebra.lsmul R R M) a) p) {m : Module.AEval R M a} : m ∈ Module.AEval.mapSubmodule a hp ↔ (LinearEquiv.symm (Module.AEval.of R M a)) m ∈ p

@[simp]

theorem Module.AEval.mapSubmodule_comapSubmodule {R : Type u_2} {A : Type u_3} {M : Type u_1} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] {q : Submodule (Polynomial R) (Module.AEval R M a)} (h : optParam ((Module.AEval.comapSubmodule R M a) q ≤ Submodule.comap ((Algebra.lsmul R R M) a) ((Module.AEval.comapSubmodule R M a) q)) ⋯) : Module.AEval.mapSubmodule a h = q

@[simp]

theorem Module.AEval.comapSubmodule_mapSubmodule {R : Type u_2} {A : Type u_3} {M : Type u_1} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] {p : Submodule R M} (hp : p ≤ Submodule.comap ((Algebra.lsmul R R M) a) p) : (Module.AEval.comapSubmodule R M a) (Module.AEval.mapSubmodule a hp) = p

theorem Module.AEval.injective_comapSubmodule (R : Type u_2) {A : Type u_3} (M : Type u_1) [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] : Function.Injective ⇑(Module.AEval.comapSubmodule R M a)

theorem Module.AEval.range_comapSubmodule (R : Type u_2) {A : Type u_3} (M : Type u_1) [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] : Set.range ⇑(Module.AEval.comapSubmodule R M a) = {p : Submodule R M | p ≤ Submodule.comap ((Algebra.lsmul R R M) a) p}

@[inline, reducible]

abbrev Module.AEval' {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (φ : M →ₗ[R] M) : Type u_2

Given and R-module M and a linear map φ : M →ₗ[R] M, Module.AEval' φ is loosely speaking the R[X]-module with elements m : M, where the action of a polynomial $f$ is given by $f • m = f(a) • m$.

More precisely, Module.AEval' φ has elements Module.AEval'.of φ m for m : M, and the action of f is f • (of φ m) = of φ ((aeval φ f) • m).

Module.AEval' is defined as a special case of Module.AEval in which the R-algebra is M →ₗ[R] M. Lemmas involving Module.AEval may be applied to Module.AEval'.

Equations

• Module.AEval' φ = Module.AEval R M φ

@[inline, reducible]

abbrev Module.AEval'.of {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (φ : M →ₗ[R] M) : M ≃ₗ[R] Module.AEval' φ

The canonical linear equivalence between M and Module.AEval' φ as an R-module, where φ : M →ₗ[R] M.

Equations

• Module.AEval'.of φ = Module.AEval.of R M φ

theorem Module.AEval'_def {R : Type u_2} {M : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] (φ : M →ₗ[R] M) : Module.AEval' φ = Module.AEval R M φ

theorem Module.AEval'.X_smul_of {R : Type u_2} {M : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] (φ : M →ₗ[R] M) (m : M) : Polynomial.X • (Module.AEval'.of φ) m = (Module.AEval'.of φ) (φ m)

theorem Module.AEval'.of_symm_X_smul {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (φ : M →ₗ[R] M) (m : Module.AEval' φ) : (LinearEquiv.symm (Module.AEval'.of φ)) (Polynomial.X • m) = φ ((LinearEquiv.symm (Module.AEval'.of φ)) m)

instance Module.instFinitePolynomialToSemiringAEval'SemiringInstAddCommMonoidLinearMapIdToNonAssocSemiringSemiringInstAlgebraProof_1ToSMulIdProof_2ApplyModuleApply_isScalarTowerInstModulePolynomial {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (φ : M →ₗ[R] M) [Module.Finite R M] : Module.Finite (Polynomial R) (Module.AEval' φ)

Equations

• ⋯ = ⋯

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

Equations

• PolynomialModule.instModulePolynomialModuleToSemiringToAddCommMonoidInstAddCommGroupPolynomialModule 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.instCoeFunPolynomialModuleForAllNat (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.instCoeFunPolynomialModuleForAllNat 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

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

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

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 Polynomial.coeff f (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 = Finset.sum (Finset.antidiagonal n) fun (x : ℕ × ℕ) => Polynomial.coeff f 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

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

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