English
The equivalence between comap equality and maximality: for J in Localization.AtPrime I, Ideal.comap equals I iff J is the maximal ideal.
Русский
Эквивалентность между равенством comap и максимальностью: для J в Localization.AtPrime I, comap равен I тогда и только тогда, когда J — максимальный идеал.
LaTeX
$$$$ \text{eq_maximalIdeal_iff_comap_eq} : \forall J, \; \operatorname{Ideal.comap}(\operatorname{algebraMap} R (Localization.AtPrime I)) J = I \,\Longleftrightarrow\, J = \operatorname{IsLocalRing.maximalIdeal}(Localization.AtPrime I) $$$$
Lean4
/-- The image of `I` in the localization at `I.primeCompl` is a maximal ideal, and in particular
it is the unique maximal ideal given by the local ring structure `AtPrime.isLocalRing` -/
theorem map_eq_maximalIdeal :
Ideal.map (algebraMap R (Localization.AtPrime I)) I = IsLocalRing.maximalIdeal (Localization I.primeCompl) :=
by
convert congr_arg (Ideal.map _) AtPrime.comap_maximalIdeal.symm
rw [map_comap I.primeCompl]
