surjectiveOnStalks_of_exists_div — Mathlib

English

A succinct equivalence: f.SurjectiveOnStalks iff for all maximal ideals I, the localized map is surjective; equivalently, using a simplified form.

Русский

Краткая эквивалентность: f.SurjectiveOnStalks эквивалентно сюръективности локализованного отображения по всем максимальным идеалам I.

LaTeX

$$$f.SurjectiveOnStalks \\iff \\forall I\\ (I.IsPrime),\\;\\text{surjective\_localRingHom }_I f rfl$$$

Lean4

theorem surjectiveOnStalks_of_exists_div (h : ∀ x : S, ∃ r s : R, IsUnit (f s) ∧ f s * x = f r) :
    SurjectiveOnStalks f :=
  surjectiveOnStalks_iff_forall_ideal.mpr fun I hI x ↦
    let ⟨r, s, hr, hr'⟩ := h x
    ⟨r, s, 1, by simpa [← Ideal.eq_top_iff_one], fun h ↦ hI (I.eq_top_of_isUnit_mem h hr), by simpa⟩

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