Documentation

Mathlib.Algebra.Polynomial.Lifts

Polynomials that lift #

Given semirings R and S with a morphism f : R →+* S, we define a subsemiring lifts of S[X] by the image of RingHom.of (map f). Then, we prove that a polynomial that lifts can always be lifted to a polynomial of the same degree and that a monic polynomial that lifts can be lifted to a monic polynomial (of the same degree).

Main definition #

Main results #

Implementation details #

In general R and S are semiring, so lifts is a semiring. In the case of rings, see lifts_iff_lifts_ring.

Since we do not assume R to be commutative, we cannot say in general that the set of polynomials that lift is a subalgebra. (By lift_iff this is true if R is commutative.)

def Polynomial.lifts {R : Type u} [Semiring R] {S : Type v} [Semiring S] (f : R →+* S) :

We define the subsemiring of polynomials that lifts as the image of RingHom.of (map f).

Equations
Instances For
    theorem Polynomial.mem_lifts {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} (p : Polynomial S) :
    theorem Polynomial.lifts_iff_coeff_lifts {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} (p : Polynomial S) :
    p Polynomial.lifts f ∀ (n : ), p.coeff n Set.range f
    theorem Polynomial.C_mem_lifts {R : Type u} [Semiring R] {S : Type v} [Semiring S] (f : R →+* S) (r : R) :
    Polynomial.C (f r) Polynomial.lifts f

    If (r : R), then C (f r) lifts.

    theorem Polynomial.C'_mem_lifts {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} {s : S} (h : s Set.range f) :
    Polynomial.C s Polynomial.lifts f

    If (s : S) is in the image of f, then C s lifts.

    theorem Polynomial.X_mem_lifts {R : Type u} [Semiring R] {S : Type v} [Semiring S] (f : R →+* S) :
    Polynomial.X Polynomial.lifts f

    The polynomial X lifts.

    theorem Polynomial.X_pow_mem_lifts {R : Type u} [Semiring R] {S : Type v} [Semiring S] (f : R →+* S) (n : ) :
    Polynomial.X ^ n Polynomial.lifts f

    The polynomial X ^ n lifts.

    theorem Polynomial.base_mul_mem_lifts {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} {p : Polynomial S} (r : R) (hp : p Polynomial.lifts f) :
    Polynomial.C (f r) * p Polynomial.lifts f

    If p lifts and (r : R) then r * p lifts.

    theorem Polynomial.monomial_mem_lifts {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} {s : S} (n : ) (h : s Set.range f) :

    If (s : S) is in the image of f, then monomial n s lifts.

    theorem Polynomial.erase_mem_lifts {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} {p : Polynomial S} (n : ) (h : p Polynomial.lifts f) :

    If p lifts then p.erase n lifts.

    theorem Polynomial.monomial_mem_lifts_and_degree_eq {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} {s : S} {n : } (hl : (Polynomial.monomial n) s Polynomial.lifts f) :
    ∃ (q : Polynomial R), Polynomial.map f q = (Polynomial.monomial n) s q.degree = ((Polynomial.monomial n) s).degree
    theorem Polynomial.mem_lifts_and_degree_eq {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} {p : Polynomial S} (hlifts : p Polynomial.lifts f) :
    ∃ (q : Polynomial R), Polynomial.map f q = p q.degree = p.degree

    A polynomial lifts if and only if it can be lifted to a polynomial of the same degree.

    theorem Polynomial.lifts_and_degree_eq_and_monic {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} [Nontrivial S] {p : Polynomial S} (hlifts : p Polynomial.lifts f) (hp : p.Monic) :
    ∃ (q : Polynomial R), Polynomial.map f q = p q.degree = p.degree q.Monic

    A monic polynomial lifts if and only if it can be lifted to a monic polynomial of the same degree.

    theorem Polynomial.lifts_and_natDegree_eq_and_monic {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} {p : Polynomial S} (hlifts : p Polynomial.lifts f) (hp : p.Monic) :
    ∃ (q : Polynomial R), Polynomial.map f q = p q.natDegree = p.natDegree q.Monic
    def Polynomial.liftsRing {R : Type u} [Ring R] {S : Type v} [Ring S] (f : R →+* S) :

    The subring of polynomials that lift.

    Equations
    Instances For

      If R and S are rings, p is in the subring of polynomials that lift if and only if it is in the subsemiring of polynomials that lift.

      The map R[X] → S[X] as an algebra homomorphism.

      Equations
      Instances For

        mapAlg is the morphism induced by R → S.

        A polynomial p lifts if and only if it is in the image of mapAlg.

        theorem Polynomial.smul_mem_lifts {R : Type u} [CommSemiring R] {S : Type v} [Semiring S] [Algebra R S] {p : Polynomial S} (r : R) (hp : p Polynomial.lifts (algebraMap R S)) :

        If p lifts and (r : R) then r • p lifts.