minpoly.isIntegrallyClosed_dvd
theorem minpoly.isIntegrallyClosed_dvd :
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R]
[inst_3 : Algebra R S] [inst_4 : IsDomain S] [inst_5 : NoZeroSMulDivisors R S] [inst_6 : IsIntegrallyClosed R]
{s : S}, IsIntegral R s → ∀ {p : Polynomial R}, (Polynomial.aeval s) p = 0 → minpoly R s ∣ p
This theorem states that for integrally closed rings, the minimal polynomial divides any polynomial that has the integral element as a root. This is generally applied in the setting where R and S are two commutative rings, S is an R-algebra, and both R and S are integral domains with no zero divisors of the form a * s = 0 with a in R and s in S. Given these conditions and the fact that an element s in S is integral over R, if a polynomial p over R evaluates to zero at s (using the algebra homomorphism that sends the indeterminate to s), then the minimal polynomial of s over R divides p. The theorem provides a key property of minimal polynomials in the context of integral elements and integrally closed domains.
More concisely: If R is an integrally closed domain, and s is an element in the R-algebra S that is integral over R, then the minimal polynomial of s over R divides any polynomial in R[x] that evaluates to zero at s.
|
minpoly.isIntegrallyClosed_eq_field_fractions
theorem minpoly.isIntegrallyClosed_eq_field_fractions :
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R]
[inst_3 : Algebra R S] (K : Type u_3) (L : Type u_4) [inst_4 : Field K] [inst_5 : Algebra R K]
[inst_6 : IsFractionRing R K] [inst_7 : CommRing L] [inst_8 : Nontrivial L] [inst_9 : Algebra R L]
[inst_10 : Algebra S L] [inst_11 : Algebra K L] [inst_12 : IsScalarTower R K L] [inst_13 : IsScalarTower R S L]
[inst_14 : IsIntegrallyClosed R] [inst_15 : IsDomain S] {s : S},
IsIntegral R s → minpoly K ((algebraMap S L) s) = Polynomial.map (algebraMap R K) (minpoly R s)
This theorem states that for an integrally closed domain, the minimal polynomial over the ring is the same as the minimal polynomial over the fraction field. More specifically, given an integral domain `R` that is integrally closed, a commutative ring `S`, and a field of fractions `K` of `R`, if `s` is an element of `S` that is integral over `R`, then the minimal polynomial of `s` over `K` is the same as the minimal polynomial of `s` over `R` after mapping it to `K` using the algebra map from `R` to `K`. This holds true when `S` is considered an algebra over both `R` and `K`, `K` is an algebra over `R`, and there is a scalar tower structure over `R`, `K`, and `L` - a commutative ring with non-trivial zero divisors which is also an algebra over `R`, `S`, and `K`.
More concisely: For an integrally closed domain R, the minimal polynomial of an integral element s in a commutative ring S with a scalar tower structure over R, K, and L equals the minimal polynomial of s over R when considered as an element of the field of fractions K.
|
minpoly.isIntegrallyClosed_dvd_iff
theorem minpoly.isIntegrallyClosed_dvd_iff :
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R]
[inst_3 : Algebra R S] [inst_4 : IsDomain S] [inst_5 : NoZeroSMulDivisors R S] [inst_6 : IsIntegrallyClosed R]
{s : S}, IsIntegral R s → ∀ (p : Polynomial R), (Polynomial.aeval s) p = 0 ↔ minpoly R s ∣ p
The theorem `minpoly.isIntegrallyClosed_dvd_iff` asserts that for any commutative ring `R`, commutative ring `S`, `R`-algebra structure on `S`, and a chosen element `s` from `S` which is integral over `R`, a polynomial `p` from `R` satisfies that its evaluation at `s` equals zero if and only if the minimal polynomial of `s` over `R` divides `p`. The theorem's conditions also require that `R` is an integral domain, `S` is an integral domain, `R` and `S` have no zero divisors under scalar multiplication, and `R` is integrally closed.
More concisely: A polynomial in an integrally closed integrally dominated commutative ring evaluates to zero at an algebraic element if and only if it is divisible by the element's minimal polynomial.
|
minpoly.IsIntegrallyClosed.degree_le_of_ne_zero
theorem minpoly.IsIntegrallyClosed.degree_le_of_ne_zero :
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R]
[inst_3 : Algebra R S] [inst_4 : IsDomain S] [inst_5 : NoZeroSMulDivisors R S] [inst_6 : IsIntegrallyClosed R]
{s : S},
IsIntegral R s → ∀ {p : Polynomial R}, p ≠ 0 → (Polynomial.aeval s) p = 0 → (minpoly R s).degree ≤ p.degree
The theorem states that for a commutative ring `R` and a ring `S` with an algebra structure over `R`, if `R` is integrally closed (meaning all integral elements of its field of fractions are also elements of `R`) and `S` is a domain (a non-zero commutative ring in which the product of two non-zero elements is always non-zero), then for a given element `s` in `S` that is integral over `R`, any nonzero polynomial `p` from `R` for which `s` is a root, the degree of the minimal polynomial of `s` over `R` is less than or equal to the degree of `p`. This is a statement about how the minimal polynomial of an element `s` in an algebra `S` over a ring `R` relates to other polynomials in `R` that have `s` as a root.
More concisely: If `R` is a commutative integrally closed ring and `S` is a domain with `R` being a subalgebra, then for any element `s` in `S` integral over `R` and any polynomial `p` in `R` of which `s` is a root, the degree of the minimal polynomial of `s` over `R` is less than or equal to the degree of `p`.
|
IsIntegrallyClosed.minpoly.unique
theorem IsIntegrallyClosed.minpoly.unique :
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R]
[inst_3 : Algebra R S] [inst_4 : IsDomain S] [inst_5 : NoZeroSMulDivisors R S] [inst_6 : IsIntegrallyClosed R]
{s : S} {P : Polynomial R},
P.Monic →
(Polynomial.aeval s) P = 0 →
(∀ (Q : Polynomial R), Q.Monic → (Polynomial.aeval s) Q = 0 → P.degree ≤ Q.degree) → P = minpoly R s
The theorem `IsIntegrallyClosed.minpoly.unique` states that the minimal polynomial of an element `s` in a ring `S` over a ring `R` is uniquely determined by its defining property. Specifically, if there exists another monic polynomial `P` in `R` that has `s` as a root and is of minimal degree, then this polynomial `P` is equal to the minimal polynomial of `s`. This is true under the conditions that `R` is a commutative ring, `S` is a commutative ring and a domain, there are no zero divisors in the product of `R` and `S`, `R` is integrally closed, and the polynomial `P` is monic and evaluates to zero when `s` is substituted.
More concisely: Given a commutative ring `R`, a commutative domain `S`, no zero divisors in `R` multiplying elements of `S`, an integrally closed `R`, and a monic polynomial `P` in `R` of minimal degree having `s` as a root, then `P` is the minimal polynomial of `s` in `S` over `R`.
|
minpoly.isIntegrallyClosed_eq_field_fractions'
theorem minpoly.isIntegrallyClosed_eq_field_fractions' :
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R]
[inst_3 : Algebra R S] (K : Type u_3) [inst_4 : Field K] [inst_5 : Algebra R K] [inst_6 : IsFractionRing R K]
[inst_7 : IsIntegrallyClosed R] [inst_8 : IsDomain S] [inst_9 : Algebra K S] [inst_10 : IsScalarTower R K S]
{s : S}, IsIntegral R s → minpoly K s = Polynomial.map (algebraMap R K) (minpoly R s)
This theorem states that for integrally closed domains, the minimal polynomial over the ring is the same as the minimal polynomial over the field of fractions. More precisely, given a commutative ring `R` and another ring `S` with `R` being a domain and integrally closed, and `K` being a field which is the field of fractions of `R`, an element `s` of `S` which is integral over `R`, then the minimal polynomial of `s` over `K` is equal to the minimal polynomial of `s` over `R` mapped across the ring homomorphism from `R` to `K`. This version of the theorem is useful when the element is in a ring that is already a `K`-algebra.
More concisely: For an integrally closed domain `R`, the minimal polynomial of an integral element `s` over the field of fractions `K` equals the minimal polynomial of `s` over `R`, when viewed as a polynomial in `K[X]` via the natural homomorphism from `R[X]` to `K[X]`.
|