English
If a polynomial p over R evaluates to zero at x under f, and the leading coefficient of p lies in M, then the image of x in the localized ring is integral over the localization.
Русский
Если p над R при вычислении даёт 0 в x, и ведущий коэффициент p лежит в M, то образ x в локализации является интегралом над локализацией.
LaTeX
$$$ (map S_m f M.le_comap_map).IsIntegralElem( algebraMap S S_m x)$ under given assumptions$$
Lean4
theorem isIntegralElem_localization_at_leadingCoeff {R S : Type*} [CommSemiring R] [CommSemiring S] (f : R →+* S)
(x : S) (p : R[X]) (hf : p.eval₂ f x = 0) (M : Submonoid R) (hM : p.leadingCoeff ∈ M) {Rₘ Sₘ : Type*} [CommRing Rₘ]
[CommRing Sₘ] [Algebra R Rₘ] [IsLocalization M Rₘ] [Algebra S Sₘ] [IsLocalization (M.map f : Submonoid S) Sₘ] :
(map Sₘ f M.le_comap_map : Rₘ →+* _).IsIntegralElem (algebraMap S Sₘ x) :=
by
by_cases triv : (1 : Rₘ) = 0
· exact ⟨0, ⟨_root_.trans leadingCoeff_zero triv.symm, eval₂_zero _ _⟩⟩
haveI : Nontrivial Rₘ := nontrivial_of_ne 1 0 triv
obtain ⟨b, hb⟩ := isUnit_iff_exists_inv.mp (map_units Rₘ ⟨p.leadingCoeff, hM⟩)
refine ⟨p.map (algebraMap R Rₘ) * C b, ⟨?_, ?_⟩⟩
· refine monic_mul_C_of_leadingCoeff_mul_eq_one ?_
rwa [leadingCoeff_map_of_leadingCoeff_ne_zero (algebraMap R Rₘ)]
refine fun hfp => zero_ne_one (_root_.trans (zero_mul b).symm (hfp ▸ hb) : (0 : Rₘ) = 1)
· refine eval₂_mul_eq_zero_of_left _ _ _ ?_
rw [eval₂_map, IsLocalization.map_comp, ← hom_eval₂ _ f (algebraMap S Sₘ) x]
exact _root_.trans (congr_arg (algebraMap S Sₘ) hf) (RingHom.map_zero _)
