Polynomial.C_mem_lifts
theorem Polynomial.C_mem_lifts :
∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] (f : R →+* S) (r : R),
Polynomial.C (f r) ∈ Polynomial.lifts f
The theorem `Polynomial.C_mem_lifts` states that for any semirings `R` and `S`, and for any ring homomorphism `f` from `R` to `S`, and any element `r` of `R`, the constant polynomial `C (f r)` is in the subsemiring of the polynomials of `S` that lift through `f`. In other words, if you have a ring homomorphism `f` from `R` to `S`, and a constant `r` in `R`, applying `f` to `r` and then creating a constant polynomial from the result will be in the subsemiring of polynomials that can be constructed through the `f` map.
More concisely: For any semirings R and S, ring homomorphism f from R to S, and element r in R, the constant polynomial C(fr) belongs to the subsemiring of S-polynomials that map to R-polynomials under f.
|
Polynomial.monomial_mem_lifts
theorem Polynomial.monomial_mem_lifts :
∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] {f : R →+* S} {s : S} (n : ℕ),
s ∈ Set.range ⇑f → (Polynomial.monomial n) s ∈ Polynomial.lifts f
The theorem `Polynomial.monomial_mem_lifts` states that for any semirings `R` and `S`, any ring homomorphism `f` from `R` to `S`, any element `s` of `S`, and any natural number `n`, if `s` is in the image of `f`, then the polynomial `a * X^n` where `a` is `s`, is in the set of polynomials that lift via `f`. In other words, if a scalar `s` can be obtained from `R` by way of the function `f`, then the polynomial that has `s` as a coefficient of `X^n` can be obtained from the polynomials over `R` by using the ring homomorphism induced by `f` on the polynomials.
More concisely: If `f` is a ring homomorphism from semiring `R` to semiring `S`, and `s` is an image of some `a` in `R`, then the monomial `a * X^n` is in the image of the polynomial map induced by `f`.
|
Polynomial.C'_mem_lifts
theorem Polynomial.C'_mem_lifts :
∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] {f : R →+* S} {s : S},
s ∈ Set.range ⇑f → Polynomial.C s ∈ Polynomial.lifts f
This theorem states that for any semirings `R` and `S` and a ring homomorphism `f` from `R` to `S`, if an element `s` from `S` is in the image of `f` (i.e., there exists some element in `R` that maps to `s` under `f`), then the constant polynomial with coefficient `s` is in the image under the ring homomorphism of the polynomial map of `f`. In other words, the constant polynomial `s` can be lifted back through the polynomial map of `f` to a polynomial in `R`.
More concisely: Given a ring homomorphism `f` from semiring `R` to semiring `S`, if `s` is in the image of `f`, then the constant polynomial `X => s` is in the image of the polynomial map of `f`.
|
Polynomial.mem_lifts_iff_mem_alg
theorem Polynomial.mem_lifts_iff_mem_alg :
∀ (R : Type u) [inst : CommSemiring R] {S : Type v} [inst_1 : Semiring S] [inst_2 : Algebra R S] (p : Polynomial S),
p ∈ Polynomial.lifts (algebraMap R S) ↔ p ∈ (Polynomial.mapAlg R S).range
The theorem `Polynomial.mem_lifts_iff_mem_alg` states that for any commutative semiring `R`, any semiring `S`, and any polynomial `p` of `S`, `p` belongs to the subsemiring of polynomials that lift through the algebra map from `R` to `S` if and only if `p` belongs to the range of the algebra homomorphism `Polynomial.mapAlg` from `R` to `S`. In other words, a polynomial `p` can be lifted from `R` to `S` using the algebra map if and only if it can be obtained through the algebra homomorphism that maps polynomials in `R` to polynomials in `S`.
More concisely: A polynomial in `S` lifts through the algebra map from `R` if and only if it is in the image of the polynomial homomorphism from `R` to `S`.
|
Polynomial.lifts_and_degree_eq_and_monic
theorem Polynomial.lifts_and_degree_eq_and_monic :
∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] {f : R →+* S} [inst_2 : Nontrivial S]
{p : Polynomial S},
p ∈ Polynomial.lifts f → p.Monic → ∃ q, Polynomial.map f q = p ∧ q.degree = p.degree ∧ q.Monic
The theorem states that for any semirings `R` and `S`, with a ring homomorphism `f` from `R` to `S`, and a nontrivial semiring `S`, if a polynomial `p` from semiring `S` is in the image of `f` under polynomial mapping (i.e., `p` is in the subsemiring of polynomials that lifts as the image of `f`), and `p` is a monic polynomial, then there exists a polynomial `q` such that `q` is the image of the polynomial `f` and the degree of `q` is the same as the degree of `p`, and `q` is also a monic polynomial. This theorem essentially provides a condition under which a polynomial can be lifted to another polynomial of the same degree and monic nature via a ring homomorphism.
More concisely: Given a semiring homomorphism `f` from semiring `R` to nontrivial semiring `S`, and a monic polynomial `p` in `S` that is the image of a polynomial in `R`, there exists a monic polynomial `q` of the same degree in `S` that is the image of a polynomial in `R` under `f`.
|
Polynomial.smul_mem_lifts
theorem Polynomial.smul_mem_lifts :
∀ {R : Type u} [inst : CommSemiring R] {S : Type v} [inst_1 : Semiring S] [inst_2 : Algebra R S] {p : Polynomial S}
(r : R), p ∈ Polynomial.lifts (algebraMap R S) → r • p ∈ Polynomial.lifts (algebraMap R S)
This theorem, `Polynomial.smul_mem_lifts`, is a statement about polynomials and algebraic structures. It states that for any commutative semiring `R`, any semiring `S`, and any algebra structure from `R` to `S`, if a polynomial `p` over `S` is in the image of the ring homomorphism induced by the `Algebra` structure (thus, `p` can be "lifted" from `R`), then the product of `p` and any element `r` from `R` (denoted `r • p`) is also in the lift of `R` to `S`. This means that scaling a polynomial which can be lifted from `R` to `S` by an element from `R` results in a polynomial that can also be lifted.
More concisely: For any commutative semirings R and S, and an algebra structure from R to S, if a polynomial p over S is the image of a polynomial q in R under the induced ring homomorphism, then r • p = r • (image of q) for any r in R. (Here, • denotes multiplication in both R and S.)
|
Polynomial.X_pow_mem_lifts
theorem Polynomial.X_pow_mem_lifts :
∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] (f : R →+* S) (n : ℕ),
Polynomial.X ^ n ∈ Polynomial.lifts f
This theorem states that for any semirings `R` and `S`, any ring homomorphism `f` from `R` to `S`, and any natural number `n`, the `n`-th power of the polynomial `X` is in the subsemiring of polynomials over `S` that lifts, i.e., is the image of `f` under polynomial mapping. In plain words, the `n`-th power of the polynomial `X` can be obtained by applying the ring homomorphism `f` to the coefficients of some polynomial in `R`. This property holds for all powers `n` of `X`, which makes the theorem quite powerful.
More concisely: For any semirings R and S, any ring homomorphism f from R to S, and natural number n, the image of X^n under f is in the subsemiring of polynomials over S that lift from R.
|
Polynomial.lifts_iff_liftsRing
theorem Polynomial.lifts_iff_liftsRing :
∀ {R : Type u} [inst : Ring R] {S : Type v} [inst_1 : Ring S] (f : R →+* S) (p : Polynomial S),
p ∈ Polynomial.lifts f ↔ p ∈ Polynomial.liftsRing f
This theorem states that for any rings `R` and `S`, a polynomial `p` from the ring `S` is in the subsemiring of polynomials that lift from `R` to `S` if and only if it's in the subring of polynomials that also lift from `R` to `S`. The lifting in this context refers to the ability to map the polynomial from `R` to `S` through a given ring homomorphism `f`.
More concisely: For any ring homomorphisms `f : R → S` and rings `R` and `S`, a polynomial `p` in `S` lifts from `R` if and only if it is in the subring of polynomials over `S` that also lie in the image of the polynomial ring `R[X]` under `f`.
|
Polynomial.erase_mem_lifts
theorem Polynomial.erase_mem_lifts :
∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] {f : R →+* S} {p : Polynomial S} (n : ℕ),
p ∈ Polynomial.lifts f → Polynomial.erase n p ∈ Polynomial.lifts f
This theorem states that for any semirings `R` and `S`, and any ring homomorphism `f` from `R` to `S`, if a polynomial `p` from the semiring `S` lies in the subsemiring of polynomials that can be obtained by mapping `R` through `f`, then the polynomial obtained by erasing the `X^n` term from `p` also lies in the same subsemiring. This means that if a polynomial can be constructed by mapping elements from `R` using `f`, then the same is true for the polynomial obtained by removing the `X^n` term from it.
More concisely: If `f` is a ring homomorphism from semiring `R` to semiring `S`, and polynomial `p` in `S` obtained from `R` elements lies in the image of `f`, then the polynomial `p` without the `X^n` term also belongs to the image of `f`.
|
Polynomial.mem_lifts_and_degree_eq
theorem Polynomial.mem_lifts_and_degree_eq :
∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] {f : R →+* S} {p : Polynomial S},
p ∈ Polynomial.lifts f → ∃ q, Polynomial.map f q = p ∧ q.degree = p.degree
The theorem `Polynomial.mem_lifts_and_degree_eq` states that, for any semirings `R` and `S`, a ring morphism `f` from `R` to `S`, and a polynomial `p` over `S`, if `p` is in the subsemiring of polynomials that lifts as the image of `f`, then there exists a polynomial `q` such that `q` mapped across `f` equals `p` and the degree of `q` is the same as the degree of `p`. This theorem characterizes the condition under which a polynomial over a semiring can be lifted to a polynomial of the same degree over another semiring via a ring morphism.
More concisely: Given semirings R and S, a ring morphism f from R to S, and a polynomial p over S that is the image of a polynomial q over R under f, then the degree of p equals the degree of q.
|
Polynomial.X_mem_lifts
theorem Polynomial.X_mem_lifts :
∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] (f : R →+* S),
Polynomial.X ∈ Polynomial.lifts f
This theorem states that for any given semirings `R` and `S` and any ring homomorphism `f` from `R` to `S`, the polynomial `X` (the polynomial variable or indeterminate) is an element of the subsemiring of polynomials that lifts as the image of `RingHom.of (map f)`. In other words, the polynomial `X` can be lifted through the ring homomorphism `f` into the semiring `S`.
More concisely: For any semirings R and S and ring homomorphism f from R to S, the polynomial indeterminate X in R[X] is mapped to the polynomial indeterminate in S[X] under the image of the homomorphism f.
|
Polynomial.mapAlg_eq_map
theorem Polynomial.mapAlg_eq_map :
∀ {R : Type u} [inst : CommSemiring R] {S : Type v} [inst_1 : Semiring S] [inst_2 : Algebra R S] (p : Polynomial R),
(Polynomial.mapAlg R S) p = Polynomial.map (algebraMap R S) p
The theorem `Polynomial.mapAlg_eq_map` states that for any commutative semiring `R`, semiring `S`, and polynomial `p` over `R`, the map `Polynomial.mapAlg R S` applied to `p` is equivalent to applying the `Polynomial.map` function to `p` with the `algebraMap R S`. In other words, the `mapAlg` function, which represents the algebra homomorphism from `R[X]` to `S[X]`, is actually induced by the ring homomorphism `R → S`, given by the `algebraMap` function.
More concisely: For any commutative semirings R and S, and polynomial p over R, the algebra homomorphism from R[X] to S[X] induced by the ring homomorphism R -> S is equivalent to applying the Polynomial.map function with algebraMap R S to p.
|
Polynomial.base_mul_mem_lifts
theorem Polynomial.base_mul_mem_lifts :
∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] {f : R →+* S} {p : Polynomial S} (r : R),
p ∈ Polynomial.lifts f → Polynomial.C (f r) * p ∈ Polynomial.lifts f
The theorem `Polynomial.base_mul_mem_lifts` states that for any given types `R` and `S` with Semiring structures, a Ring homomorphism `f` from `R` to `S`, a polynomial `p` of type `S`, and a scalar `r` of type `R`, if the polynomial `p` is in the subsemiring of polynomials that lifts as the image of the Ring homomorphism `f`, then the polynomial resulted from the multiplication of the constant polynomial of `f r` and `p` also belongs to the same subsemiring. In simpler words, if `p` is a polynomial that can be 'lifted' from `R` to `S` by the homomorphism `f`, then the polynomial `f r * p` can also be 'lifted' in the same manner.
More concisely: If `f` is a Ring homomorphism from semiring `R` to semiring `S`, `p` is a polynomial in `S` that lifts from `R`, and `r` is an element of `R`, then the polynomial `f r * p` also lifts from `R` to `S`.
|