isMaximal_iff_isMaximal_disjoint — Mathlib

English

Let R be Jacobson and S the localization of R away from y. For any maximal ideal J of S, the preimage comap R → S of J is maximal in R and disjoint from y in the sense that y is not contained in that preimage's maximal extension.

Русский

Пусть R — кольцо Якобсона, а S — локализация R away от элемента y. Для любой максимальной идеала J в S его предобраз через comaps имеет максимальность в R и не содержит y в соответствующей области.

LaTeX

$$$J\\ IsMaximal \\iff (comap (algebraMap\na R S) J).IsMaximal \\wedge y \\notin I$$$

Lean4

/-- If `R` is a Jacobson ring, then maximal ideals in the localization at `y`
correspond to maximal ideals in the original ring `R` that don't contain `y`.
This lemma gives the correspondence in the particular case of an ideal and its comap.
See `le_relIso_of_maximal` for the more general relation isomorphism -/
theorem isMaximal_iff_isMaximal_disjoint [H : IsJacobsonRing R] (J : Ideal S) :
    J.IsMaximal ↔ (comap (algebraMap R S) J).IsMaximal ∧ y ∉ Ideal.comap (algebraMap R S) J :=
  by
  constructor
  · refine fun h => ⟨?_, fun hy => h.ne_top (Ideal.eq_top_of_isUnit_mem _ hy (map_units _ ⟨y, Submonoid.mem_powers _⟩))⟩
    have hJ : J.IsPrime := IsMaximal.isPrime h
    rw [isPrime_iff_isPrime_disjoint (Submonoid.powers y)] at hJ
    have : y ∉ (comap (algebraMap R S) J).1 := Set.disjoint_left.1 hJ.right (Submonoid.mem_powers _)
    rw [← H.out hJ.left.isRadical, jacobson, Submodule.mem_toAddSubmonoid, Ideal.mem_sInf] at this
    push_neg at this
    rcases this with ⟨I, hI, hI'⟩
    convert hI.right
    by_cases hJ : J = I.map (algebraMap R S)
    · rw [hJ, comap_map_of_isPrime_disjoint (powers y) S I (IsMaximal.isPrime hI.right)]
      rwa [disjoint_powers_iff_notMem y hI.right.isPrime.isRadical]
    · have hI_p : (I.map (algebraMap R S)).IsPrime :=
        by
        refine isPrime_of_isPrime_disjoint (powers y) _ I hI.right.isPrime ?_
        rwa [disjoint_powers_iff_notMem y hI.right.isPrime.isRadical]
      have : J ≤ I.map (algebraMap R S) := map_comap (Submonoid.powers y) S J ▸ map_mono hI.left
      exact absurd (h.1.2 _ (lt_of_le_of_ne this hJ)) hI_p.1
  · refine fun h => ⟨⟨fun hJ => h.1.ne_top (eq_top_iff.2 ?_), fun I hI => ?_⟩⟩
    · rwa [eq_top_iff, ← (IsLocalization.orderEmbedding (powers y) S).le_iff_le] at hJ
    · have := congr_arg (Ideal.map (algebraMap R S)) (h.1.1.2 _ ⟨comap_mono (le_of_lt hI), ?_⟩)
      · rwa [map_comap (powers y) S I, Ideal.map_top] at this
      refine fun hI' => hI.right ?_
      rw [← map_comap (powers y) S I, ← map_comap (powers y) S J]
      exact map_mono hI'

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