isJacobsonRing_localization — Mathlib

English

If S is the localization of a Jacobson ring R at y, then S is Jacobson.

Русский

Если S является локализацией кольца Якобсона R в отношении y, то S тоже является кольцом Якобсона.

LaTeX

$$$IsJacobsonRing(R) \\Rightarrow IsJacobsonRing(S)$$$

Lean4

/-- If `S` is the localization of the Jacobson ring `R` at the submonoid generated by `y : R`, then
`S` is Jacobson. -/
theorem isJacobsonRing_localization [H : IsJacobsonRing R] : IsJacobsonRing S :=
  by
  rw [isJacobsonRing_iff_prime_eq]
  refine fun P' hP' => le_antisymm ?_ le_jacobson
  obtain ⟨hP', hPM⟩ := (IsLocalization.isPrime_iff_isPrime_disjoint (powers y) S P').mp hP'
  have hP := H.out hP'.isRadical
  refine
    (IsLocalization.map_comap (powers y) S P'.jacobson).ge.trans
      ((map_mono ?_).trans (IsLocalization.map_comap (powers y) S P').le)
  have : sInf {I : Ideal R | comap (algebraMap R S) P' ≤ I ∧ I.IsMaximal ∧ y ∉ I} ≤ comap (algebraMap R S) P' :=
    by
    intro x hx
    have hxy : x * y ∈ (comap (algebraMap R S) P').jacobson :=
      by
      rw [Ideal.jacobson, Ideal.mem_sInf]
      intro J hJ
      by_cases h : y ∈ J
      · exact J.mul_mem_left x h
      · exact J.mul_mem_right y ((mem_sInf.1 hx) ⟨hJ.left, ⟨hJ.right, h⟩⟩)
    rw [hP] at hxy
    rcases hP'.mem_or_mem hxy with hxy | hxy
    · exact hxy
    · exact (hPM.le_bot ⟨Submonoid.mem_powers _, hxy⟩).elim
  refine le_trans ?_ this
  rw [Ideal.jacobson, comap_sInf', sInf_eq_iInf]
  refine iInf_le_iInf_of_subset fun I hI => ⟨map (algebraMap R S) I, ⟨?_, ?_⟩⟩
  ·
    exact
      ⟨le_trans (le_of_eq (IsLocalization.map_comap (powers y) S P').symm) (map_mono hI.1),
        isMaximal_of_isMaximal_disjoint y _ hI.2.1 hI.2.2⟩
  ·
    exact
      IsLocalization.comap_map_of_isPrime_disjoint _ S I (IsMaximal.isPrime hI.2.1)
        ((disjoint_powers_iff_notMem y hI.2.1.isPrime.isRadical).2 hI.2.2)

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