English
A domain R is integrally closed if and only if Gauss's lemma holds for monic polynomials: for every monic p ∈ R[X], p is irreducible in R[X] iff p.map(algebraMap R K) is irreducible in K[X], for any field K with IsFractionRing R K.
Русский
Домена R интегрально замкнут — тогда и только тогда выполняется лемма Гаусса: для любой моноичной полиномиальной функции p ∈ R[X] неприводимость p совпадает с неприводимостью map(algebraMap R K)(p) в K[X].
LaTeX
$$$[IsDomain\ R] \\Rightarrow (IsIntegrallyClosed R \\leftrightarrow \\forall p:\\!R[X],\\, p.Monic \\rightarrow (\\text{Irreducible } p \\leftrightarrow \\text{Irreducible } (p.map(\\mathrm{algebraMap} R K))))$$$
Lean4
/-- Integrally closed domains are precisely the domains for in which Gauss's lemma holds
for monic polynomials -/
theorem isIntegrallyClosed_iff' [IsDomain R] :
IsIntegrallyClosed R ↔ ∀ p : R[X], p.Monic → (Irreducible p ↔ Irreducible (p.map <| algebraMap R K)) :=
by
constructor
· intro hR p hp; exact Monic.irreducible_iff_irreducible_map_fraction_map hp
· intro H
refine
(isIntegrallyClosed_iff K).mpr fun {x} hx => RingHom.mem_range.mp <| minpoly.mem_range_of_degree_eq_one R x ?_
rw [← Monic.degree_map (minpoly.monic hx) (algebraMap R K)]
apply degree_eq_one_of_irreducible_of_root ((H _ <| minpoly.monic hx).mp (minpoly.irreducible hx))
rw [IsRoot, eval_map, ← aeval_def, minpoly.aeval R x]
