English
If f: R →+* S is surjective and P is a prime ideal of S, then the localized map R_{f^{-1}(P)} →+* S_P is surjective.
Русский
Если f: R →+* S сюръективен и P — простая идеал S, то локализованная карта R_{f^{-1}(P)} →+* S_P сюръективна.
LaTeX
$$$$ \forall (f : R \to+* S), \; \mathrm{Surjective}(f) \Rightarrow \forall P [P.IsPrime], \; \mathrm{Surjective}( \operatorname{Localization.localRingHom} (P.comap f) P f ). $$$$
Lean4
/-- A surjective ring homomorphism `R →+* S` induces a surjective homomorphism `R_{f⁻¹(P)} →+* S_P`
for every prime ideal `P` of `S`. -/
theorem surjective_localRingHom_of_surjective {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S)
(h : Function.Surjective f) (P : Ideal S) [P.IsPrime] :
Function.Surjective (Localization.localRingHom (P.comap f) P f rfl) :=
have : IsLocalization (Submonoid.map f (Ideal.comap f P).primeCompl) (Localization.AtPrime P) :=
(Submonoid.map_comap_eq_of_surjective h P.primeCompl).symm ▸ Localization.isLocalization
surjective_localizationPreserves _ _ _ _ h
