Theorems · Theorem · commutative algebra

IsLocalization.isMaximal_iff_isMaximal_disjoint

∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] (y : R) [inst_2 : Algebra R S]
  [IsLocalization.Away y S] [H : IsJacobsonRing R] (J : Ideal S),
  J.IsMaximal ↔ (Ideal.under R J).IsMaximal ∧ y ∉ Ideal.under R J

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

Defined in

Mathlib.RingTheory.Jacobson.Ring

Cited by

3 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraIsLocalization.AwayIsJacobsonRing