# 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`.

source
theorem minpoly.isIntegrallyClosed_eq_field_fractions {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] (K : Type u_3) (L : Type u_4) [Field K] [Algebra R K] [IsFractionRing R K] [CommRing L] [Nontrivial L] [Algebra R L] [Algebra S L] [Algebra K L] [IsScalarTower R K L] [IsScalarTower R S L] [IsIntegrallyClosed R] [IsDomain S] {s : S} (hs : IsIntegral R s) :
minpoly K ((algebraMap S L) s) = Polynomial.map (algebraMap 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.isIntegrallyClosed_eq_field_fractions'` if `S` is already a `K`-algebra.

source
theorem minpoly.isIntegrallyClosed_eq_field_fractions' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] (K : Type u_3) [Field K] [Algebra R K] [IsFractionRing R K] [IsIntegrallyClosed R] [IsDomain S] [Algebra K S] [IsScalarTower R K S] {s : S} (hs : IsIntegral R s) :
minpoly K s = Polynomial.map (algebraMap 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.isIntegrallyClosed_eq_field_fractions`, this version is useful if the element is in a ring that is already a `K`-algebra.

source
theorem minpoly.isIntegrallyClosed_dvd {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {s : S} (hs : IsIntegral 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.isIntegrallyClosed_dvd_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {s : S} (hs : IsIntegral 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} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {s : S} (hs : IsIntegral R s) :
RingHom.ker (Polynomial.aeval s).toRingHom = Ideal.span {minpoly R s}
source
theorem minpoly.IsIntegrallyClosed.degree_le_of_ne_zero {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {s : 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 IsIntegrallyClosed.minpoly.unique {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed 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.IsIntegrallyClosed.unique_of_degree_le_degree_minpoly {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {s : S} {p : Polynomial R} (hmo : p.Monic) (hp : (Polynomial.aeval s) p = 0) (pmin : p.degree ≤ (minpoly R s).degree) :
p = minpoly R s
source
theorem minpoly.IsIntegrallyClosed.isIntegral_iff_leadingCoeff_dvd {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {s : S} {p : Polynomial R} (hp : (Polynomial.aeval s) p = 0) (h₀ : p ≠ 0) (pmin : ∀ (q : Polynomial R), q.Monic → (Polynomial.aeval s) q = 0 → p.degree ≤ q.degree) :
IsIntegral R s ↔ Polynomial.C p.leadingCoeff ∣ p
source
theorem minpoly.prime_of_isIntegrallyClosed {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {x : S} (hx : IsIntegral R x) :
Prime (minpoly R x)
source
theorem minpoly.ToAdjoin.injective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {x : S} (hx : IsIntegral R x) :
Function.Injective ⇑(AdjoinRoot.Minpoly.toAdjoin R x)
source
def minpoly.equivAdjoin {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {x : S} (hx : IsIntegral R x) :
AdjoinRoot (minpoly R x) ≃ₐ[R] ↥(Algebra.adjoin R {x})

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

Equations

- minpoly.equivAdjoin hx = AlgEquiv.ofBijective (AdjoinRoot.Minpoly.toAdjoin R x) ⋯

Instances For

source
@[simp]
theorem minpoly.equivAdjoin_toAlgHom {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {x : S} (hx : IsIntegral R x) :
↑(equivAdjoin hx) = AdjoinRoot.Minpoly.toAdjoin R x
source
@[simp]
theorem minpoly.coe_equivAdjoin {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {x : S} (hx : IsIntegral R x) :
⇑(equivAdjoin hx) = ⇑(AdjoinRoot.Minpoly.toAdjoin R x)
source
@[deprecated minpoly.coe_equivAdjoin (since := "2025-07-21")]
theorem minpoly.equivAdjoin_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {x : S} (hx : IsIntegral R x) :
⇑(equivAdjoin hx) = ⇑(AdjoinRoot.Minpoly.toAdjoin R x)

Alias of `minpoly.coe_equivAdjoin`.

source
def Algebra.adjoin.powerBasis' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {x : S} (hx : IsIntegral R x) :
PowerBasis R ↥(adjoin R {x})

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

Equations

- Algebra.adjoin.powerBasis' hx = (AdjoinRoot.powerBasis' ⋯).map (minpoly.equivAdjoin hx)

Instances For

source
@[simp]
theorem Algebra.adjoin.powerBasis'_dim {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {x : S} (hx : IsIntegral R x) :
(powerBasis' hx).dim = (minpoly R x).natDegree
source
@[simp]
theorem Algebra.adjoin.powerBasis'_gen {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {x : S} (hx : IsIntegral R x) :
(powerBasis' hx).gen = ⟨x, ⋯⟩
source
noncomputable def PowerBasis.ofAdjoinEqTop' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {x : S} (hx : IsIntegral R x) (hx' : Algebra.adjoin R {x} = ⊤) :
PowerBasis R S

If `x` generates `S` over `R` and is integral over `R`, then it defines a power basis. See `PowerBasis.ofAdjoinEqTop` for a version over a field.

Equations

- PowerBasis.ofAdjoinEqTop' hx hx' = (Algebra.adjoin.powerBasis' hx).map (((Algebra.adjoin R {x}).equivOfEq ⊤ hx').trans Subalgebra.topEquiv)

Instances For

source
@[deprecated PowerBasis.ofAdjoinEqTop' "Use in combination with `PowerBasis.adjoin_eq_top_of_gen_mem_adjoin` to recover the deprecated definition" (since := "2025-09-28")]
def PowerBasis.ofGenMemAdjoin' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {x : S} (hx : IsIntegral R x) (hx' : Algebra.adjoin R {x} = ⊤) :
PowerBasis R S

Alias of `PowerBasis.ofAdjoinEqTop'`.

If `x` generates `S` over `R` and is integral over `R`, then it defines a power basis. See `PowerBasis.ofAdjoinEqTop` for a version over a field.

Equations

- @PowerBasis.ofGenMemAdjoin' = @PowerBasis.ofAdjoinEqTop'

Instances For

source
@[simp]
theorem PowerBasis.ofAdjoinEqTop'_dim {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {x : S} (hx : IsIntegral R x) (hx' : Algebra.adjoin R {x} = ⊤) :
(ofAdjoinEqTop' hx hx').dim = (minpoly R x).natDegree
source
@[simp]
theorem PowerBasis.ofAdjoinEqTop'_gen {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {x : S} (hx : IsIntegral R x) (hx' : Algebra.adjoin R {x} = ⊤) :
(ofAdjoinEqTop' hx hx').gen = x
source
@[deprecated PowerBasis.ofAdjoinEqTop'_dim "Use in combination with `PowerBasis.adjoin_eq_top_of_gen_mem_adjoin` to recover the deprecated definition" (since := "2025-09-28")]
theorem PowerBasis.ofGenMemAdjoin'_dim {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {x : S} (hx : IsIntegral R x) (hx' : Algebra.adjoin R {x} = ⊤) :
(ofAdjoinEqTop' hx hx').dim = (minpoly R x).natDegree

Alias of `PowerBasis.ofAdjoinEqTop'_dim`.

source
@[deprecated PowerBasis.ofAdjoinEqTop'_gen "Use in combination with `PowerBasis.adjoin_eq_top_of_gen_mem_adjoin` to recover the deprecated definition" (since := "2025-09-28")]
theorem PowerBasis.ofGenMemAdjoin'_gen {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {x : S} (hx : IsIntegral R x) (hx' : Algebra.adjoin R {x} = ⊤) :
(ofAdjoinEqTop' hx hx').gen = x

Alias of `PowerBasis.ofAdjoinEqTop'_gen`.

source
instance minpoly.instAlgebraSubtypeMemSubringSubalgebraIntegralClosure {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (A : Subring K) :
Algebra ↥A ↥(integralClosure (↥A) L)
Equations

- minpoly.instAlgebraSubtypeMemSubringSubalgebraIntegralClosure A = (integralClosure (↥A) L).algebra

source
instance minpoly.instSMulSubtypeMemSubringSubalgebraIntegralClosure {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (A : Subring K) :
SMul ↥A ↥(integralClosure (↥A) L)
Equations

- minpoly.instSMulSubtypeMemSubringSubalgebraIntegralClosure A = (minpoly.instAlgebraSubtypeMemSubringSubalgebraIntegralClosure A).toSMul

source
instance minpoly.instIsScalarTowerSubtypeMemSubringSubalgebraIntegralClosure {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (A : Subring K) :
IsScalarTower (↥A) (↥(integralClosure (↥A) L)) L
source
theorem minpoly.ofSubring {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (A : Subring K) [IsIntegrallyClosed ↥A] [IsFractionRing (↥A) K] (x : ↥(integralClosure (↥A) L)) :
Polynomial.map (algebraMap (↥A) K) (minpoly (↥A) x) = minpoly K ↑x

The minimal polynomial of `x : L` over `K` agrees with its minimal polynomial over the integrally closed subring `A`.