Documentation

Mathlib.Algebra.Polynomial.Module.AEval

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] :
AType 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
Instances For
    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] :
    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] :
    Equations
    • = inst
    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] :
    Equations
    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] :

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

    Equations
    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) :
      @[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) :
      Polynomial.C t m = t m
      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] :
      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] :
      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) :

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

      Equations
      Instances For
        @[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] :
        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] :

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

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

          Equations
          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} :
            @[simp]
            @[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) :
            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] :
            @[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
            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) :

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

              Equations
              Instances For
                theorem Module.AEval'_def {R : Type u_2} {M : Type u_1} [CommSemiring R] [AddCommMonoid M] [Module R M] (φ : M →ₗ[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)
                Equations
                • =