# Action of the polynomial ring on module induced by an algebra element. #

Given an element `a` in an `R`-algebra `A` and an `A`-module `M` we define 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`.

source
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

Instances For

source
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 (AEval R M a)
Equations

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

source
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 (AEval R M a)
Equations

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

source
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 (AEval R M a)
Equations

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

source
instance Module.AEval.instFiniteOrig {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] [Module.Finite R M] :
Module.Finite R (AEval R M a)
source
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) (AEval R M a)
Equations

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

source
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] 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

Instances For

source
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) :
(of R M a) ((Polynomial.aeval a) f • m) = f • (of R M a) m
source
@[simp]
theorem Module.AEval.of_symm_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 : AEval R M a) :
(of R M a).symm (f • m) = (Polynomial.aeval a) f • (of R M a).symm m
source
@[simp]
theorem Module.AEval.C_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] (t : R) (m : AEval R M a) :
Polynomial.C t • m = t • m
source
theorem Module.AEval.X_smul_of {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] (m : M) :
Polynomial.X • (of R M a) m = (of R M a) (a • m)
source
theorem Module.AEval.X_pow_smul_of {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] (m : M) (n : ℕ) :
Polynomial.X ^ n • (of R M a) m = (of R M a) (a ^ n • m)
source
theorem Module.AEval.of_symm_X_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] (m : AEval R M a) :
(of R M a).symm (Polynomial.X • m) = a • (of R M a).symm m
source
instance Module.AEval.instIsScalarTowerOrigPolynomial {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] :
IsScalarTower R (Polynomial R) (AEval R M a)
source
instance Module.AEval.instFinitePolynomial {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] [Module.Finite R M] :
Module.Finite (Polynomial R) (AEval R M a)
source
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 = { toAddHom := (f ∘ₗ ↑(Module.AEval.of R M a).symm).toAddHom, map_smul' := ⋯ }

Instances For

source
def LinearEquiv.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 equivalence out of `AEval R M a` from a `R`-linear map out of `M`.

Equations

- LinearEquiv.ofAEval a f hf = { toLinearMap := LinearMap.ofAEval a (↑f) hf, invFun := ⇑(Module.AEval.of R M a) ∘ ⇑f.symm, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
theorem Module.AEval.annihilator_eq_ker_aeval {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] [FaithfulSMul A M] :
annihilator (Polynomial R) (AEval R M a) = RingHom.ker (Polynomial.aeval a)
source
@[simp]
theorem Module.AEval.annihilator_top_eq_ker_aeval {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] [FaithfulSMul A M] :
⊤.annihilator = RingHom.ker (Polynomial.aeval a)
source
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] :
↥((Algebra.lsmul R R M) a).invtSubmodule ≃o Submodule (Polynomial R) (AEval R M a)

The natural order isomorphism between the two ways to represent invariant submodules.

Equations

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

Instances For

source
@[simp]
theorem Module.AEval.mem_mapSubmodule_apply (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 : ↥((Algebra.lsmul R R M) a).invtSubmodule} {m : AEval R M a} :
m ∈ (mapSubmodule R M a) p ↔ (of R M a).symm m ∈ ↑p
source
@[simp]
theorem Module.AEval.mem_mapSubmodule_symm_apply (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] {q : Submodule (Polynomial R) (AEval R M a)} {m : M} :
m ∈ ↑((mapSubmodule R M a).symm q) ↔ (of R M a) m ∈ q
source
def Module.AEval.equiv_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 ∈ ((Algebra.lsmul R R M) a).invtSubmodule) :
↥p ≃ₗ[R] ↥((mapSubmodule R M a) ⟨p, hp⟩)

The natural `R`-linear equivalence between the two ways to represent an invariant submodule.

Equations

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

Instances For

source
noncomputable def Module.AEval.restrict_equiv_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 ∈ ((Algebra.lsmul R R M) a).invtSubmodule) :
AEval R (↥p) (LinearMap.restrict ((Algebra.lsmul R R M) a) hp) ≃ₗ[Polynomial R] ↥((mapSubmodule R M a) ⟨p, hp⟩)

The natural `R[X]`-linear equivalence between the two ways to represent an invariant submodule.

Equations

- Module.AEval.restrict_equiv_mapSubmodule a p hp = LinearEquiv.ofAEval (LinearMap.restrict ((Algebra.lsmul R R M) a) hp) (Module.AEval.equiv_mapSubmodule a p hp) ⋯

Instances For

source
@[reducible, inline]
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 φ

Instances For

source
@[reducible, inline]
abbrev Module.AEval'.of {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (φ : M →ₗ[R] M) :
M ≃ₗ[R] 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 φ

Instances For

source
theorem Module.AEval'_def {R : Type u_2} {M : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] (φ : M →ₗ[R] M) :
AEval' φ = AEval R M φ
source
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 • (of φ) m = (of φ) (φ m)
source
theorem Module.AEval'.X_pow_smul_of {R : Type u_2} {M : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] (φ : M →ₗ[R] M) (m : M) (n : ℕ) :
Polynomial.X ^ n • (of φ) m = (of φ) (φ ^ n • m)
source
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 : AEval' φ) :
(of φ).symm (Polynomial.X • m) = φ ((of φ).symm m)
source
instance Module.instFinitePolynomialAEval' {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) (AEval' φ)