Skip to content

Minimal polynomials and integrality

3 fully proved

Minimal polynomials

TheoremIntegrality via a lift of the minimal polynomial#✓fully proved

Let \(R\) be an integrally closed domain with fraction field \(K\), and let \(L\) be a field extension of \(K\) that is also an \(R\)-algebra, with the \(R\)-algebra structure on \(L\) the composite of \(R \to K\) and \(K \to L\). An element \(x \in L\) that is algebraic over \(K\) is integral over \(R\) if and only if the minimal polynomial of \(x\) over \(K\) is the image of a polynomial in \(R[X]\) under the map \(R[X] \to K[X]\) that applies \(R \to K\) to each coefficient.

theorem isIntegral_iff_mem_lifts {x : L} (hx : IsAlgebraic K x) :
    IsIntegral R x ↔ minpoly K x ∈ Polynomial.lifts (algebraMap R K)
Used by 1
Used byIntegrality via the coefficients of the minimal polynomial

TheoremIntegrality via the coefficients of the minimal polynomial#✓fully proved

Let \(R\) be an integrally closed domain with fraction field \(K\), and let \(L\) be a field extension of \(K\) that is also an \(R\)-algebra, with the \(R\)-algebra structure on \(L\) the composite of \(R \to K\) and \(K \to L\). An element \(x \in L\) that is algebraic over \(K\) is integral over \(R\) if and only if every coefficient of the minimal polynomial of \(x\) over \(K\) lies in the image of \(R\) in \(K\).

theorem isIntegral_iff_coeff_mem_range {x : L} (hx : IsAlgebraic K x) :
    IsIntegral R x ↔ ∀ n, (minpoly K x).coeff n ∈ Set.range (algebraMap R K)
Uses 1 · Used by 1
Proof usesIntegrality via a lift of the minimal polynomial
Used byIntegrality via equality of minimal polynomials

Integrally closed domains

TheoremIntegrality via equality of minimal polynomials#✓fully proved

Let \(A\) be an integrally closed domain with fraction field \(K\), and let \(L\) be a field extension of \(K\) that is also an \(A\)-algebra, with the \(A\)-algebra structure on \(L\) the composite of \(A \to K\) and \(K \to L\). An element \(\alpha \in L\) that is integral over \(K\) is integral over \(A\) if and only if the minimal polynomial of \(\alpha\) over \(K\) equals the image of the minimal polynomial of \(\alpha\) over \(A\) under the map \(A[X] \to K[X]\) that applies \(A \to K\) to each coefficient. Here the minimal polynomial of \(\alpha\) over \(A\) is taken to be \(0\) when \(\alpha\) is not integral over \(A\).

theorem minpoly_eq_map_iff_isIntegral
    {A : Type*} [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
    {K : Type*} [Field K] [Algebra A K] [IsFractionRing A K]
    {L : Type*} [Field L] [Algebra K L] [Algebra A L] [IsScalarTower A K L]
    {α : L} (hα : IsIntegral K α) :
    minpoly K α = (minpoly A α).map (algebraMap A K) ↔ IsIntegral A α
Sources
  • Proposition 1.28, in equality form.
Uses 1
Proof usesIntegrality via the coefficients of the minimal polynomial

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.