Mathlib.Algebra.Polynomial.Lifts

Polynomial.lifts definition

(f : R →+* S) : Subsemiring S[X]

Full source

/-- We define the subsemiring of polynomials that lifts as the image of `RingHom.of (map f)`. -/
def lifts (f : R →+* S) : Subsemiring S[X] :=
  RingHom.rangeS (mapRingHom f)

Subsemiring of liftable polynomials via $f$

Informal description

Given a semiring homomorphism $f \colon R \to S$, the subsemiring $\text{lifts}(f)$ of $S[X]$ consists of all polynomials that can be expressed as $f(q)$ for some polynomial $q \in R[X]$, where $f$ is extended to a polynomial ring homomorphism. In other words, $\text{lifts}(f)$ is the image of the induced map $f_* \colon R[X] \to S[X]$ that applies $f$ to each coefficient.

Polynomial.mem_lifts theorem

(p : S[X]) : p ∈ lifts f ↔ ∃ q : R[X], map f q = p

Full source

theorem mem_lifts (p : S[X]) : p ∈ lifts fp ∈ lifts f ↔ ∃ q : R[X], map f q = p := by
  simp only [coe_mapRingHom, lifts, RingHom.mem_rangeS]

Characterization of Polynomials in $\text{lifts}(f)$ via Lifting Condition

Informal description

For any polynomial $p \in S[X]$, $p$ belongs to the subsemiring $\text{lifts}(f)$ if and only if there exists a polynomial $q \in R[X]$ such that the image of $q$ under the polynomial map induced by $f$ equals $p$, i.e., $\text{map}(f)(q) = p$.

Polynomial.lifts_iff_set_range theorem

(p : S[X]) : p ∈ lifts f ↔ p ∈ Set.range (map f)

Full source

theorem lifts_iff_set_range (p : S[X]) : p ∈ lifts fp ∈ lifts f ↔ p ∈ Set.range (map f) := by
  simp only [coe_mapRingHom, lifts, Set.mem_range, RingHom.mem_rangeS]

Characterization of Liftable Polynomials via Range of Induced Map

Informal description

For any polynomial $p \in S[X]$, $p$ belongs to the subsemiring $\text{lifts}(f)$ if and only if there exists a polynomial $q \in R[X]$ such that the image of $q$ under the polynomial map induced by $f$ equals $p$, i.e., $p = \text{map}(f)(q)$.

Polynomial.lifts_iff_ringHom_rangeS theorem

(p : S[X]) : p ∈ lifts f ↔ p ∈ (mapRingHom f).rangeS

Full source

theorem lifts_iff_ringHom_rangeS (p : S[X]) : p ∈ lifts fp ∈ lifts f ↔ p ∈ (mapRingHom f).rangeS := by
  simp only [coe_mapRingHom, lifts, Set.mem_range, RingHom.mem_rangeS]

Characterization of Liftable Polynomials via Ring Homomorphism Range

Informal description

For any polynomial $p \in S[X]$, $p$ belongs to the subsemiring $\text{lifts}(f)$ if and only if $p$ is in the range of the ring homomorphism $\text{mapRingHom}(f) \colon R[X] \to S[X]$.

Polynomial.lifts_iff_coeff_lifts theorem

(p : S[X]) : p ∈ lifts f ↔ ∀ n : ℕ, p.coeff n ∈ Set.range f

Full source

theorem lifts_iff_coeff_lifts (p : S[X]) : p ∈ lifts fp ∈ lifts f ↔ ∀ n : ℕ, p.coeff n ∈ Set.range f := by
  rw [lifts_iff_ringHom_rangeS, mem_map_rangeS f]
  rfl

Characterization of Liftable Polynomials via Coefficient Lifting

Informal description

For a polynomial $p \in S[X]$, $p$ belongs to the subsemiring $\text{lifts}(f)$ if and only if every coefficient of $p$ lies in the range of the ring homomorphism $f \colon R \to S$. More precisely, for every natural number $n$, the coefficient of $X^n$ in $p$ (denoted $p_n$) satisfies $p_n \in f(R)$.

Polynomial.lifts_iff_coeffs_subset_range theorem

(p : S[X]) : p ∈ lifts f ↔ (p.coeffs : Set S) ⊆ Set.range f

Full source

theorem lifts_iff_coeffs_subset_range (p : S[X]) :
    p ∈ lifts fp ∈ lifts f ↔ (p.coeffs : Set S) ⊆ Set.range f := by
  rw [lifts_iff_coeff_lifts]
  constructor
  · intro h _ hc
    obtain ⟨n, ⟨-, hn⟩⟩ := mem_coeffs_iff.mp hc
    exact hn ▸ h n
  · intro h n
    by_cases hn : p.coeff n = 0
    · exact ⟨0, by simp [hn]⟩
    · exact h <| coeff_mem_coeffs _ _ hn

Characterization of Liftable Polynomials via Coefficient Set Inclusion

Informal description

For a polynomial $p \in S[X]$, $p$ belongs to the subsemiring $\text{lifts}(f)$ if and only if the set of nonzero coefficients of $p$ is contained in the range of the ring homomorphism $f \colon R \to S$.

Polynomial.C_mem_lifts theorem

(f : R →+* S) (r : R) : C (f r) ∈ lifts f

Full source

/-- If `(r : R)`, then `C (f r)` lifts. -/
theorem C_mem_lifts (f : R →+* S) (r : R) : CC (f r) ∈ lifts f :=
  ⟨C r, by
    simp only [coe_mapRingHom, map_C, Set.mem_univ, Subsemiring.coe_top, eq_self_iff_true,
      and_self_iff]⟩

Lifting of Constant Polynomials via Ring Homomorphism

Informal description

For any semiring homomorphism $f \colon R \to S$ and any element $r \in R$, the constant polynomial $C(f(r))$ in $S[X]$ belongs to the subsemiring $\text{lifts}(f)$ of polynomials that can be lifted via $f$.

Polynomial.C'_mem_lifts theorem

{f : R →+* S} {s : S} (h : s ∈ Set.range f) : C s ∈ lifts f

Full source

/-- If `(s : S)` is in the image of `f`, then `C s` lifts. -/
theorem C'_mem_lifts {f : R →+* S} {s : S} (h : s ∈ Set.range f) : CC s ∈ lifts f := by
  obtain ⟨r, rfl⟩ := Set.mem_range.1 h
  use C r
  simp only [coe_mapRingHom, map_C, Set.mem_univ, Subsemiring.coe_top, eq_self_iff_true,
    and_self_iff]

Liftability of Constant Polynomials via Ring Homomorphism

Informal description

Let $R$ and $S$ be semirings with a ring homomorphism $f \colon R \to S$. For any element $s \in S$ that is in the range of $f$, the constant polynomial $C(s) \in S[X]$ belongs to the subsemiring of liftable polynomials $\text{lifts}(f)$.

Polynomial.X_mem_lifts theorem

(f : R →+* S) : (X : S[X]) ∈ lifts f

Full source

/-- The polynomial `X` lifts. -/
theorem X_mem_lifts (f : R →+* S) : (X : S[X]) ∈ lifts f :=
  ⟨X, by
    simp only [coe_mapRingHom, Set.mem_univ, Subsemiring.coe_top, eq_self_iff_true, map_X,
      and_self_iff]⟩

Liftability of the Polynomial Variable $X$ via Ring Homomorphism

Informal description

For any semiring homomorphism $f \colon R \to S$, the polynomial variable $X$ in $S[X]$ belongs to the subsemiring of liftable polynomials $\text{lifts}(f)$.

Polynomial.X_pow_mem_lifts theorem

(f : R →+* S) (n : ℕ) : (X ^ n : S[X]) ∈ lifts f

Full source

/-- The polynomial `X ^ n` lifts. -/
theorem X_pow_mem_lifts (f : R →+* S) (n : ℕ) : (X ^ n : S[X]) ∈ lifts f :=
  ⟨X ^ n, by
    simp only [coe_mapRingHom, map_pow, Set.mem_univ, Subsemiring.coe_top, eq_self_iff_true,
      map_X, and_self_iff]⟩

Liftability of $X^n$ via semiring homomorphism

Informal description

For any semiring homomorphism $f \colon R \to S$ and any natural number $n$, the polynomial $X^n$ in $S[X]$ belongs to the subsemiring of liftable polynomials $\text{lifts}(f)$.

Polynomial.base_mul_mem_lifts theorem

{p : S[X]} (r : R) (hp : p ∈ lifts f) : C (f r) * p ∈ lifts f

Full source

/-- If `p` lifts and `(r : R)` then `r * p` lifts. -/
theorem base_mul_mem_lifts {p : S[X]} (r : R) (hp : p ∈ lifts f) : CC (f r) * p ∈ lifts f := by
  simp only [lifts, RingHom.mem_rangeS] at hp ⊢
  obtain ⟨p₁, rfl⟩ := hp
  use C r * p₁
  simp only [coe_mapRingHom, map_C, map_mul]

Liftability is preserved under scalar multiplication by lifted constants

Informal description

Let $R$ and $S$ be semirings with a semiring homomorphism $f \colon R \to S$. For any polynomial $p \in S[X]$ that lifts via $f$ (i.e., $p \in \text{lifts}(f)$) and any element $r \in R$, the polynomial $C(f(r)) \cdot p$ also lifts via $f$, where $C$ is the constant polynomial embedding.

Polynomial.monomial_mem_lifts theorem

{s : S} (n : ℕ) (h : s ∈ Set.range f) : monomial n s ∈ lifts f

Full source

/-- If `(s : S)` is in the image of `f`, then `monomial n s` lifts. -/
theorem monomial_mem_lifts {s : S} (n : ℕ) (h : s ∈ Set.range f) : monomialmonomial n s ∈ lifts f := by
  obtain ⟨r, rfl⟩ := Set.mem_range.1 h
  use monomial n r
  simp only [coe_mapRingHom, Set.mem_univ, map_monomial, Subsemiring.coe_top, eq_self_iff_true,
    and_self_iff]

Liftability of monomials via range elements

Informal description

Let $R$ and $S$ be semirings with a semiring homomorphism $f \colon R \to S$. If an element $s \in S$ is in the image of $f$ (i.e., there exists $r \in R$ such that $f(r) = s$), then for any natural number $n$, the monomial $sX^n$ belongs to the subsemiring of liftable polynomials $\text{lifts}(f) \subseteq S[X]$.

Polynomial.erase_mem_lifts theorem

{p : S[X]} (n : ℕ) (h : p ∈ lifts f) : p.erase n ∈ lifts f

Full source

/-- If `p` lifts then `p.erase n` lifts. -/
theorem erase_mem_lifts {p : S[X]} (n : ℕ) (h : p ∈ lifts f) : p.erase n ∈ lifts f := by
  rw [lifts_iff_ringHom_rangeS, mem_map_rangeS] at h ⊢
  intro k
  by_cases hk : k = n
  · use 0
    simp only [hk, RingHom.map_zero, erase_same]
  obtain ⟨i, hi⟩ := h k
  use i
  simp only [hi, hk, erase_ne, Ne, not_false_iff]

Liftability is preserved under polynomial term erasure

Informal description

Let $R$ and $S$ be semirings with a semiring homomorphism $f \colon R \to S$, and let $p \in S[X]$ be a polynomial that lifts via $f$ (i.e., $p \in \text{lifts}(f)$). Then for any natural number $n$, the polynomial $p.\text{erase}(n)$ obtained by removing the term of degree $n$ from $p$ also lifts via $f$.

Polynomial.monomial_mem_lifts_and_degree_eq theorem

 {s : S} {n : ℕ} (hl : monomial n s ∈ lifts f) : ∃ q : R[X], map f q = monomial n s ∧ q.degree = (monomial n s).degree

Full source

theorem monomial_mem_lifts_and_degree_eq {s : S} {n : ℕ} (hl : monomialmonomial n s ∈ lifts f) :
    ∃ q : R[X], map f q = monomial n s ∧ q.degree = (monomial n s).degree := by
  rcases eq_or_ne s 0 with rfl | h
  · exact ⟨0, by simp⟩
  obtain ⟨a, rfl⟩ := coeff_monomial_same n s ▸ (monomial n s).lifts_iff_coeff_lifts.mp hl n
  refine ⟨monomial n a, map_monomial f, ?_⟩
  rw [degree_monomial, degree_monomial n h]
  exact mt (fun ha ↦ ha ▸ map_zero f) h

Lifting of Monomials with Degree Preservation

Informal description

Let $R$ and $S$ be semirings with a semiring homomorphism $f \colon R \to S$. For any monomial $sX^n \in S[X]$ that lifts via $f$ (i.e., $sX^n \in \text{lifts}(f)$), there exists a polynomial $q \in R[X]$ such that: 1. The image of $q$ under the polynomial map induced by $f$ equals $sX^n$, i.e., $f_*(q) = sX^n$ 2. The degree of $q$ equals the degree of $sX^n$

Polynomial.mem_lifts_and_degree_eq theorem

{p : S[X]} (hlifts : p ∈ lifts f) : ∃ q : R[X], map f q = p ∧ q.degree = p.degree

Full source

/-- A polynomial lifts if and only if it can be lifted to a polynomial of the same degree. -/
theorem mem_lifts_and_degree_eq {p : S[X]} (hlifts : p ∈ lifts f) :
    ∃ q : R[X], map f q = p ∧ q.degree = p.degree := by
  rw [lifts_iff_coeff_lifts] at hlifts
  let g : ℕ → R := fun k ↦ (hlifts k).choose
  have hg : ∀ k, f (g k) = p.coeff k := fun k ↦ (hlifts k).choose_spec
  let q : R[X] := ∑ k ∈ p.support, monomial k (g k)
  have hq : map f q = p := by simp_rw [q, Polynomial.map_sum, map_monomial, hg, ← as_sum_support]
  have hq' : q.support = p.support := by
    simp_rw [Finset.ext_iff, mem_support_iff, q, finset_sum_coeff, coeff_monomial,
      Finset.sum_ite_eq', ite_ne_right_iff, mem_support_iff, and_iff_left_iff_imp, not_imp_not]
    exact fun k h ↦ by rw [← hg, h, map_zero]
  exact ⟨q, hq, congrArg Finset.max hq'⟩

Lifting of Polynomials with Degree Preservation

Informal description

Let $R$ and $S$ be semirings with a semiring homomorphism $f \colon R \to S$. For any polynomial $p \in S[X]$ that belongs to the subsemiring of liftable polynomials $\text{lifts}(f)$, there exists a polynomial $q \in R[X]$ such that: 1. The image of $q$ under the coefficient-wise extension of $f$ equals $p$ (i.e., $\text{map}(f)(q) = p$), 2. The degree of $q$ equals the degree of $p$.

Polynomial.lifts_and_degree_eq_and_monic theorem

 [Nontrivial S] {p : S[X]} (hlifts : p ∈ lifts f) (hp : p.Monic) :
  ∃ q : R[X], map f q = p ∧ q.degree = p.degree ∧ q.Monic

Full source

/-- A monic polynomial lifts if and only if it can be lifted to a monic polynomial
of the same degree. -/
theorem lifts_and_degree_eq_and_monic [Nontrivial S] {p : S[X]} (hlifts : p ∈ lifts f)
    (hp : p.Monic) : ∃ q : R[X], map f q = p ∧ q.degree = p.degree ∧ q.Monic := by
  rw [lifts_iff_coeff_lifts] at hlifts
  let g : ℕ → R := fun k ↦ (hlifts k).choose
  have hg k : f (g k) = p.coeff k := (hlifts k).choose_spec
  let q : R[X] := X ^ p.natDegree + ∑ k ∈ Finset.range p.natDegree, C (g k) * X ^ k
  have hq : map f q = p := by
    simp_rw [q, Polynomial.map_add, Polynomial.map_sum, Polynomial.map_mul, Polynomial.map_pow,
      map_X, map_C, hg, ← hp.as_sum]
  have h : q.Monic := monic_X_pow_add (by simp_rw [← Fin.sum_univ_eq_sum_range, degree_sum_fin_lt])
  exact ⟨q, hq, hq ▸ (h.degree_map f).symm, h⟩

Lifting of Monic Polynomials with Degree Preservation

Informal description

Let $R$ and $S$ be semirings with $S$ nontrivial, and let $f \colon R \to S$ be a semiring homomorphism. For any monic polynomial $p \in S[X]$ that belongs to the subsemiring of liftable polynomials $\text{lifts}(f)$, there exists a monic polynomial $q \in R[X]$ such that: 1. The image of $q$ under the coefficient-wise extension of $f$ equals $p$ (i.e., $\text{map}(f)(q) = p$), 2. The degree of $q$ equals the degree of $p$.

Polynomial.lifts_and_natDegree_eq_and_monic theorem

 {p : S[X]} (hlifts : p ∈ lifts f) (hp : p.Monic) : ∃ q : R[X], map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic

Full source

theorem lifts_and_natDegree_eq_and_monic {p : S[X]} (hlifts : p ∈ lifts f) (hp : p.Monic) :
    ∃ q : R[X], map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic := by
  rcases subsingleton_or_nontrivial S with hR | hR
  · obtain rfl : p = 1 := Subsingleton.elim _ _
    exact ⟨1, Subsingleton.elim _ _, by simp, by simp⟩
  obtain ⟨p', h₁, h₂, h₃⟩ := lifts_and_degree_eq_and_monic hlifts hp
  exact ⟨p', h₁, natDegree_eq_of_degree_eq h₂, h₃⟩

Lifting of Monic Polynomials with Natural Degree Preservation

Informal description

Let $R$ and $S$ be semirings, and let $f \colon R \to S$ be a semiring homomorphism. For any monic polynomial $p \in S[X]$ that belongs to the subsemiring of liftable polynomials $\text{lifts}(f)$, there exists a monic polynomial $q \in R[X]$ such that: 1. The image of $q$ under the coefficient-wise extension of $f$ equals $p$ (i.e., $\text{map}(f)(q) = p$), 2. The natural degree of $q$ equals the natural degree of $p$.

Polynomial.liftsRing definition

(f : R →+* S) : Subring S[X]

Full source

/-- The subring of polynomials that lift. -/
def liftsRing (f : R →+* S) : Subring S[X] :=
  RingHom.range (mapRingHom f)

Subring of liftable polynomials via a ring homomorphism

Informal description

Given a ring homomorphism $ f \colon R \to S $, the subring $\text{liftsRing}(f)$ of $S[X]$ consists of all polynomials that can be expressed as $ \text{map}(f)(q) $ for some polynomial $ q \in R[X] $. In other words, it is the range of the induced ring homomorphism $\text{mapRingHom}(f) \colon R[X] \to S[X]$, which applies $ f $ coefficient-wise to polynomials in $ R[X] $.

Polynomial.lifts_iff_liftsRing theorem

(p : S[X]) : p ∈ lifts f ↔ p ∈ liftsRing f

Full source

/-- 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. -/
theorem lifts_iff_liftsRing (p : S[X]) : p ∈ lifts fp ∈ lifts f ↔ p ∈ liftsRing f := by
  simp only [lifts, liftsRing, RingHom.mem_range, RingHom.mem_rangeS]

Equivalence of Liftable Polynomials in Subsemiring and Subring via $f$

Informal description

For any polynomial $p \in S[X]$, $p$ belongs to the subsemiring of liftable polynomials via $f$ if and only if $p$ belongs to the subring of liftable polynomials via $f$.

Polynomial.mapAlg definition

(R : Type u) [CommSemiring R] (S : Type v) [Semiring S] [Algebra R S] : R[X] →ₐ[R] S[X]

Full source

/-- The map `R[X] → S[X]` as an algebra homomorphism. -/
def mapAlg (R : Type u) [CommSemiring R] (S : Type v) [Semiring S] [Algebra R S] :
    R[X]R[X] →ₐ[R] S[X] :=
  @aeval _ S[X] _ _ _ (X : S[X])

Polynomial algebra homomorphism induced by $ R $-algebra structure

Informal description

Given a commutative semiring $ R $, a semiring $ S $ with an $ R $-algebra structure, the algebra homomorphism $\text{mapAlg} \colon R[X] \to S[X]$ is the unique $ R $-algebra homomorphism that sends the polynomial variable $ X $ in $ R[X] $ to $ X $ in $ S[X] $. It maps a polynomial $ p \in R[X] $ to the polynomial in $ S[X] $ obtained by applying the algebra structure map $ R \to S $ to each coefficient of $ p $.

Polynomial.mapAlg_eq_map theorem

(p : R[X]) : mapAlg R S p = map (algebraMap R S) p

Full source

/-- `mapAlg` is the morphism induced by `R → S`. -/
theorem mapAlg_eq_map (p : R[X]) : mapAlg R S p = map (algebraMap R S) p := by
  simp only [mapAlg, aeval_def, eval₂_eq_sum, map, algebraMap_apply, RingHom.coe_comp]
  ext; congr

Equality of Polynomial Algebra Homomorphism and Coefficient-wise Map

Informal description

For any polynomial $p \in R[X]$, the image of $p$ under the algebra homomorphism $\text{mapAlg} \colon R[X] \to S[X]$ is equal to the polynomial obtained by applying the algebra structure map $\text{algebraMap} \colon R \to S$ to each coefficient of $p$.

Polynomial.mem_lifts_iff_mem_alg theorem

 (R : Type u) [CommSemiring R] {S : Type v} [Semiring S] [Algebra R S] (p : S[X]) :
  p ∈ lifts (algebraMap R S) ↔ p ∈ AlgHom.range (@mapAlg R _ S _ _)

Full source

/-- A polynomial `p` lifts if and only if it is in the image of `mapAlg`. -/
theorem mem_lifts_iff_mem_alg (R : Type u) [CommSemiring R] {S : Type v} [Semiring S] [Algebra R S]
    (p : S[X]) : p ∈ lifts (algebraMap R S)p ∈ lifts (algebraMap R S) ↔ p ∈ AlgHom.range (@mapAlg R _ S _ _) := by
  simp only [coe_mapRingHom, lifts, mapAlg_eq_map, AlgHom.mem_range, RingHom.mem_rangeS]

Characterization of Liftable Polynomials via Algebra Homomorphism

Informal description

Let $R$ be a commutative semiring and $S$ a semiring with an $R$-algebra structure. For any polynomial $p \in S[X]$, $p$ belongs to the subsemiring of liftable polynomials $\text{lifts}(\text{algebraMap}\, R\, S)$ if and only if $p$ is in the range of the algebra homomorphism $\text{mapAlg} \colon R[X] \to S[X]$.

Polynomial.smul_mem_lifts theorem

{p : S[X]} (r : R) (hp : p ∈ lifts (algebraMap R S)) : r • p ∈ lifts (algebraMap R S)

Full source

/-- If `p` lifts and `(r : R)` then `r • p` lifts. -/
theorem smul_mem_lifts {p : S[X]} (r : R) (hp : p ∈ lifts (algebraMap R S)) :
    r • p ∈ lifts (algebraMap R S) := by
  rw [mem_lifts_iff_mem_alg] at hp ⊢
  exact Subalgebra.smul_mem (mapAlg R S).range hp r

Closure of liftable polynomials under scalar multiplication

Informal description

Let $R$ be a commutative semiring and $S$ a semiring with an $R$-algebra structure. For any polynomial $p \in S[X]$ that belongs to the subsemiring of liftable polynomials $\text{lifts}(\text{algebraMap}\, R\, S)$, and for any element $r \in R$, the scalar multiple $r \cdot p$ also belongs to $\text{lifts}(\text{algebraMap}\, R\, S)$.

Polynomial.monic_of_monic_mapAlg theorem

[FaithfulSMul R S] {p : Polynomial R} (hp : (mapAlg R S p).Monic) : p.Monic

Full source

theorem monic_of_monic_mapAlg [FaithfulSMul R S] {p : Polynomial R} (hp : (mapAlg R S p).Monic) :
    p.Monic :=
  monic_of_injective (FaithfulSMul.algebraMap_injective R S) hp

Monicity Preservation under Polynomial Algebra Homomorphism

Informal description

Let $R$ be a commutative semiring and $S$ a semiring with a faithful scalar multiplication action of $R$. For any polynomial $p \in R[X]$, if the image of $p$ under the algebra homomorphism $\text{mapAlg} \colon R[X] \to S[X]$ is monic, then $p$ itself is monic.

Mathlib.Algebra.Polynomial.Lifts

Main definition

Main results

Implementation details