English
In an integrally closed context, the kernel of evaluation at an integral element equals the ideal generated by its minimal polynomial.
Русский
В интегрально закрытом контексте ядро отображения на интегральный элемент равно идеалу, порождённому минимальным полиномом.
LaTeX
$$$\ker(\operatorname{aeval}_s) = \langle minpoly_R(s) \rangle$$$
Lean4
/-- 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 isIntegrallyClosed_dvd {s : S} (hs : IsIntegral R s) {p : R[X]} (hp : Polynomial.aeval s p = 0) :
minpoly R s ∣ p := by
let K := FractionRing R
let L := FractionRing S
let _ : Algebra K L := FractionRing.liftAlgebra R L
have : minpoly K (algebraMap S L s) ∣ map (algebraMap R K) (p %ₘ minpoly R s) :=
by
rw [map_modByMonic _ (minpoly.monic hs), modByMonic_eq_sub_mul_div]
· refine dvd_sub (minpoly.dvd K (algebraMap S L s) ?_) ?_
· rw [← map_aeval_eq_aeval_map, hp, map_zero]
rw [← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
apply dvd_mul_of_dvd_left
rw [isIntegrallyClosed_eq_field_fractions K L hs]
exact Monic.map _ (minpoly.monic hs)
rw [isIntegrallyClosed_eq_field_fractions _ _ hs,
map_dvd_map (algebraMap R K) (IsFractionRing.injective R K) (minpoly.monic hs)] at this
rw [← modByMonic_eq_zero_iff_dvd (minpoly.monic hs)]
exact Polynomial.eq_zero_of_dvd_of_degree_lt this (degree_modByMonic_lt p <| minpoly.monic hs)
