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.

• minpoly.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} [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] [Field 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.

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.

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] [Nontrivial 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.

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] [Nontrivial R] {s : S} (hs : IsIntegral R s) (p : Polynomial R) : ↑(Polynomial.aeval s) p = 0 ↔ minpoly R s ∣ p

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) = Ideal.span {minpoly R s}

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} (hs : IsIntegral R s) {p : Polynomial R} (hp0 : p ≠ 0) (hp : ↑(Polynomial.aeval s) p = 0) : Polynomial.degree (minpoly R s) ≤ Polynomial.degree p

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} [CommRing R] [CommRing S] [IsDomain R] [Algebra R S] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {s : S} {P : Polynomial R} (hmo : Polynomial.Monic P) (hP : ↑(Polynomial.aeval s) P = 0) (Pmin : ∀ (Q : Polynomial R), Polynomial.Monic Q → ↑(Polynomial.aeval s) Q = 0 → Polynomial.degree P ≤ Polynomial.degree Q) : 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} [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)

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)

@[simp]

theorem minpoly.equivAdjoin_symm_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) : ∀ (a : { x // x ∈ Algebra.adjoin R {x} }), ↑(AlgEquiv.symm (minpoly.equivAdjoin hx)) a = ↑(Equiv.ofBijective ↑(AdjoinRoot.Minpoly.toAdjoin R x) (_ : Function.Injective ↑(AdjoinRoot.Minpoly.toAdjoin R x) ∧ Function.Surjective ↑(AdjoinRoot.Minpoly.toAdjoin R x))).symm a

@[simp]

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) : ∀ (a : AdjoinRoot (minpoly R x)), ↑(minpoly.equivAdjoin hx) a = ↑(QuotientAddGroup.lift (Submodule.toAddSubgroup (Ideal.span {minpoly R x})) ↑(Polynomial.eval₂RingHom (algebraMap R { x // x ∈ Algebra.adjoin R {x} }) { val := x, property := (_ : x ∈ Algebra.adjoin R {x}) }) (_ : ∀ (g : Polynomial R), g ∈ Ideal.span {minpoly R x} → ↑(Polynomial.eval₂RingHom (algebraMap R { x // x ∈ Algebra.adjoin R {x} }) { val := x, property := (_ : x ∈ Algebra.adjoin R {x}) }) g = 0)) a

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] { x // x ∈ Algebra.adjoin R {x} }

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

Equations

• One or more equations did not get rendered due to their size.

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 { x // x ∈ Algebra.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 = PowerBasis.map (AdjoinRoot.powerBasis' (_ : Polynomial.Monic (minpoly R x))) (minpoly.equivAdjoin hx)

@[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) : (Algebra.adjoin.powerBasis' hx).dim = Polynomial.natDegree (minpoly R x)

@[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) : (Algebra.adjoin.powerBasis' hx).gen = { val := x, property := (_ : x ∈ Algebra.adjoin R {x}) }

noncomputable 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} (B : PowerBasis R S) (hint : IsIntegral R x) (hx : B.gen ∈ Algebra.adjoin R {x}) : PowerBasis R S

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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} (B : PowerBasis R S) (hint : IsIntegral R x) (hx : B.gen ∈ Algebra.adjoin R {x}) : (PowerBasis.ofGenMemAdjoin' B hint hx).dim = Polynomial.natDegree (minpoly R x)

@[simp]

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} (B : PowerBasis R S) (hint : IsIntegral R x) (hx : B.gen ∈ Algebra.adjoin R {x}) : (PowerBasis.ofGenMemAdjoin' B hint hx).gen = x