ideal_eq_bot_of_localization — Mathlib

English

If for every maximal P, the localized image of I is zero, then I = 0.

Русский

Если в каждой локализации максимального P образ I равен нулю, то I = 0.

LaTeX

$$$\\forall P (P\\text{ maximal}), \\; \\mathrm{Ideal.map}(\\mathrm{algebraMap}_{R}^{\\mathrm{Localization.AtPrime}(P)})\\,I = \\mathbf{0} \\Rightarrow I = \\mathbf{0}$$$

Lean4

/-- An ideal is trivial if its localization at every maximal ideal is trivial. -/
theorem ideal_eq_bot_of_localization (I : Ideal R)
    (h : ∀ (J : Ideal R) (_ : J.IsMaximal), IsLocalization.coeSubmodule (Localization.AtPrime J) I = ⊥) : I = ⊥ :=
  bot_unique fun r hr ↦ eq_zero_of_localization r fun J hJ ↦ (h J hJ).le ⟨r, hr, rfl⟩

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