Documentation

Mathlib.Data.Polynomial.AlgebraMap

Theory of univariate polynomials #

We show that A[X] is an R-algebra when A is an R-algebra. We promote eval₂ to an algebra hom in aeval.

instance Polynomial.algebraOfAlgebra {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] :

Note that this instance also provides Algebra R R[X].

Equations
theorem Polynomial.algebraMap_apply {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) :
(algebraMap R (Polynomial A)) r = Polynomial.C ((algebraMap R A) r)
@[simp]
theorem Polynomial.toFinsupp_algebraMap {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) :
((algebraMap R (Polynomial A)) r).toFinsupp = (algebraMap R (AddMonoidAlgebra A )) r
theorem Polynomial.ofFinsupp_algebraMap {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) :
{ toFinsupp := (algebraMap R (AddMonoidAlgebra A )) r } = (algebraMap R (Polynomial A)) r
theorem Polynomial.C_eq_algebraMap {R : Type u} [CommSemiring R] (r : R) :
Polynomial.C r = (algebraMap R (Polynomial R)) r

When we have [CommSemiring R], the function C is the same as algebraMap R R[X].

(But note that C is defined when R is not necessarily commutative, in which case algebraMap is not available.)

@[simp]
theorem Polynomial.CAlgHom_apply {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] :
∀ (a : A), Polynomial.CAlgHom a = Polynomial.C a

Polynomial.C as an AlgHom.

Equations
  • Polynomial.CAlgHom = { toRingHom := Polynomial.C, commutes' := }
Instances For
    theorem Polynomial.algHom_ext' {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {f : Polynomial A →ₐ[R] B} {g : Polynomial A →ₐ[R] B} (hC : AlgHom.comp f Polynomial.CAlgHom = AlgHom.comp g Polynomial.CAlgHom) (hX : f Polynomial.X = g Polynomial.X) :
    f = g

    Extensionality lemma for algebra maps out of A'[X] over a smaller base ring than A'

    @[simp]
    theorem Polynomial.toFinsuppIsoAlg_apply (R : Type u) [CommSemiring R] (self : Polynomial R) :
    (Polynomial.toFinsuppIsoAlg R) self = self.toFinsupp
    @[simp]
    theorem Polynomial.toFinsuppIsoAlg_symm_apply_toFinsupp (R : Type u) [CommSemiring R] (toFinsupp : AddMonoidAlgebra R ) :
    ((AlgEquiv.symm (Polynomial.toFinsuppIsoAlg R)) toFinsupp).toFinsupp = toFinsupp

    Algebra isomorphism between R[X] and R[ℕ]. This is just an implementation detail, but it can be useful to transfer results from Finsupp to polynomials.

    Equations
    Instances For
      Equations
      • =
      @[simp]
      theorem Polynomial.algHom_eval₂_algebraMap {R : Type u_3} {A : Type u_4} {B : Type u_5} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (p : Polynomial R) (f : A →ₐ[R] B) (a : A) :
      @[simp]
      theorem Polynomial.eval₂_algebraMap_X {R : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] (p : Polynomial R) (f : Polynomial R →ₐ[R] A) :
      Polynomial.eval₂ (algebraMap R A) (f Polynomial.X) p = f p
      @[simp]
      theorem Polynomial.ringHom_eval₂_cast_int_ringHom {R : Type u_3} {S : Type u_4} [Ring R] [Ring S] (p : Polynomial ) (f : R →+* S) (r : R) :
      @[simp]
      theorem Polynomial.eval₂_int_castRingHom_X {R : Type u_3} [Ring R] (p : Polynomial ) (f : Polynomial →+* R) :
      Polynomial.eval₂ (Int.castRingHom R) (f Polynomial.X) p = f p
      @[simp]
      theorem Polynomial.eval₂AlgHom'_apply {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (b : B) (hf : ∀ (a : A), Commute (f a) b) (p : Polynomial A) :
      def Polynomial.eval₂AlgHom' {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (b : B) (hf : ∀ (a : A), Commute (f a) b) :

      Polynomial.eval₂ as an AlgHom for noncommutative algebras.

      This is Polynomial.eval₂RingHom' for AlgHoms.

      Equations
      Instances For
        def Polynomial.aeval {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) :

        Given a valuation x of the variable in an R-algebra A, aeval R A x is the unique R-algebra homomorphism from R[X] to A sending X to x.

        This is a stronger variant of the linear map Polynomial.leval.

        Equations
        Instances For
          @[simp]
          theorem Polynomial.adjoin_X {R : Type u} [CommSemiring R] :
          Algebra.adjoin R {Polynomial.X} =
          theorem Polynomial.algHom_ext {R : Type u} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {f : Polynomial R →ₐ[R] B} {g : Polynomial R →ₐ[R] B} (hX : f Polynomial.X = g Polynomial.X) :
          f = g
          theorem Polynomial.aeval_def {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) (p : Polynomial R) :
          theorem Polynomial.aeval_zero {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) :
          @[simp]
          theorem Polynomial.aeval_X {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) :
          (Polynomial.aeval x) Polynomial.X = x
          @[simp]
          theorem Polynomial.aeval_C {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) (r : R) :
          (Polynomial.aeval x) (Polynomial.C r) = (algebraMap R A) r
          @[simp]
          theorem Polynomial.aeval_monomial {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) {n : } {r : R} :
          theorem Polynomial.aeval_X_pow {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) {n : } :
          (Polynomial.aeval x) (Polynomial.X ^ n) = x ^ n
          theorem Polynomial.aeval_add {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] {p : Polynomial R} {q : Polynomial R} (x : A) :
          theorem Polynomial.aeval_one {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) :
          @[deprecated]
          theorem Polynomial.aeval_bit0 {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] {p : Polynomial R} (x : A) :
          @[deprecated]
          theorem Polynomial.aeval_bit1 {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] {p : Polynomial R} (x : A) :
          theorem Polynomial.aeval_nat_cast {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) (n : ) :
          (Polynomial.aeval x) n = n
          theorem Polynomial.aeval_mul {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] {p : Polynomial R} {q : Polynomial R} (x : A) :
          @[simp]
          theorem Polynomial.algEquivOfCompEqX_symm_apply {R : Type u} [CommSemiring R] (p : Polynomial R) (q : Polynomial R) (hpq : Polynomial.comp p q = Polynomial.X) (hqp : Polynomial.comp q p = Polynomial.X) (a : Polynomial R) :
          @[simp]
          theorem Polynomial.algEquivOfCompEqX_apply {R : Type u} [CommSemiring R] (p : Polynomial R) (q : Polynomial R) (hpq : Polynomial.comp p q = Polynomial.X) (hqp : Polynomial.comp q p = Polynomial.X) (a : Polynomial R) :
          def Polynomial.algEquivOfCompEqX {R : Type u} [CommSemiring R] (p : Polynomial R) (q : Polynomial R) (hpq : Polynomial.comp p q = Polynomial.X) (hqp : Polynomial.comp q p = Polynomial.X) :

          Two polynomials p and q such that p(q(X))=X and q(p(X))=X induces an automorphism of the polynomial algebra.

          Equations
          Instances For
            @[simp]
            theorem Polynomial.algEquivAevalXAddC_apply {R : Type u_3} [CommRing R] (t : R) (a : Polynomial R) :
            (Polynomial.algEquivAevalXAddC t) a = (Polynomial.aeval (Polynomial.X + Polynomial.C t)) a
            @[simp]
            theorem Polynomial.algEquivAevalXAddC_symm_apply {R : Type u_3} [CommRing R] (t : R) (a : Polynomial R) :
            (AlgEquiv.symm (Polynomial.algEquivAevalXAddC t)) a = (Polynomial.aeval (Polynomial.X - Polynomial.C t)) a

            The automorphism of the polynomial algebra given by p(X) ↦ p(X+t), with inverse p(X) ↦ p(X-t).

            Equations
            Instances For
              theorem Polynomial.aeval_algHom {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (x : A) :
              @[simp]
              theorem Polynomial.aeval_X_left_apply {R : Type u} [CommSemiring R] (p : Polynomial R) :
              (Polynomial.aeval Polynomial.X) p = p
              theorem Polynomial.eval_unique {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (φ : Polynomial R →ₐ[R] A) (p : Polynomial R) :
              φ p = Polynomial.eval₂ (algebraMap R A) (φ Polynomial.X) p
              theorem Polynomial.aeval_algHom_apply {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {F : Type u_3} [FunLike F A B] [AlgHomClass F R A B] (f : F) (x : A) (p : Polynomial R) :
              (Polynomial.aeval (f x)) p = f ((Polynomial.aeval x) p)
              @[simp]
              theorem Polynomial.coe_aeval_mk_apply {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] {p : Polynomial R} (x : A) {S : Subalgebra R A} (h : x S) :
              ((Polynomial.aeval { val := x, property := h }) p) = (Polynomial.aeval x) p
              theorem Polynomial.aeval_algEquiv {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) (x : A) :
              @[simp]
              theorem Polynomial.aeval_fn_apply {R : Type u} [CommSemiring R] {X : Type u_3} (g : Polynomial R) (f : XR) (x : X) :
              theorem Polynomial.aeval_subalgebra_coe {R : Type u} [CommSemiring R] (g : Polynomial R) {A : Type u_3} [Semiring A] [Algebra R A] (s : Subalgebra R A) (f : s) :
              ((Polynomial.aeval f) g) = (Polynomial.aeval f) g
              theorem Polynomial.map_aeval_eq_aeval_map {R : Type u} [CommSemiring R] {S : Type u_3} {T : Type u_4} {U : Type u_5} [CommSemiring S] [CommSemiring T] [Semiring U] [Algebra R S] [Algebra T U] {φ : R →+* T} {ψ : S →+* U} (h : RingHom.comp (algebraMap T U) φ = RingHom.comp ψ (algebraMap R S)) (p : Polynomial R) (a : S) :
              theorem Polynomial.aeval_eq_zero_of_dvd_aeval_eq_zero {S : Type v} {T : Type w} [CommSemiring S] [CommSemiring T] [Algebra S T] {p : Polynomial S} {q : Polynomial S} (h₁ : p q) {a : T} (h₂ : (Polynomial.aeval a) p = 0) :
              @[simp]
              theorem Polynomial.aeval_eq_sum_range' {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {p : Polynomial R} {n : } (hn : Polynomial.natDegree p < n) (x : S) :
              theorem Polynomial.isRoot_of_eval₂_map_eq_zero {R : Type u} {S : Type v} [CommSemiring R] {p : Polynomial R} [Semiring S] {f : R →+* S} (hf : Function.Injective f) {r : R} :
              def Polynomial.aevalTower {R : Type u} {S : Type v} {A' : Type u_1} [CommSemiring R] [CommSemiring A'] [CommSemiring S] [Algebra S R] [Algebra S A'] (f : R →ₐ[S] A') (x : A') :

              Version of aeval for defining algebra homs out of R[X] over a smaller base ring than R.

              Equations
              Instances For
                @[simp]
                theorem Polynomial.aevalTower_X {R : Type u} {S : Type v} {A' : Type u_1} [CommSemiring R] [CommSemiring A'] [CommSemiring S] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') :
                (Polynomial.aevalTower g y) Polynomial.X = y
                @[simp]
                theorem Polynomial.aevalTower_C {R : Type u} {S : Type v} {A' : Type u_1} [CommSemiring R] [CommSemiring A'] [CommSemiring S] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') (x : R) :
                (Polynomial.aevalTower g y) (Polynomial.C x) = g x
                @[simp]
                theorem Polynomial.aevalTower_comp_C {R : Type u} {S : Type v} {A' : Type u_1} [CommSemiring R] [CommSemiring A'] [CommSemiring S] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') :
                RingHom.comp ((Polynomial.aevalTower g y)) Polynomial.C = g
                @[simp]
                theorem Polynomial.aevalTower_algebraMap {R : Type u} {S : Type v} {A' : Type u_1} [CommSemiring R] [CommSemiring A'] [CommSemiring S] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') (x : R) :
                @[simp]
                theorem Polynomial.aevalTower_comp_algebraMap {R : Type u} {S : Type v} {A' : Type u_1} [CommSemiring R] [CommSemiring A'] [CommSemiring S] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') :
                theorem Polynomial.aevalTower_toAlgHom {R : Type u} {S : Type v} {A' : Type u_1} [CommSemiring R] [CommSemiring A'] [CommSemiring S] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') (x : R) :
                @[simp]
                theorem Polynomial.aevalTower_comp_toAlgHom {R : Type u} {S : Type v} {A' : Type u_1} [CommSemiring R] [CommSemiring A'] [CommSemiring S] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') :
                @[simp]
                theorem Polynomial.aevalTower_id {S : Type v} [CommSemiring S] :
                Polynomial.aevalTower (AlgHom.id S S) = Polynomial.aeval
                @[simp]
                theorem Polynomial.aevalTower_ofId {S : Type v} {A' : Type u_1} [CommSemiring A'] [CommSemiring S] [Algebra S A'] :
                Polynomial.aevalTower (Algebra.ofId S A') = Polynomial.aeval
                theorem Polynomial.dvd_term_of_dvd_eval_of_dvd_terms {S : Type v} [CommRing S] {z : S} {p : S} {f : Polynomial S} (i : ) (dvd_eval : p Polynomial.eval z f) (dvd_terms : ∀ (j : ), j ip Polynomial.coeff f j * z ^ j) :
                theorem Polynomial.dvd_term_of_isRoot_of_dvd_terms {S : Type v} [CommRing S] {r : S} {p : S} {f : Polynomial S} (i : ) (hr : Polynomial.IsRoot f r) (h : ∀ (j : ), j ip Polynomial.coeff f j * r ^ j) :
                theorem Polynomial.eval_mul_X_sub_C {R : Type u} [Ring R] {p : Polynomial R} (r : R) :
                Polynomial.eval r (p * (Polynomial.X - Polynomial.C r)) = 0

                The evaluation map is not generally multiplicative when the coefficient ring is noncommutative, but nevertheless any polynomial of the form p * (X - monomial 0 r) is sent to zero when evaluated at r.

                This is the key step in our proof of the Cayley-Hamilton theorem.

                theorem Polynomial.not_isUnit_X_sub_C {R : Type u} [Ring R] [Nontrivial R] (r : R) :
                ¬IsUnit (Polynomial.X - Polynomial.C r)
                theorem Polynomial.aeval_endomorphism {R : Type u} {M : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) (v : M) (p : Polynomial R) :
                ((Polynomial.aeval f) p) v = Polynomial.sum p fun (n : ) (b : R) => b (f ^ n) v
                theorem Polynomial.aeval_apply_smul_mem_of_le_comap' {R : Type u} {A : Type z} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] {q : Submodule R M} {m : M} (hm : m q) (p : Polynomial R) [Semiring A] [Algebra R A] [Module A M] [IsScalarTower R A M] (a : A) (hq : q Submodule.comap ((Algebra.lsmul R R M) a) q) :
                theorem Polynomial.aeval_apply_smul_mem_of_le_comap {R : Type u} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] {q : Submodule R M} {m : M} (hm : m q) (p : Polynomial R) (f : Module.End R M) (hq : q Submodule.comap f q) :
                ((Polynomial.aeval f) p) m q