English
If f is integral and M is a submonoid, then the localization map preserves integrality along the target localization.
Русский
Если f - интегральное расширение, то локализация сохраняет интегральность вдоль целевой локализации.
LaTeX
$$$\text{isIntegral_localization'}(f,M)$$$
Lean4
/-- Given a particular witness to an element being algebraic over an algebra `R → S`,
We can localize to a submonoid containing the leading coefficient to make it integral.
Explicitly, the map between the localizations will be an integral ring morphism -/
theorem is_integral_localization_at_leadingCoeff {x : S} (p : R[X]) (hp : aeval x p = 0) (hM : p.leadingCoeff ∈ M) :
(map Sₘ (algebraMap R S) (show _ ≤ (Algebra.algebraMapSubmonoid S M).comap _ from M.le_comap_map) :
Rₘ →+* _).IsIntegralElem
(algebraMap S Sₘ x) :=
haveI : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ :=
inferInstanceAs (IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ)
(algebraMap R S).isIntegralElem_localization_at_leadingCoeff x p hp M hM
