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
.
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
Equations
Equations
Equations
Equations
- ⋯ = inst
Equations
- Module.AEval.instModulePolynomial a = Module.compHom M (Polynomial.aeval a).toRingHom
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
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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
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.
Instances For
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' := ⋯ }
Instances For
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
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
Equations
- ⋯ = ⋯