surjectiveOnStalks_iff_forall_maximal'

English

Same as above, with a variant form: f.SurjectiveOnStalks iff ∀ I ⊆ S, I.IsMaximal → ∀ s ∈ S, ∃ x, r, c ∉ I, f(r) ∉ I ∧ c f(r) s = c f(x).

Русский

То же самое, но с иной формой условия: для всех максимальных идеалов I и для всех s существуют x,r,c не в I такие, что c f(r) s = c f(x).

LaTeX

$$$f.SurjectiveOnStalks \\iff \\forall I\\ (I.IsMaximal)\\to \\forall s\\in S, \\exists x,r,c\\notin I: f(r)\\notin I \\land c f(r) s = c f(x)$$$

Lean4

theorem surjectiveOnStalks_iff_forall_maximal' :
    f.SurjectiveOnStalks ↔ ∀ I : Ideal S, I.IsMaximal → ∀ s : S, ∃ x r : R, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x :=
  by simp only [surjectiveOnStalks_iff_forall_maximal, surjective_localRingHom_iff]

Похожие утверждения