English
If a monic polynomial g lies in an ideal I of S[X], then the image of X in the quotient (S[X]/I) is integral over S.
Русский
Если моноический полином g лежит в идеале I в S[X], то образ X в факторкольце S[X]/I интегрально над S.
LaTeX
$$$\text{Monic}(g) \wedge g \in I \Rightarrow ((\operatorname{Ideal.Quotient.mk_{a}} S I)\circ (\text{algebraMap } S (\operatorname{Polynomial} S))).IsIntegralElem(\operatorname{RingHom}.coe (\operatorname{Ideal.Quotient.mk I}) X)$$$
Lean4
theorem quotient_isIntegral {g : S[X]} (mon : g.Monic) {I : Ideal S[X]} (h : g ∈ I) :
((Ideal.Quotient.mkₐ S I).comp (Algebra.ofId S S[X])).IsIntegral :=
by
have eq_top : Algebra.adjoin S {(Ideal.Quotient.mkₐ S I) X} = ⊤ :=
by
ext g
constructor
· simp only [Algebra.mem_top, implies_true]
· intro _
obtain ⟨g', hg⟩ := Ideal.Quotient.mkₐ_surjective S I g
have : g = (Polynomial.aeval ((Ideal.Quotient.mkₐ S I) X)) g' :=
by
nth_rw 1 [← hg, aeval_eq_sum_range' (lt_add_one _), as_sum_range_C_mul_X_pow g', map_sum]
simp only [Polynomial.C_mul', ← map_pow, map_smul]
exact this ▸ (aeval_mem_adjoin_singleton S ((Ideal.Quotient.mk I) Polynomial.X))
exact fun a ↦ (eq_top ▸ adjoin_le_integralClosure <| mon.quotient_isIntegralElem h) Algebra.mem_top
