English
Let R be a maximal local subring of a field K. If x is integral over R, then x lies in R.
Русский
Пусть R — максимальное локальное подкольцо над полем K. Если элемент x ∈ K является интегралом над R, то x принадлежит R.
LaTeX
$$$\\text{IsMax}(R^{\\mathrm{toLocalSubring}}) \\Rightarrow \\forall x \\in K, \\; \\text{IsIntegral}(R^{\\mathrm{toSubring}}(x)) \\Rightarrow x \\in R^{\\mathrm{toSubring}}.$$$
Lean4
@[stacks 00IC]
theorem mem_of_isMax_of_isIntegral {R : LocalSubring K} (hR : IsMax R) {x : K} (hx : IsIntegral R.toSubring x) :
x ∈ R.toSubring := by
let S := Algebra.adjoin R.toSubring { x }
have : Algebra.IsIntegral R.toSubring S := Algebra.IsIntegral.adjoin (by simpa)
have : FaithfulSMul R.toSubring S := NoZeroSMulDivisors.instFaithfulSMulOfNontrivial
obtain ⟨Q : Ideal S.toSubring, hQ, e⟩ :=
Ideal.exists_ideal_over_maximal_of_isIntegral (R := R.toSubring) (S := S) (maximalIdeal _)
(le_maximalIdeal (by simp))
have : R = .ofPrime S.toSubring Q :=
by
have hRS : R.toSubring ≤ S.toSubring := fun r hr ↦ algebraMap_mem S ⟨r, hr⟩
apply hR.eq_of_le ⟨hRS.trans (LocalSubring.le_ofPrime _ _), ⟨?_⟩⟩
intro r hr
have := (IsLocalization.AtPrime.isUnit_to_map_iff (R := S.toSubring) _ Q ⟨_, hRS r.2⟩).mp hr
by_contra h
rw [← mem_nonunits_iff, ← mem_maximalIdeal, ← e] at h
exact this h
rw [this]
exact LocalSubring.le_ofPrime _ _ (Algebra.self_mem_adjoin_singleton _ _)
