English
If I is a maximal ideal of R with y not in I, then its image in S under the localization map is maximal.
Русский
Если I — максимальный идеал R и y ∉ I, то образ I в S по локализационной карте максимален.
LaTeX
$$(I.map( algebraMap R S)).IsMaximal$$
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 map.
See `le_relIso_of_maximal` for the more general statement, and the reverse of this implication -/
theorem isMaximal_of_isMaximal_disjoint [IsJacobsonRing R] (I : Ideal R) (hI : I.IsMaximal) (hy : y ∉ I) :
(I.map (algebraMap R S)).IsMaximal :=
by
rw [isMaximal_iff_isMaximal_disjoint S y,
comap_map_of_isPrime_disjoint (powers y) S I (IsMaximal.isPrime hI)
((disjoint_powers_iff_notMem y hI.isPrime.isRadical).2 hy)]
exact ⟨hI, hy⟩
