Documentation

Mathlib.Algebra.Polynomial.Module.Basic

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.

def PolynomialModule (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] :
Type (max 0 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
    noncomputable instance PolynomialModule.instModule (R : Type u_1) {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {S : Type u_3} [CommSemiring S] [Module S M] :

    This is required to have the IsScalarTower S R M instance to avoid diamonds.

    Equations
    instance PolynomialModule.instFunLike (R : Type u_1) {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] :
    Equations
    instance PolynomialModule.instCoeFunForallNat (R : Type u_1) {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] :
    CoeFun (PolynomialModule R M) fun (x : PolynomialModule R M) => 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
        noncomputable instance PolynomialModule.polynomialModule {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] :
        Equations
        instance PolynomialModule.instIsScalarTower {R : Type u_1} [CommRing R] {S : Type u_3} [CommSemiring S] [Algebra S R] (M : Type u) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower S R M] :
        Equations
        • =
        instance PolynomialModule.isScalarTower' {R : Type u_1} [CommRing R] {S : Type u_3} [CommSemiring S] [Algebra S R] (M : Type u) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower S 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 f.coeff (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 = xFinset.antidiagonal n, f.coeff 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
            @[simp]
            theorem PolynomialModule.equivPolynomialSelf_apply_eq {R : Type u_1} [CommRing R] (p : PolynomialModule R R) :
            PolynomialModule.equivPolynomialSelf p = PolynomialModule.equivPolynomial p
            @[simp]
            theorem PolynomialModule.equivPolynomial_single {R : Type u_1} [CommRing R] {S : Type u_4} [CommRing S] [Algebra R S] (n : ) (x : S) :
            PolynomialModule.equivPolynomial ((PolynomialModule.single R n) x) = (Polynomial.monomial n) x
            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'] [Module R M'] [Algebra R R'] [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
              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'] [Module R M'] [Algebra R R'] [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) :
                @[simp]
                theorem PolynomialModule.aeval_equivPolynomial {R : Type u_1} [CommRing R] {S : Type u_6} [CommRing S] [Algebra S R] (f : PolynomialModule S S) (x : R) :
                (Polynomial.aeval x) (PolynomialModule.equivPolynomial f) = (PolynomialModule.eval x) ((PolynomialModule.map R (Algebra.linearMap S R)) f)
                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) :
                  theorem PolynomialModule.comp_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (p : Polynomial R) (p' : Polynomial R) (q : PolynomialModule R M) :