English
A ring homomorphism f is surjective on stalks if and only if the localized maps at maximal ideals of the target are surjective: f.SurjectiveOnStalks iff for all maximal ideals I ⊆ S, Localization.localRingHom _ I f rfl is surjective.
Русский
Гомоморфизм колец f существует на всех локализациях по максимальным идеалам: f.SurjectiveOnStalks, если и только если для каждого максимального идеала I в S отображение после локализации является сюръективным.
LaTeX
$$$f\\text{ SurjectiveOnStalks} \\iff \\forall I\\, (I\\text{ maximal in } S),\\ \\text{Localization.localRingHom }_I f\\; \\text{is surjective}$$$
Lean4
/-- A ring homomorphism `R →+* S` is surjective on stalks if `R_p →+* S_q` is surjective for all pairs
of primes `p = f⁻¹(q)`.
-/
def SurjectiveOnStalks (f : R →+* S) : Prop :=
∀ (P : Ideal S) (_ : P.IsPrime), Function.Surjective (Localization.localRingHom _ P f rfl)
