Integrality over ideals

Main results

• Polynomial.exists_monic_aeval_eq_zero_forall_mem_of_mem_map: If S is an integral R-algebra, and I is an ideal of R, then any x ∈ IS is integral over I, i.e. it is a root of some monic polynomial in R[X] whose non-leading coefficients are in I.

Note

We actually prove something stronger, namely that the Xⁿ⁻ⁱ-th coefficient lives in Iⁿ. This the definitition that x is integral over I in https://stacks.math.columbia.edu/tag/00H2.

theorem Polynomial.coeff_mem_pow_of_mem_adjoin_C_mul_X {R : Type u_3} [CommRing R] {I : Ideal R} {P : Polynomial R} (hP : P ∈ Algebra.adjoin R {x : Polynomial R | ∃ r ∈ I, C r * X = x}) (i : ℕ) : P.coeff i ∈ I ^ i

theorem Polynomial.exists_monic_aeval_eq_zero_forall_mem_pow_of_isIntegral {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {I : Ideal R} {x : S} (hx : IsIntegral (↥(Algebra.adjoin R {x : Polynomial R | ∃ r ∈ I, C r * X = x})) (C x * X)) : ∃ (p : Polynomial R), p.Monic ∧ (aeval x) p = 0 ∧ ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)

theorem Polynomial.exists_monic_aeval_eq_zero_forall_mem_pow_of_mem_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] {I : Ideal R} {x : S} (hx : x ∈ Ideal.map (algebraMap R S) I) : ∃ (p : Polynomial R), p.Monic ∧ (aeval x) p = 0 ∧ ∀ (i : ℕ), p.coeff i ∈ I ^ (p.natDegree - i)

theorem Polynomial.exists_monic_aeval_eq_zero_forall_mem_of_mem_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Algebra.IsIntegral R S] {I : Ideal R} {x : S} (hx : x ∈ Ideal.map (algebraMap R S) I) : ∃ (p : Polynomial R), p.Monic ∧ (aeval x) p = 0 ∧ ∀ (i : ℕ), i ≠ p.natDegree → p.coeff i ∈ I

Stacks Tag 00H5