Documentation

Mathlib.Data.Polynomial.Module

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] :
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_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] :
    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_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) :
      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] :
      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] :
      Equations
      @[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
      Instances For
        @[inline, reducible]
        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' φ) :
          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 :

          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
          Instances For
            noncomputable instance instInhabitedPolynomialModule (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] :
            Equations
            noncomputable instance instAddCommGroupPolynomialModule (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] :
            Equations
            instance PolynomialModule.funLike (R : Type u_1) {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] :
            FunLike (PolynomialModule R M) fun (x : ) => M
            Equations
            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 : ) :

            The monomial m * x ^ i. This is defeq to Finsupp.singleAddHom, and is redefined here so that it has the desired type signature.

            Equations
            Instances For
              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 : ) :

              PolynomialModule.single as a linear map.

              Equations
              Instances For
                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) :
                theorem PolynomialModule.induction_linear {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {P : PolynomialModule R MProp} (f : PolynomialModule R M) (h0 : P 0) (hadd : ∀ (f g : PolynomialModule R M), P fP gP (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] :
                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) :
                @[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

                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.
                Instances For
                  noncomputable def PolynomialModule.equivPolynomial {R : Type u_1} [CommRing R] {S : Type u_4} [CommRing S] [Algebra R 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.
                  Instances For
                    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') :

                    The image of a polynomial under a linear map.

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

                      Evaluate a polynomial p : PolynomialModule R M at r : R.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[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) :
                        @[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) :
                        @[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) :
                        @[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) :
                        noncomputable def PolynomialModule.comp {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (p : Polynomial R) :

                        comp p q is the composition of p : R[X] and q : M[X] as q(p(x)).

                        Equations
                        Instances For
                          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) :