The kernel of R[T] → S, T ↦ ξ, for an integrally closed base

Let R be an integrally closed domain, S a domain and f : R →+* S injective. If ξ ∈ S is a root of a monic irreducible Q ∈ R[T], then Q is the minimal polynomial of ξ over R and every H ∈ R[T] with H(ξ) = 0 is divisible by Q: Mathlib's minpoly.isIntegrallyClosed_dvd (the minimal polynomial over an integrally closed domain divides every annihilating polynomial), a consequence of Gauss's lemma. In the parametrization theorem [Fre17, Ch. I, 8.3] this identifies the kernel of 𝒪_d[T] → 𝒪_n/P', T ↦ X_{i₀}, with (Q): the base 𝒪_d is a unique factorization domain (UFD.lean), hence integrally closed, and 𝒪_n/P' is a domain into which 𝒪_d embeds (the injectivity of the Noether normalization).

Stated with a ring map (Polynomial.eval₂ f), for the same reason as in PrimitiveRelations.lean: the S it is applied to is a quotient of 𝒪_n, and the R-algebra structure is introduced only locally, inside the proof.

theorem Analytic.dvd_of_eval₂_eq_zero_of_monic_irreducible {R : Type u_1} {S : Type u_2} [CommRing R] [IsDomain R] [IsIntegrallyClosed R] [CommRing S] [IsDomain S] (f : R →+* S) (hinj : Function.Injective ⇑f) {ξ : S} {Q : Polynomial R} (hQ : Q.Monic) (hQirr : Irreducible Q) (hQξ : Polynomial.eval₂ f ξ Q = 0) {H : Polynomial R} (hHξ : Polynomial.eval₂ f ξ H = 0) : Q ∣ H

Over an integrally closed domain R embedded in a domain S by f, a monic irreducible Q ∈ R[T] with root ξ divides every H ∈ R[T] vanishing at ξ (Gauss's lemma through Mathlib's minpoly.isIntegrallyClosed_dvd).