English
For a ring hom f: R → S, f.SurjectiveOnStalks is equivalent to a local criterion: for every ideal I ⊊ S, and every s ∈ S, there exist x, r ∈ R and c ∈ S with c ∉ I and f(r) ∉ I such that c f(r) s = c f(x).
Русский
Для гомоморфизма колец f: R → S условие сюръективности на стека эквивалентно локальному критерию: для каждого идеала I ⊊ S и для каждого s ∈ S существуют x, r ∈ R и c ∈ S с c ∉ I, f(r) ∉ I и c f(r) s = c f(x).
LaTeX
$$$f.SurjectiveOnStalks \\;\\iff\\; \\forall I:\\text{Ideal}(S),\\ I \\neq \\top \\to \\forall s \\in S,\\ \\exists x,r \\in R,\\exists c \\in S\\setminus I,\\ f(r) \\notin I \\land c f(r) s = c f(x)$$$
Lean4
theorem surjectiveOnStalks_iff_forall_ideal :
f.SurjectiveOnStalks ↔ ∀ I : Ideal S, I ≠ ⊤ → ∀ s : S, ∃ x r : R, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x :=
by
simp_rw [SurjectiveOnStalks, surjective_localRingHom_iff]
refine ⟨fun H I hI s ↦ ?_, fun H I hI ↦ H I hI.ne_top⟩
obtain ⟨M, hM, hIM⟩ := I.exists_le_maximal hI
obtain ⟨x, r, c, hc, hr, e⟩ := H M hM.isPrime s
exact ⟨x, r, c, fun h ↦ hc (hIM h), fun h ↦ hr (hIM h), e⟩
