English
Let R be a commutative ring, M a submonoid of R, and S a commutative ring with an R-algebra structure. If x in S is integral over the localization R_M, then there exists m in M such that m · x is integral over R.
Русский
Пусть R — коммутативное кольцо, M — подмножество-моноид R, S — коммутативное кольцо с алгебраическим отображением из R. Если x ∈ S интеграл над локализацией R_M, то существует m ∈ M такое, что m · x интеграл над R.
LaTeX
$$$\exists m \in M,\; \operatorname{IsIntegral}_R(m \cdot x)$$$
Lean4
theorem exists_multiple_integral_of_isLocalization [Algebra Rₘ S] [IsScalarTower R Rₘ S] (x : S)
(hx : IsIntegral Rₘ x) : ∃ m : M, IsIntegral R (m • x) :=
by
rcases subsingleton_or_nontrivial Rₘ with _ | nontriv
· haveI := (_root_.algebraMap Rₘ S).codomain_trivial
exact ⟨1, Polynomial.X, Polynomial.monic_X, Subsingleton.elim _ _⟩
obtain ⟨p, hp₁, hp₂⟩ := hx
have := lifts_and_natDegree_eq_and_monic (IsLocalization.scaleRoots_commonDenom_mem_lifts M p ?_) ?_
· obtain ⟨p', hp'₁, -, hp'₂⟩ := this
refine ⟨IsLocalization.commonDenom M p.support p.coeff, p', hp'₂, ?_⟩
rw [IsScalarTower.algebraMap_eq R Rₘ S, ← Polynomial.eval₂_map, hp'₁, Submonoid.smul_def, Algebra.smul_def,
IsScalarTower.algebraMap_apply R Rₘ S]
exact Polynomial.scaleRoots_eval₂_eq_zero _ hp₂
· rw [hp₁.leadingCoeff]
exact one_mem _
· rwa [Polynomial.monic_scaleRoots_iff]
