Documentation

CompPoly.Univariate.ToPoly.RingHom

C, eval₂, and coefficient-mapping as ring homomorphisms #

CPolynomial.C, CPolynomial.eval₂ and coefficient-mapping bundled as RingHoms, plus a ring-hom extensionality principle transported from Mathlib's Polynomial.ringHom_ext.

CHom and eval₂Hom are computable; toPolyRingHom is the noncomputable bundling of toPoly (it is CPolynomial.ringEquiv), used in proofs only. These are the bundled-map building blocks behind the computable finSuccEquivNth construction for CMvPolynomial.

source
theorem CompPoly.CPolynomial.toPoly_injective {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] :
Function.Injective toPoly

toPoly is injective — it is the forward map of CPolynomial.ringEquiv.

source
theorem CompPoly.CPolynomial.eval_eq_eval₂ {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (x : R) (p : CPolynomial R) :
eval x p = eval₂ (RingHom.id R) x p

CPolynomial.eval is the identity-coefficient case of eval₂.

source
def CompPoly.CPolynomial.CHom {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] :
R →+* CPolynomial R

CPolynomial.C bundled as a ring homomorphism. Computable.

Instances For
    source
    @[simp]
    theorem CompPoly.CPolynomial.CHom_apply {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (r : R) :
    CHom r = C r
    source
    noncomputable def CompPoly.CPolynomial.toPolyRingHom {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] :
    CPolynomial R →+* Polynomial R

    toPoly bundled as a ring homomorphism (it is CPolynomial.ringEquiv). Noncomputable; used in proofs only, e.g. to bring MvPolynomial.eval₂_comp_left to bear.

    Instances For
      source
      @[simp]
      theorem CompPoly.CPolynomial.toPolyRingHom_apply {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : CPolynomial R) :
      toPolyRingHom p = p.toPoly
      source
      theorem CompPoly.CPolynomial.ringHom_ext {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] {S : Type u_2} [Semiring S] {f g : CPolynomial R →+* S} (hC : ∀ (r : R), f (C r) = g (C r)) (hX : f X = g X) :
      f = g

      Two ring homomorphisms out of CPolynomial R are equal once they agree on the constants and on X.

      source
      def CompPoly.CPolynomial.eval₂Hom {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] {S : Type u_2} [CommSemiring S] (f : R →+* S) (x : S) :
      CPolynomial R →+* S

      CPolynomial.eval₂ bundled as a ring homomorphism (the coefficient map f and the point x are fixed). Computable when S's ring operations are.

      Instances For
        source
        @[simp]
        theorem CompPoly.CPolynomial.eval₂Hom_apply {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] {S : Type u_2} [CommSemiring S] (f : R →+* S) (x : S) (p : CPolynomial R) :
        (eval₂Hom f x) p = eval₂ f x p
        source
        @[simp]
        theorem CompPoly.CPolynomial.eval₂Hom_C {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] {S : Type u_2} [CommSemiring S] (f : R →+* S) (x : S) (r : R) :
        (eval₂Hom f x) (C r) = f r
        source
        @[simp]
        theorem CompPoly.CPolynomial.eval₂Hom_X {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] {S : Type u_2} [CommSemiring S] (f : R →+* S) (x : S) :
        (eval₂Hom f x) X = x
        source
        def CompPoly.CPolynomial.mapRingHom {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] {S : Type u_2} [CommSemiring S] [BEq S] [LawfulBEq S] [Nontrivial S] (f : R →+* S) :
        CPolynomial R →+* CPolynomial S

        Map the coefficients of a computable univariate polynomial along a ring homomorphism. Computable.

        Instances For
          source
          @[simp]
          theorem CompPoly.CPolynomial.mapRingHom_C {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] {S : Type u_2} [CommSemiring S] [BEq S] [LawfulBEq S] [Nontrivial S] (f : R →+* S) (r : R) :
          (mapRingHom f) (C r) = C (f r)
          source
          @[simp]
          theorem CompPoly.CPolynomial.mapRingHom_X {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] {S : Type u_2} [CommSemiring S] [BEq S] [LawfulBEq S] [Nontrivial S] (f : R →+* S) :
          (mapRingHom f) X = X
          source
          theorem CompPoly.CPolynomial.eval_mapRingHom {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] {S : Type u_2} [CommSemiring S] [BEq S] [LawfulBEq S] [Nontrivial S] (f : R →+* S) (x : S) (p : CPolynomial R) :
          eval x ((mapRingHom f) p) = eval₂ f x p

          Evaluating a coefficient-mapped polynomial: eval x (mapRingHom f p) = eval₂ f x p.

          source
          theorem CompPoly.CPolynomial.toPoly_mapRingHom {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] {S : Type u_2} [CommSemiring S] [BEq S] [LawfulBEq S] [Nontrivial S] (f : R →+* S) (p : CPolynomial R) :
          ((mapRingHom f) p).toPoly = Polynomial.map f p.toPoly

          toPoly commutes with coefficient-mapping.

          source
          theorem CompPoly.CPolynomial.natDegree_mapRingHom_le {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] {S : Type u_2} [CommSemiring S] [BEq S] [LawfulBEq S] [Nontrivial S] (f : R →+* S) (p : CPolynomial R) :
          ((mapRingHom f) p).natDegree ≤ p.natDegree

          Coefficient-mapping does not increase the degree.