# 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.)

source
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 = (Polynomial.mapRingHom f).rangeS

Instances For

source
theorem Polynomial.mem_lifts {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} (p : Polynomial S) :
p ∈ lifts f ↔ ∃ (q : Polynomial R), map f q = p
source
theorem Polynomial.lifts_iff_set_range {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} (p : Polynomial S) :
p ∈ lifts f ↔ p ∈ Set.range (map f)
source
theorem Polynomial.lifts_iff_ringHom_rangeS {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} (p : Polynomial S) :
p ∈ lifts f ↔ p ∈ (mapRingHom f).rangeS
source
theorem Polynomial.lifts_iff_coeff_lifts {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} (p : Polynomial S) :
p ∈ lifts f ↔ ∀ (n : ℕ), p.coeff n ∈ Set.range ⇑f
source
theorem Polynomial.lifts_iff_coeffs_subset_range {R : Type u} [Semiring R] {S : Type v} [Semiring S] {f : R →+* S} (p : Polynomial S) :
p ∈ lifts f ↔ ↑p.coeffs ⊆ Set.range ⇑f
source
theorem Polynomial.C_mem_lifts {R : Type u} [Semiring R] {S : Type v} [Semiring S] (f : R →+* S) (r : R) :
C (f r) ∈ lifts f

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

source
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) :
C s ∈ lifts f

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

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

The polynomial `X` lifts.

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

The polynomial `X ^ n` lifts.

source
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 ∈ lifts f) :
C (f r) * p ∈ lifts f

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

source
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) :
(monomial n) s ∈ lifts f

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

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

If `p` lifts then `p.erase n` lifts.

source
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 : (monomial n) s ∈ lifts f) :
∃ (q : Polynomial R), map f q = (monomial n) s ∧ q.degree = ((monomial n) s).degree
source
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 ∈ lifts f) :
∃ (q : Polynomial R), 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.

source
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 ∈ lifts f) (hp : p.Monic) :
∃ (q : Polynomial R), 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.

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

Instances For

source
theorem Polynomial.lifts_iff_liftsRing {R : Type u} [Ring R] {S : Type v} [Ring S] (f : R →+* S) (p : Polynomial S) :
p ∈ lifts f ↔ p ∈ 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.

source
theorem Polynomial.mem_lifts_iff_mem_alg (R : Type u) [CommSemiring R] {S : Type v} [Semiring S] [Algebra R S] (p : Polynomial S) :
p ∈ lifts (algebraMap R S) ↔ p ∈ (mapAlg R S).range

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

source
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 ∈ lifts (algebraMap R S)) :
r • p ∈ lifts (algebraMap R S)

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

source
theorem Polynomial.monic_of_monic_mapAlg {R : Type u} [CommSemiring R] {S : Type v} [Semiring S] [Algebra R S] [FaithfulSMul R S] {p : Polynomial R} (hp : ((mapAlg R S) p).Monic) :
p.Monic