isJacobsonRing_iff_jacobsonSpace — Mathlib

English

A ring is Jacobson if and only if its prime spectrum is a Jacobson space.

Русский

Кольцо является Якобсоновым тогда и только тогда, когда спектр его п является пространством Якобсона.

LaTeX

$$$IsJacobsonRing R \\iff JacobsonSpace (PrimeSpectrum R)$$$

Lean4

theorem isJacobsonRing_iff_jacobsonSpace : IsJacobsonRing R ↔ JacobsonSpace (PrimeSpectrum R) :=
  by
  refine ⟨fun _ ↦ inferInstance, fun H ↦ ⟨fun I hI ↦ le_antisymm ?_ Ideal.le_jacobson⟩⟩
  rw [← I.isRadical_jacobson.radical]
  conv_rhs => rw [← hI.radical]
  simp_rw [← vanishingIdeal_zeroLocus_eq_radical]
  apply vanishingIdeal_anti_mono
  rw [← H.1 (isClosed_zeroLocus I), (isClosed_zeroLocus _).closure_subset_iff]
  rintro x ⟨hx : I ≤ x.asIdeal, hx'⟩
  change jacobson I ≤ x.asIdeal
  exact sInf_le ⟨hx, (isClosed_singleton_iff_isMaximal _).mp hx'⟩

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