Results about coefficients of polynomials being integral

Main results

• Polynomial.isIntegral_coeff_of_dvd: If a monic polynomial p divides another monic polynomial with integral coefficients, then the coefficients of p are themselves integral.
• IsIntegral.coeff_of_isFractionRing: Let R be a domain with fraction ring K. If p : K[X] is integral over R[X], then the coefficients of p are integral over R.
• We also provide the instance [IsIntegrallyClosed R] : IsIntegrallyClosed R[X].

theorem Polynomial.isIntegral_coeff_prod {R : Type u_1} {S : Type u_2} {ι : Type u_3} [CommRing R] [CommRing S] [Algebra R S] (s : Finset ι) (p : ι → Polynomial S) (H : ∀ i ∈ s, ∀ (j : ℕ), IsIntegral R ((p i).coeff j)) (j : ℕ) : IsIntegral R ((s.prod p).coeff j)

theorem Polynomial.isIntegral_coeff_of_factors {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain S] (p : Polynomial S) (hpmon : IsIntegral R p.leadingCoeff) (hp : p.Splits) (hpr : ∀ x ∈ p.roots, IsIntegral R x) (i : ℕ) : IsIntegral R (p.coeff i)

theorem Polynomial.isIntegral_coeff_of_dvd {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain S] (p : Polynomial R) (q : Polynomial S) (hp : p.Monic) (hq : IsIntegral R q.leadingCoeff) (H : q ∣ map (algebraMap R S) p) (i : ℕ) : IsIntegral R (q.coeff i)

Stacks Tag 00H6 ((1))

theorem IsAlmostIntegral.coeff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsDomain R] [FaithfulSMul R S] {p : Polynomial S} (hp : IsAlmostIntegral (Polynomial R) p) (i : ℕ) : IsAlmostIntegral R (p.coeff i)

Stacks Tag 00H0 ((1))

theorem IsIntegral.coeff_of_exists_smul_mem_lifts {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [FaithfulSMul R S] [IsDomain S] {p : Polynomial S} (hp : IsIntegral (Polynomial R) p) (hp' : ∃ r ∈ nonZeroDivisors R, r • p ∈ Polynomial.lifts (algebraMap R S)) (i : ℕ) : IsIntegral R (p.coeff i)

theorem IsIntegral.coeff_of_isFractionRing {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsFractionRing R S] [IsDomain R] {p : Polynomial S} (hp : IsIntegral (Polynomial R) p) (i : ℕ) : IsIntegral R (p.coeff i)

Stacks Tag 00H0 ((2))

instance instIsIntegrallyClosedPolynomialOfIsDomain {R : Type u_4} [CommRing R] [IsDomain R] [IsIntegrallyClosed R] : IsIntegrallyClosed (Polynomial R)

Stacks Tag 030A