ideal_ne_top_iff_exists — Mathlib

English

For a Dedekind domain R with R not a field, an ideal I is not the whole ring if and only if I is contained in the ideal of some height-one spectrum element.

Русский

Для кольца Дедекинда R, если R не поле, то I ≠ R тогда и только тогда, когда I ⊆ v.asIdeal для некоторого v в HeightOneSpectrum(R).

LaTeX

$$$I \\neq \\top \\;\\Longleftrightarrow\\; \\exists P:\\HeightOneSpectrum(R),\, I \\le P.asIdeal$$$

Lean4

/-- An ideal of `R` is not the whole ring if and only if it is contained in an element of
`HeightOneSpectrum R` -/
theorem ideal_ne_top_iff_exists (hR : ¬IsField R) (I : Ideal R) : I ≠ ⊤ ↔ ∃ P : HeightOneSpectrum R, I ≤ P.asIdeal :=
  by
  rw [Ideal.ne_top_iff_exists_maximal]
  constructor
  · rintro ⟨M, hMmax, hIM⟩
    exact ⟨(equivMaximalSpectrum hR).symm ⟨M, hMmax⟩, hIM⟩
  · rintro ⟨P, hP⟩
    exact ⟨((equivMaximalSpectrum hR) P).asIdeal, ((equivMaximalSpectrum hR) P).isMaximal, hP⟩

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