English
For a ring hom f, surjectivity on stalks is equivalent to surjectivity on localizations at all maximal ideals: f.SurjectiveOnStalks iff ∀ I ⊆ S, I.IsMaximal → Function.Surjective (Localization.localRingHom _ I f rfl).
Русский
Для гомоморфизма f условие сюръективности на стека эквивалентно сюръективности на локализациях по всем максимальным идеалам: f.SurjectiveOnStalks эквивалентно ∀ максимальный идеал I, локализованный гомоморфизм SURJ.
LaTeX
$$$f.SurjectiveOnStalks \\iff \\forall I\\,(I.IsMaximal),\\ \\text{Function.Surjective}(Localization.localRingHom _ I f rfl)$$$
Lean4
theorem surjectiveOnStalks_iff_forall_maximal :
f.SurjectiveOnStalks ↔
∀ (I : Ideal S) (_ : I.IsMaximal), Function.Surjective (Localization.localRingHom _ I f rfl) :=
by
refine ⟨fun H I hI ↦ H I hI.isPrime, fun H I hI ↦ ?_⟩
simp_rw [surjective_localRingHom_iff] at H ⊢
intro s
obtain ⟨M, hM, hIM⟩ := I.exists_le_maximal hI.ne_top
obtain ⟨x, r, c, hc, hr, e⟩ := H M hM s
exact ⟨x, r, c, fun h ↦ hc (hIM h), fun h ↦ hr (hIM h), e⟩
