Theorems · Theorem · commutative algebra

IsLocalization.isMaximal_of_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] [IsJacobsonRing R] (I : Ideal R),
  I.IsMaximal → y ∉ I → (Ideal.map (algebraMap R S) I).IsMaximal

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 map. See le_relIso_of_maximal for the more general statement, and the reverse of this implication

Defined in

Mathlib.RingTheory.Jacobson.Ring

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIsLocalization.AwayIsJacobsonRing