mathlib3 documentation

data.polynomial.lifts

Polynomials that lift #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Given semirings R and S with a morphism f : R →+* S, we define a subsemiring lifts of S[X] by the image of ring_hom.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 map_alg, where map_alg : 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.)

noncomputable 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 ring_hom.of (map f).

Equations

polynomial.lifts f = (polynomial.map_ring_hom f).srange

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_ring_hom_srange {R : Type u} [semiring R] {S : Type v} [semiring S] {f : R →+* S} (p : polynomial S) :

p ∈ polynomial.lifts f ↔ p ∈ (polynomial.map_ring_hom f).srange

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) :

⇑(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 ∧ 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_nat_degree_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.nat_degree = p.nat_degree ∧ q.monic

noncomputable def polynomial.lifts_ring {R : Type u} [ring R] {S : Type v} [ring S] (f : R →+* S) :

subring (polynomial S)

The subring of polynomials that lift.

Equations

polynomial.lifts_ring f = (polynomial.map_ring_hom f).range

theorem polynomial.lifts_iff_lifts_ring {R : Type u} [ring R] {S : Type v} [ring S] (f : R →+* S) (p : polynomial S) :

p ∈ polynomial.lifts f ↔ p ∈ polynomial.lifts_ring 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.

noncomputable def polynomial.map_alg (R : Type u) [comm_semiring 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.map_alg R S = polynomial.aeval polynomial.X

theorem polynomial.map_alg_eq_map {R : Type u} [comm_semiring R] {S : Type v} [semiring S] [algebra R S] (p : polynomial R) :

⇑(polynomial.map_alg R S) p = polynomial.map (algebra_map R S) p

map_alg is the morphism induced by R → S.

theorem polynomial.mem_lifts_iff_mem_alg (R : Type u) [comm_semiring R] {S : Type v} [semiring S] [algebra R S] (p : polynomial S) :

p ∈ polynomial.lifts (algebra_map R S) ↔ p ∈ (polynomial.map_alg R S).range

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

theorem polynomial.smul_mem_lifts {R : Type u} [comm_semiring R] {S : Type v} [semiring S] [algebra R S] {p : polynomial S} (r : R) (hp : p ∈ polynomial.lifts (algebra_map R S)) :

r • p ∈ polynomial.lifts (algebra_map R S)

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