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.
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
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
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
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
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 (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
Instances For
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_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 : Module.AEval R M a)
:
(Module.AEval.of R M a).symm (f • m) = (Polynomial.aeval a) f • (Module.AEval.of R M a).symm m
@[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 : Module.AEval R M a)
:
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 • (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_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 : Module.AEval R M a)
:
(Module.AEval.of R M a).symm (Polynomial.X • m) = a • (Module.AEval.of R M a).symm m
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) (Module.AEval R M a)
Equations
- ⋯ = ⋯
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) (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 ∘ₗ ↑(Module.AEval.of R M a).symm; { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
Instances For
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]
:
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_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)
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.
Instances For
@[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' := ⋯ }
Instances For
@[simp]
theorem
Module.AEval.mem_mapSubmodule
{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]
{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 ↔ (Module.AEval.of R M a).symm 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]
:
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}
@[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
@[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] 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 φ
Instances For
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' φ)
:
(Module.AEval'.of φ).symm (Polynomial.X • m) = φ ((Module.AEval'.of φ).symm m)
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) (Module.AEval' φ)
Equations
- ⋯ = ⋯