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

• lifts (f : R →+* S) : the subsemiring of polynomials that lift.

Main results

• lifts_and_degree_eq : A polynomial lifts if and only if it can be lifted to a polynomial of the same degree.
• lifts_and_degree_eq_and_monic : A monic polynomial lifts if and only if it can be lifted to a monic polynomial of the same degree.
• lifts_iff_alg : if R is commutative, a polynomial lifts if and only if it is in the image of mapAlg, where mapAlg : R[X] →ₐ[R] S[X] is the only R-algebra map that sends X to X.

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) : Subsemiring (Polynomial S)

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

Equations

• Polynomial.lifts f = RingHom.rangeS (Polynomial.mapRingHom f)

theorem Polynomial.mem_lifts {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} (p : Polynomial S) : p ∈ Polynomial.lifts f ↔ ∃ (q : Polynomial R), Polynomial.map f q = p

theorem Polynomial.lifts_iff_set_range {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} (p : Polynomial S) : p ∈ Polynomial.lifts f ↔ p ∈ Set.range (Polynomial.map f)

theorem Polynomial.lifts_iff_ringHom_rangeS {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} (p : Polynomial S) : p ∈ Polynomial.lifts f ↔ p ∈ RingHom.rangeS (Polynomial.mapRingHom f)

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 : ℕ), Polynomial.coeff p 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) : (Polynomial.monomial n) s ∈ Polynomial.lifts 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) : Polynomial.erase n 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 ∧ Polynomial.degree q = Polynomial.degree ((Polynomial.monomial n) s)

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 ∧ Polynomial.degree q = Polynomial.degree p

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 : Polynomial.Monic p) : ∃ (q : Polynomial R), Polynomial.map f q = p ∧ Polynomial.degree q = Polynomial.degree p ∧ Polynomial.Monic q

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 : Polynomial.Monic p) : ∃ (q : Polynomial R), Polynomial.map f q = p ∧ Polynomial.natDegree q = Polynomial.natDegree p ∧ Polynomial.Monic q

def Polynomial.liftsRing {R : Type u} [Ring R] {S : Type v} [Ring S] (f : R →+* S) : Subring (Polynomial S)

The subring of polynomials that lift.

Equations

• Polynomial.liftsRing f = RingHom.range (Polynomial.mapRingHom f)

theorem Polynomial.lifts_iff_liftsRing {R : Type u} [Ring R] {S : Type v} [Ring S] (f : R →+* S) (p : Polynomial S) : p ∈ Polynomial.lifts f ↔ p ∈ Polynomial.liftsRing f

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.

def Polynomial.mapAlg (R : Type u) [CommSemiring R] (S : Type v) [Semiring S] [Algebra R S] : Polynomial R →ₐ[R] Polynomial S

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

Equations

• Polynomial.mapAlg R S = Polynomial.aeval Polynomial.X

theorem Polynomial.mapAlg_eq_map {R : Type u} [CommSemiring R] {S : Type v} [Semiring S] [Algebra R S] (p : Polynomial R) : (Polynomial.mapAlg R S) p = Polynomial.map (algebraMap R S) p

mapAlg is the morphism induced by R → S.

theorem Polynomial.mem_lifts_iff_mem_alg (R : Type u) [CommSemiring R] {S : Type v} [Semiring S] [Algebra R S] (p : Polynomial S) : p ∈ Polynomial.lifts (algebraMap R S) ↔ p ∈ AlgHom.range (Polynomial.mapAlg 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)) : r • p ∈ Polynomial.lifts (algebraMap R S)

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