# Minimal polynomials over a GCD monoid #

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

## Main results #

• minpoly.isIntegrallyClosed_eq_field_fractions: For integrally closed domains, the minimal polynomial over the ring is the same as the minimal polynomial over the fraction field.

• minpoly.isIntegrallyClosed_dvd : For integrally closed domains, the minimal polynomial divides any primitive polynomial that has the integral element as root.

• IsIntegrallyClosed.Minpoly.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.isIntegrallyClosed_eq_field_fractions {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] (K : Type u_3) (L : Type u_4) [] [Algebra R K] [] [] [] [Algebra R L] [Algebra S L] [Algebra K L] [] [] [] {s : S} (hs : ) :

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

theorem minpoly.isIntegrallyClosed_eq_field_fractions' {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] (K : Type u_3) [] [Algebra R K] [] [] [Algebra K S] [] {s : S} (hs : ) :

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

theorem minpoly.isIntegrallyClosed_dvd {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] [] [] {s : S} (hs : ) {p : } (hp : 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.

theorem minpoly.isIntegrallyClosed_dvd_iff {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] [] [] {s : S} (hs : ) (p : ) :
p = 0 minpoly R s p
theorem minpoly.ker_eval {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] [] [] {s : S} (hs : ) :
RingHom.ker .toRingHom = Ideal.span {minpoly R s}
theorem minpoly.IsIntegrallyClosed.degree_le_of_ne_zero {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] [] [] {s : S} (hs : ) {p : } (hp0 : p 0) (hp : 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.

theorem IsIntegrallyClosed.minpoly.unique {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] [] [] {s : S} {P : } (hmo : P.Monic) (hP : P = 0) (Pmin : ∀ (Q : ), Q.Monic Q = 0P.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.

theorem minpoly.prime_of_isIntegrallyClosed {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] [] [] {x : S} (hx : ) :
theorem minpoly.ToAdjoin.injective {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] [] [] {x : S} (hx : ) :
@[simp]
theorem minpoly.equivAdjoin_symm_apply {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] [] [] {x : S} (hx : ) (b : (Algebra.adjoin R {x})) :
.symm b =
@[simp]
theorem minpoly.equivAdjoin_apply {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] [] [] {x : S} (hx : ) (a : AdjoinRoot (minpoly R x)) :
def minpoly.equivAdjoin {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] [] [] {x : S} (hx : ) :

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

Equations
Instances For
def Algebra.adjoin.powerBasis' {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] [] [] {x : S} (hx : ) :

The PowerBasis of adjoin R {x} given by x. See Algebra.adjoin.powerBasis for a version over a field.

Equations
• = .map
Instances For
@[simp]
theorem Algebra.adjoin.powerBasis'_dim {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] [] [] {x : S} (hx : ) :
.dim = (minpoly R x).natDegree
@[simp]
theorem Algebra.adjoin.powerBasis'_gen {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] [] [] {x : S} (hx : ) :
.gen = x,
noncomputable def PowerBasis.ofGenMemAdjoin' {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] [] [] {x : S} (B : ) (hint : ) (hx : B.gen Algebra.adjoin R {x}) :

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

Equations
• B.ofGenMemAdjoin' hint hx = .map (((Algebra.adjoin R {x}).equivOfEq ).trans Subalgebra.topEquiv)
Instances For
@[simp]
theorem PowerBasis.ofGenMemAdjoin'_dim {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] [] [] {x : S} (B : ) (hint : ) (hx : B.gen Algebra.adjoin R {x}) :
(B.ofGenMemAdjoin' hint hx).dim = (minpoly R x).natDegree
@[simp]
theorem PowerBasis.ofGenMemAdjoin'_gen {R : Type u_1} {S : Type u_2} [] [] [] [Algebra R S] [] [] {x : S} (B : ) (hint : ) (hx : B.gen Algebra.adjoin R {x}) :
(B.ofGenMemAdjoin' hint hx).gen = x