Minimal polynomials over a GCD monoid #

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

This file specializes the theory of minpoly to the case of an algebra over a GCD monoid.

Main results #

is_integrally_closed_eq_field_fractions: For integrally closed domains, the minimal polynomial over the ring is the same as the minimal polynomial over the fraction field.
is_integrally_closed_dvd : For integrally closed domains, the minimal polynomial divides any primitive polynomial that has the integral element as root.
is_integrally_closed_unique : The minimal polynomial of an element x is uniquely characterized by its defining property: if there is another monic polynomial of minimal degree that has x as a root, then this polynomial is equal to the minimal polynomial of x.

theorem minpoly.is_integrally_closed_eq_field_fractions {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [algebra R S] (K : Type u_3) (L : Type u_4) [field K] [algebra R K] [is_fraction_ring R K] [field L] [algebra R L] [algebra S L] [algebra K L] [is_scalar_tower R K L] [is_scalar_tower R S L] [is_integrally_closed R] [is_domain S] {s : S} (hs : is_integral R s) :

minpoly K (⇑(algebra_map S L) s) = polynomial.map (algebra_map R K) (minpoly R s)

For integrally closed domains, the minimal polynomial over the ring is the same as the minimal polynomial over the fraction field. See minpoly.is_integrally_closed_eq_field_fractions' if S is already a K-algebra.

source

theorem minpoly.is_integrally_closed_eq_field_fractions' {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [algebra R S] (K : Type u_3) [field K] [algebra R K] [is_fraction_ring R K] [is_integrally_closed R] [is_domain S] [algebra K S] [is_scalar_tower R K S] {s : S} (hs : is_integral R s) :

minpoly K s = polynomial.map (algebra_map R K) (minpoly R s)

For integrally closed domains, the minimal polynomial over the ring is the same as the minimal polynomial over the fraction field. Compared to minpoly.is_integrally_closed_eq_field_fractions, this version is useful if the element is in a ring that is already a K-algebra.

source

theorem minpoly.is_integrally_closed_dvd {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [algebra R S] [is_domain S] [no_zero_smul_divisors R S] [is_integrally_closed R] [nontrivial R] {s : S} (hs : is_integral R s) {p : polynomial R} (hp : ⇑(polynomial.aeval s) p = 0) :

minpoly R s ∣ p

For integrally closed rings, the minimal polynomial divides any polynomial that has the integral element as root. See also minpoly.dvd which relaxes the assumptions on S in exchange for stronger assumptions on R.

source

theorem minpoly.is_integrally_closed_dvd_iff {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [algebra R S] [is_domain S] [no_zero_smul_divisors R S] [is_integrally_closed R] [nontrivial R] {s : S} (hs : is_integral R s) (p : polynomial R) :

⇑(polynomial.aeval s) p = 0 ↔ minpoly R s ∣ p

source

theorem minpoly.ker_eval {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [algebra R S] [is_domain S] [no_zero_smul_divisors R S] [is_integrally_closed R] {s : S} (hs : is_integral R s) :

ring_hom.ker (polynomial.aeval s).to_ring_hom = ideal.span {minpoly R s}

source

theorem minpoly.is_integrally_closed.degree_le_of_ne_zero {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [algebra R S] [is_domain S] [no_zero_smul_divisors R S] [is_integrally_closed R] {s : S} (hs : is_integral R s) {p : polynomial R} (hp0 : p ≠ 0) (hp : ⇑(polynomial.aeval s) p = 0) :

(minpoly R s).degree ≤ p.degree

If an element x is a root of a nonzero polynomial p, then the degree of p is at least the degree of the minimal polynomial of x. See also minpoly.degree_le_of_ne_zero which relaxes the assumptions on S in exchange for stronger assumptions on R.

source

theorem minpoly.is_integrally_closed.minpoly.unique {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [algebra R S] [is_domain S] [no_zero_smul_divisors R S] [is_integrally_closed R] {s : S} {P : polynomial R} (hmo : P.monic) (hP : ⇑(polynomial.aeval s) P = 0) (Pmin : ∀ (Q : polynomial R), Q.monic → ⇑(polynomial.aeval s) Q = 0 → P.degree ≤ Q.degree) :

P = minpoly R s

The minimal polynomial of an element x is uniquely characterized by its defining property: if there is another monic polynomial of minimal degree that has x as a root, then this polynomial is equal to the minimal polynomial of x. See also minpoly.unique which relaxes the assumptions on S in exchange for stronger assumptions on R.

source

theorem minpoly.prime_of_is_integrally_closed {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [algebra R S] [is_domain S] [no_zero_smul_divisors R S] [is_integrally_closed R] {x : S} (hx : is_integral R x) :

prime (minpoly R x)

source

theorem minpoly.to_adjoin.injective {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [algebra R S] [is_domain S] [no_zero_smul_divisors R S] [is_integrally_closed R] {x : S} (hx : is_integral R x) :

function.injective ⇑(adjoin_root.minpoly.to_adjoin R x)

source

@[simp]

theorem minpoly.equiv_adjoin_symm_apply {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [algebra R S] [is_domain S] [no_zero_smul_divisors R S] [is_integrally_closed R] {x : S} (hx : is_integral R x) (ᾰ : ↥(algebra.adjoin R {x})) :

⇑((minpoly.equiv_adjoin hx).symm) ᾰ = ⇑((ring_equiv.of_bijective ↑(adjoin_root.minpoly.to_adjoin R x) _).symm) ᾰ

source

noncomputable def minpoly.equiv_adjoin {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [algebra R S] [is_domain S] [no_zero_smul_divisors R S] [is_integrally_closed R] {x : S} (hx : is_integral R x) :

adjoin_root (minpoly R x) ≃ₐ[R] ↥(algebra.adjoin R {x})

The algebra isomorphism adjoin_root (minpoly R x) ≃ₐ[R] adjoin R x

Equations

minpoly.equiv_adjoin hx = alg_equiv.of_bijective (adjoin_root.minpoly.to_adjoin R x) _

source

@[simp]

theorem minpoly.equiv_adjoin_apply {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [algebra R S] [is_domain S] [no_zero_smul_divisors R S] [is_integrally_closed R] {x : S} (hx : is_integral R x) (ᾰ : adjoin_root (minpoly R x)) :

⇑(minpoly.equiv_adjoin hx) ᾰ = ⇑(adjoin_root.lift (algebra_map R ↥(algebra.adjoin R {x})) ⟨x, _⟩ _) ᾰ

source

@[simp]

theorem algebra.adjoin.power_basis'_dim {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [algebra R S] [is_domain S] [no_zero_smul_divisors R S] [is_integrally_closed R] {x : S} (hx : is_integral R x) :

(algebra.adjoin.power_basis' hx).dim = (minpoly R x).nat_degree

source

@[simp]

theorem algebra.adjoin.power_basis'_gen {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [algebra R S] [is_domain S] [no_zero_smul_divisors R S] [is_integrally_closed R] {x : S} (hx : is_integral R x) :

(algebra.adjoin.power_basis' hx).gen = ⟨x, _⟩

source

noncomputable def algebra.adjoin.power_basis' {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [algebra R S] [is_domain S] [no_zero_smul_divisors R S] [is_integrally_closed R] {x : S} (hx : is_integral R x) :

power_basis R ↥(algebra.adjoin R {x})

The power_basis of adjoin R {x} given by x. See algebra.adjoin.power_basis for a version over a field.

Equations

algebra.adjoin.power_basis' hx = (adjoin_root.power_basis' _).map (minpoly.equiv_adjoin hx)

source

@[simp]

theorem power_basis.of_gen_mem_adjoin'_gen {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [algebra R S] [is_domain S] [no_zero_smul_divisors R S] [is_integrally_closed R] {x : S} (B : power_basis R S) (hint : is_integral R x) (hx : B.gen ∈ algebra.adjoin R {x}) :

(B.of_gen_mem_adjoin' hint hx).gen = x

source

noncomputable def power_basis.of_gen_mem_adjoin' {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [algebra R S] [is_domain S] [no_zero_smul_divisors R S] [is_integrally_closed R] {x : S} (B : power_basis R S) (hint : is_integral R x) (hx : B.gen ∈ algebra.adjoin R {x}) :

power_basis R S

The power basis given by x if B.gen ∈ adjoin R {x}.

Equations

B.of_gen_mem_adjoin' hint hx = (algebra.adjoin.power_basis' hint).map (((algebra.adjoin R {x}).equiv_of_eq ⊤ _).trans subalgebra.top_equiv)

source

@[simp]

theorem power_basis.of_gen_mem_adjoin'_dim {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [algebra R S] [is_domain S] [no_zero_smul_divisors R S] [is_integrally_closed R] {x : S} (B : power_basis R S) (hint : is_integral R x) (hx : B.gen ∈ algebra.adjoin R {x}) :

(B.of_gen_mem_adjoin' hint hx).dim = (minpoly R x).nat_degree