AdjoinRoot.lift_of
theorem AdjoinRoot.lift_of :
∀ {R : Type u} {S : Type v} [inst : CommRing R] {f : Polynomial R} [inst_1 : CommRing S] {i : R →+* S} {a : S}
(h : Polynomial.eval₂ i a f = 0) {x : R}, (AdjoinRoot.lift i a h) ((AdjoinRoot.of f) x) = i x
The theorem `AdjoinRoot.lift_of` states that for any commutative rings `R` and `S`, any ring homomorphism `i` from `R` to `S`, any polynomial `f` over `R`, and any element `a` of `S` such that `f` evaluates to `0` at `a` (in the sense of applying the ring homomorphism `i` to the coefficients of `f` and then evaluating at `a`), the result of applying the function `AdjoinRoot.lift i a h` to the image of any element `x` of `R` under the function `AdjoinRoot.of f` is equal to the image of `x` under `i`. This effectively says that `AdjoinRoot.lift i a h` is a lifting of the ring homomorphism `i` to the ring of adjoined roots of `f`, which maps `R` to `S` in a way that preserves the images of elements of `R` under `i`.
More concisely: For any commutative rings R and S, ring homomorphism i from R to S, polynomial f over R, and element a of S such that f(a) = 0 under i, AdjoinRoot.lift i a h(AdjoinRoot.of f x) = i(x) for all x in R.
|
AdjoinRoot.algHom_ext
theorem AdjoinRoot.algHom_ext :
∀ {R : Type u} {S : Type v} [inst : CommRing R] {f : Polynomial R} [inst_1 : Semiring S] [inst_2 : Algebra R S]
{g₁ g₂ : AdjoinRoot f →ₐ[R] S}, g₁ (AdjoinRoot.root f) = g₂ (AdjoinRoot.root f) → g₁ = g₂
This theorem states that, for any given commutative ring `R`, a polynomial `f` of `R`, a semiring `S`, and an algebra `S` over `R`, any two algebra homomorphisms `g₁` and `g₂` from the ring obtained by adjoining a root of the polynomial `f` to `R` (denoted `AdjoinRoot f`) to `S` are identical if and only if they map the adjoined root of `f` to the same element in `S`. In other words, the behaviour of an algebra homomorphism from `AdjoinRoot f` to `S` is completely determined by the image of the adjoined root of `f`.
More concisely: For any commutative ring `R`, polynomial `f` over `R`, semiring `S`, and algebra `A` over `R` and `S`, two algebra homomorphisms `g₁` and `g₂` from `AdjoinRoot f` to `A` are equal if and only if they map the adjoined root of `f` to the same element in `A`.
|
AdjoinRoot.induction_on
theorem AdjoinRoot.induction_on :
∀ {R : Type u} [inst : CommRing R] (f : Polynomial R) {C : AdjoinRoot f → Prop} (x : AdjoinRoot f),
(∀ (p : Polynomial R), C ((AdjoinRoot.mk f) p)) → C x
This theorem, `AdjoinRoot.induction_on`, establishes an induction principle for elements in the ring adjoined by a root of a polynomial `f`. The theorem states that for any type `R` with a commutative ring structure, any polynomial `f` of type `Polynomial R`, any property `C` of elements in the ring `AdjoinRoot f`, and any element `x` of `AdjoinRoot f`, if the property `C` holds for all elements in the ring `AdjoinRoot f` that are images under the ring homomorphism `AdjoinRoot.mk` of polynomials in `R`, then the property `C` also holds for the element `x`. Essentially, this allows us to prove properties about elements in the adjoined ring by proving them for elements in the original ring.
More concisely: Given a commutative ring `R`, a polynomial `f` over `R`, and a property `C` of elements in the ring `AdjoinRoot f`, if `C` holds for all images of polynomials in `R` under the ring homomorphism `AdjoinRoot.mk`, then `C` holds for all elements in `AdjoinRoot f`.
|
AdjoinRoot.eval₂_root
theorem AdjoinRoot.eval₂_root :
∀ {R : Type u} [inst : CommRing R] (f : Polynomial R),
Polynomial.eval₂ (AdjoinRoot.of f) (AdjoinRoot.root f) f = 0
The theorem `AdjoinRoot.eval₂_root` states that for any commutative ring `R` and any polynomial `f` over `R`, if we evaluate the polynomial `f` using the ring homomorphism `AdjoinRoot.of f` which embeds the ring `R` into the ring of adjoined roots of `f`, and the adjoined root `AdjoinRoot.root f` of the polynomial `f`, the result is zero. This essentially means that the adjoined root is a root of the polynomial `f`.
More concisely: For any commutative ring R and polynomial f over R, evaluating f using the ring homomorphism AdjoinRoot.of f in the ring of adjoined roots results in zero at the adjoined root of f.
|
AdjoinRoot.mk_eq_mk
theorem AdjoinRoot.mk_eq_mk :
∀ {R : Type u} [inst : CommRing R] {f g h : Polynomial R}, (AdjoinRoot.mk f) g = (AdjoinRoot.mk f) h ↔ f ∣ g - h
This theorem states that for any commutative ring `R` and any polynomials `f`, `g`, and `h` over `R`, the equality of the images of `g` and `h` under the ring homomorphism from `R[x]` to `AdjoinRoot f` (which sends `X` to the `root` of `f`) is equivalent to `f` dividing the difference of `g` and `h`. That is, the ring homomorphism maps `g` and `h` to the same element in the `AdjoinRoot f` ring if and only if `f` is a divisor of the polynomial obtained by subtracting `h` from `g`.
More concisely: For any commutative ring `R`, polynomials `f`, `g`, and `h` over `R`, `g` and `h` map to the same element in `AdjoinRoot f` if and only if `f` divides `g - h` in `R[x]`.
|
AdjoinRoot.minpoly_root
theorem AdjoinRoot.minpoly_root :
∀ {K : Type w} [inst : Field K] {f : Polynomial K},
f ≠ 0 → minpoly K (AdjoinRoot.root f) = f * Polynomial.C f.leadingCoeff⁻¹
This theorem states that for any field `K` and any non-zero polynomial `f` over `K`, the minimal polynomial of the adjoined root of `f` is equal to `f` multiplied by the multiplicative inverse of the constant polynomial of the leading coefficient of `f`. Here, the minimal polynomial of an element over a field is the least degree monic polynomial which the element satisfies. The leading coefficient of a polynomial is the coefficient of the highest power of `X`. The constant polynomial of a number is the polynomial which is constantly that number.
More concisely: For any field `K` and non-zero polynomial `f` over `K`, the minimal polynomial of the root of `f` is `f` multiplied by the multiplicative inverse of `f`'s leading coefficient.
|
AdjoinRoot.powerBasis_gen
theorem AdjoinRoot.powerBasis_gen :
∀ {K : Type w} [inst : Field K] {f : Polynomial K} (hf : f ≠ 0),
(AdjoinRoot.powerBasis hf).gen = AdjoinRoot.root f
This theorem states that for any field `K` and any non-zero polynomial `f` of type `Polynomial K`, the generator of the power basis associated with the adjoined root of `f` is equal to the adjoined root of `f` itself. In other words, the base element used to construct the power basis (a certain set of elements in algebra) when adjoining the root of a non-zero polynomial to a field is the adjoined root of the polynomial.
More concisely: For any field `K` and non-zero polynomial `f` over `K`, the root of `f` is the generator of the power basis when adjoining that root to `K`.
|
AdjoinRoot.liftHom_root
theorem AdjoinRoot.liftHom_root :
∀ {R : Type u} {S : Type v} [inst : CommRing R] (f : Polynomial R) [inst_1 : CommRing S] {a : S}
[inst_2 : Algebra R S] (hfx : (Polynomial.aeval a) f = 0), (AdjoinRoot.liftHom f a hfx) (AdjoinRoot.root f) = a
The theorem `AdjoinRoot.liftHom_root` states that for any commutative ring `R`, polynomial `f` over `R`, commutative ring `S`, and element `a` of `S` such that `a` is a root of `f` (i.e., `Polynomial.aeval a f = 0`), the algebra homomorphism from `AdjoinRoot f` to `S` created by `AdjoinRoot.liftHom` maps the adjoined root of `f` (i.e., `AdjoinRoot.root f`) to `a`. This essentially states that the mapped value of the adjoined root under the created homomorphism is indeed the root `a` of the polynomial in the ring `S`.
More concisely: For any commutative rings R and S, polynomial f over R, and element a of S that is a root of f, the algebra homomorphism from AdjoinRoot f to S, created by AdjoinRoot.liftHom, maps the adjoined root of f to a.
|
AdjoinRoot.mk_eq_zero
theorem AdjoinRoot.mk_eq_zero :
∀ {R : Type u} [inst : CommRing R] {f g : Polynomial R}, (AdjoinRoot.mk f) g = 0 ↔ f ∣ g
This theorem states that for any type `R` which forms a commutative ring, and for any two polynomials `f` and `g` over this ring, the application of the `AdjoinRoot.mk` function on `f` applied to `g` equals zero if and only if `f` divides `g`. Here, the `AdjoinRoot.mk` function is a ring homomorphism from `R[x]` to `AdjoinRoot f` that sends `X` to the `root`, and `f ∣ g` denotes that `f` divides `g` in the ring of polynomials over `R`.
More concisely: For any commutative ring `R`, and polynomials `f` and `g` over `R`, `AdjoinRoot.mk f (g) = 0` if and only if `f` divides `g` in `R[x]`.
|
AdjoinRoot.lift_mk
theorem AdjoinRoot.lift_mk :
∀ {R : Type u} {S : Type v} [inst : CommRing R] {f : Polynomial R} [inst_1 : CommRing S] {i : R →+* S} {a : S}
(h : Polynomial.eval₂ i a f = 0) (g : Polynomial R),
(AdjoinRoot.lift i a h) ((AdjoinRoot.mk f) g) = Polynomial.eval₂ i a g
The theorem `AdjoinRoot.lift_mk` states that for any commutative rings `R` and `S`, a polynomial `f` from `R`, a ring homomorphism `i` from `R` to `S`, and an element `a` from `S` such that `a` is a root of `f` under the homomorphism `i`, the lift of the ring homomorphism from `AdjoinRoot f` to `S` applied to the image of any polynomial `g` from `R` under the ring homomorphism from `R[x]` to `AdjoinRoot f` is equal to the evaluation of `g` at `a` under the homomorphism `i`. In simpler terms, this theorem connects the operations of lifting a ring homomorphism and evaluating a polynomial.
More concisely: For any commutative rings R and S, a polynomial f from R, a ring homomorphism i from R to S, and an element a in S that is a root of f under i, the lifted homomorphism from AdjoinRoot(f) to S applied to the image of any polynomial g from R maps to the evaluation of g at a under i.
|
AdjoinRoot.mk_self
theorem AdjoinRoot.mk_self : ∀ {R : Type u} [inst : CommRing R] {f : Polynomial R}, (AdjoinRoot.mk f) f = 0
The theorem `AdjoinRoot.mk_self` states that for any type `R` which forms a commutative ring, denoted by `[inst : CommRing R]`, and for any polynomial `f` over `R`, the ring homomorphism `AdjoinRoot.mk f` applied to `f` yields zero. In other words, when the polynomial `f` is evaluated at the root adjoined by `f` itself, the result is zero. This is consistent with the concept that a root of a polynomial is a value which makes the polynomial equal to zero.
More concisely: For any commutative ring R and polynomial f over R, the polynomial evaluation of f at its root adjoined by `AdjoinRoot.mk f` is zero.
|
AdjoinRoot.mk_ne_zero_of_natDegree_lt
theorem AdjoinRoot.mk_ne_zero_of_natDegree_lt :
∀ {R : Type u} [inst : CommRing R] {f : Polynomial R},
f.Monic → ∀ {g : Polynomial R}, g ≠ 0 → g.natDegree < f.natDegree → (AdjoinRoot.mk f) g ≠ 0
The theorem `AdjoinRoot.mk_ne_zero_of_natDegree_lt` states that for any commutative ring `R` and any monic polynomial `f` of `R`, for any other polynomial `g` of `R` that is not zero and its natural degree is less than the natural degree of `f`, the ring homomorphism from `R[x]` to `AdjoinRoot f` that sends `X` to the root, when applied to `g`, does not result in zero. In other words, applying the said ring homomorphism to any non-zero polynomial of lower degree than a given monic polynomial will not yield zero.
More concisely: For any commutative ring R, monic polynomial f of R, and non-zero polynomial g of lower degree than f, the evaluation homomorphism from R[x] to the polynomials adjoining a root of f sends g to a non-zero element.
|
Irreducible.exists_dvd_monic_irreducible_of_isIntegral
theorem Irreducible.exists_dvd_monic_irreducible_of_isIntegral :
∀ {K : Type u_1} {L : Type u_2} [inst : CommRing K] [inst_1 : IsDomain K] [inst_2 : Field L] [inst_3 : Algebra K L],
Algebra.IsIntegral K L →
∀ {f : Polynomial L}, Irreducible f → ∃ g, g.Monic ∧ Irreducible g ∧ f ∣ Polynomial.map (algebraMap K L) g
The theorem `Irreducible.exists_dvd_monic_irreducible_of_isIntegral` states that for any commutative ring `K` (that is also a domain) and any field `L`, if the algebra extension `L / K` is integral (meaning every element of `L` is integral over `K`), then for any irreducible polynomial `f` over `L`, there exists a monic (leading coefficient is 1) irreducible polynomial `g` over `K` such that `f` divides the image of `g` under the map induced by the algebra structure from `K` to `L`. This theorem essentially connects the irreducibility property of a polynomial in an extended field to an irreducible polynomial in the base ring.
More concisely: For any commutative domain `K` and field extension `L/K`, if every element of `L` is integral over `K`, then for any irreducible polynomial `f` over `L`, there exists a monic irreducible polynomial `g` in `K[X]` such that `f` divides `g(X)` when treated as polynomials in `L[X]`.
|
AdjoinRoot.lift_root
theorem AdjoinRoot.lift_root :
∀ {R : Type u} {S : Type v} [inst : CommRing R] {f : Polynomial R} [inst_1 : CommRing S] {i : R →+* S} {a : S}
(h : Polynomial.eval₂ i a f = 0), (AdjoinRoot.lift i a h) (AdjoinRoot.root f) = a
The theorem `AdjoinRoot.lift_root` states that for all rings `R` and `S`, given a commutative ring structure on `R` and `S`, a polynomial `f` of type `R`, a ring homomorphism `i` from `R` to `S`, and an element `a` of `S` such that evaluating `f` at `a` via `i` is zero, then lifting `i` to a ring homomorphism from `AdjoinRoot f` to `S` and applying this to the root of `f` adjoined to `R` results in `a`. In other words, the lift of `i` sends the root of `f` in the adjoined ring back to the original root `a` in `S`.
More concisely: Given a commutative ring homomorphism `i` from ring `R` to `S`, if `i(f(x)) = 0` in `S` for some polynomial `f` over `R` and an element `x` in `AdjoinRoot f`, then `i(√[f](x)) = √[f](i(x)) = a`, where `a` is the root of `f` in `S`.
|
AdjoinRoot.root_isInv
theorem AdjoinRoot.root_isInv :
∀ {R : Type u} [inst : CommRing R] (r : R),
(AdjoinRoot.of (Polynomial.C r * Polynomial.X - 1)) r * AdjoinRoot.root (Polynomial.C r * Polynomial.X - 1) = 1
This theorem states that for any type `R` that forms a commutative ring, and any element `r` of this ring, the product of the embedding of `r` into the ring adjoined by the root of the polynomial `rX - 1` and the adjoined root of the polynomial `rX - 1` is equal to 1. In essence, it means that in the new ring formed by adjoining a root of the polynomial `rX - 1` to the original ring, the adjoined root serves as the multiplicative inverse of `r`.
More concisely: For any commutative ring `R` and its element `r`, the element `r` and the root of `rX - 1` adjoined to `R` form an invertible pair, i.e., their product equals 1 in the extended ring.
|
AdjoinRoot.aeval_eq
theorem AdjoinRoot.aeval_eq :
∀ {R : Type u} [inst : CommRing R] {f : Polynomial R} (p : Polynomial R),
(Polynomial.aeval (AdjoinRoot.root f)) p = (AdjoinRoot.mk f) p
This theorem states that for any commutative ring `R` and any polynomial `f` over `R`, and given any polynomial `p` over `R`, applying the algebra homomorphism `Polynomial.aeval` at the adjoined root of `f` to the polynomial `p` is equivalent to applying the ring homomorphism `AdjoinRoot.mk` at `f` to the polynomial `p`. In other words, the `Polynomial.aeval` function, when evaluated at the root adjoined to `f`, and the `AdjoinRoot.mk` function, when evaluated at `f`, are the same when applied to any polynomial `p` in `R`.
More concisely: For any commutative ring `R`, polynomial `f` over `R`, and polynomial `p` in `R`, `Polynomial.aeval (AdjoinRoot.mk f r) p = p.substRoot r f`, where `r` is the root adjoined to `f`.
|